refactor: Lint

HepLean.lean

@@ -95,6 +95,7 @@ import HepLean.Lorentz.PauliMatrices.SelfAdjoint
 import HepLean.Lorentz.RealVector.Basic
 import HepLean.Lorentz.RealVector.Contraction
 import HepLean.Lorentz.RealVector.Modules
+import HepLean.Lorentz.RealVector.NormOne
 import HepLean.Lorentz.SL2C.Basic
 import HepLean.Lorentz.Weyl.Basic
 import HepLean.Lorentz.Weyl.Contraction

HepLean/Lorentz/Group/Basic.lean

@@ -123,7 +123,6 @@ instance (M : LorentzGroup d) : Invertible M.1 where
     rw [← coe_inv]
     exact (mem_iff_self_mul_dual.mp M.2)
 
-@[simp]
 lemma subtype_inv_mul : (Subtype.val Λ)⁻¹ * (Subtype.val Λ) = 1 := by
   trans Subtype.val (Λ⁻¹ * Λ)
   · rw [← coe_inv]
@@ -131,7 +130,6 @@ lemma subtype_inv_mul : (Subtype.val Λ)⁻¹ * (Subtype.val Λ) = 1 := by
   · rw [inv_mul_cancel Λ]
     rfl
 
-@[simp]
 lemma subtype_mul_inv : (Subtype.val Λ) * (Subtype.val Λ)⁻¹ = 1 := by
   trans Subtype.val (Λ * Λ⁻¹)
   · rw [← coe_inv]

HepLean/Lorentz/Group/Boosts.lean

@@ -145,7 +145,7 @@ lemma toMatrix_apply (u v : FuturePointing d) (μ ν : Fin 1 ⊕ Fin d) :
   rw [contrContrContractField.matrix_apply_stdBasis (Λ := toMatrix u v) μ ν, toMatrix_mulVec]
   simp only [genBoost, genBoostAux₁, genBoostAux₂, smul_add, neg_smul, LinearMap.add_apply,
     LinearMap.id_apply, LinearMap.coe_mk, AddHom.coe_mk, contrContrContractField.basis_left,
-    map_add, map_smul, map_neg, toField_apply, mul_eq_mul_left_iff]
+    map_add, map_smul, map_neg, mul_eq_mul_left_iff]
   ring_nf
   simp only [Pi.add_apply, Action.instMonoidalCategory_tensorObj_V,
     Action.instMonoidalCategory_tensorUnit_V, CategoryTheory.Equivalence.symm_inverse,

HepLean/Lorentz/RealVector/Basic.lean

@@ -61,9 +61,6 @@ def Co (d : ℕ) : Rep ℝ (LorentzGroup d) := Rep.of CoMod.rep
 
 open CategoryTheory.MonoidalCategory
 
-def toField (d : ℕ) : (𝟙_ (Rep ℝ ↑(LorentzGroup d))) →ₗ[ℝ] ℝ := LinearMap.id
-
-lemma toField_apply {d : ℕ} (a : 𝟙_ (Rep ℝ ↑(LorentzGroup d))) : toField d a = a := rfl
 /-!
 
 ## Isomorphism between contravariant and covariant Lorentz vectors

HepLean/Lorentz/RealVector/Contraction.lean

@@ -200,7 +200,7 @@ lemma action_tmul (g : LorentzGroup d) : ⟪(Contr d).ρ g x, (Contr d).ρ g y
   rfl
 
 lemma as_sum : ⟪x, y⟫ₘ = x.val (Sum.inl 0) * y.val (Sum.inl 0) -
-      ∑ i, x.val (Sum.inr i) * y.val (Sum.inr i) := by
+    ∑ i, x.val (Sum.inr i) * y.val (Sum.inr i) := by
   rw [contrContrContract_hom_tmul]
   simp only [dotProduct, minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, mulVec_diagonal,
     Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, Sum.elim_inl,
@@ -214,7 +214,6 @@ lemma as_sum_toSpace : ⟪x, y⟫ₘ = x.val (Sum.inl 0) * y.val (Sum.inl 0) -
   rw [as_sum]
   rfl
 
-@[simp]
 lemma stdBasis_inl {d : ℕ} :
     ⟪@ContrMod.stdBasis d (Sum.inl 0), ContrMod.stdBasis (Sum.inl 0)⟫ₘ = (1 : ℝ) := by
   rw [as_sum]

HepLean/Lorentz/RealVector/Modules.lean

@@ -136,9 +136,11 @@ lemma stdBasis_decomp (v : ContrMod d) : v = ∑ i, v.toFin1dℝ i • stdBasis
 
 -/
 
+/-- Multiplication of a matrix with a vector in `ContrMod`. -/
 abbrev mulVec (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v : ContrMod d) :
     ContrMod d := Matrix.toLinAlgEquiv stdBasis M v
 
+/-- Multiplication of a matrix with a vector in `ContrMod`. -/
 scoped[Lorentz] infixr:73 " *ᵥ " => ContrMod.mulVec
 
 @[simp]
@@ -173,6 +175,8 @@ lemma mulVec_mulVec (M N : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v :
 (Not the Minkowski norm, but the norm of a vector in `ContrℝModule d`.)
 -/
 
+/-- A `NormedAddCommGroup` structure on `ContrMod`. This is not an instance, as we
+  don't want it to be applied always. -/
 def norm : NormedAddCommGroup (ContrMod d) where
   norm v := ‖v.val‖₊
   dist_self x := Pi.normedAddCommGroup.dist_self x.val
@@ -180,6 +184,8 @@ def norm : NormedAddCommGroup (ContrMod d) where
   dist_comm x y := Pi.normedAddCommGroup.dist_comm x.val y.val
   eq_of_dist_eq_zero {x y} := fun h => ext (MetricSpace.eq_of_dist_eq_zero h)
 
+/-- The underlying space part of a `ContrMod` formed by removing the first element.
+  A better name for this might be `tail`. -/
 def toSpace (v : ContrMod d) : EuclideanSpace ℝ (Fin d) := v.val ∘ Sum.inr
 
 /-!
@@ -368,9 +374,11 @@ lemma stdBasis_decomp (v : CoMod d) : v = ∑ i, v.toFin1dℝ i • stdBasis i :
 
 -/
 
+/-- Multiplication of a matrix with a vector in `CoMod`. -/
 abbrev mulVec (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v : CoMod d) :
     CoMod d := Matrix.toLinAlgEquiv stdBasis M v
 
+/-- Multiplication of a matrix with a vector in `CoMod`. -/
 scoped[Lorentz] infixr:73 " *ᵥ " => CoMod.mulVec
 
 @[simp]

HepLean/Lorentz/RealVector/NormOne.lean

@@ -208,7 +208,7 @@ lemma metric_reflect_not_mem_not_mem (h : v ∉ FuturePointing d) (hw : w ∉ Fu
   simp [neg, neg_tmul, tmul_neg]
 
 lemma metric_reflect_mem_not_mem (h : v ∈ FuturePointing d) (hw : w ∉ FuturePointing d) :
-   ⟪v.val, (Contr d).ρ LorentzGroup.parity w.1⟫ₘ ≤ 0 := by
+    ⟪v.val, (Contr d).ρ LorentzGroup.parity w.1⟫ₘ ≤ 0 := by
   rw [show (0 : ℝ) = - 0 from zero_eq_neg.mpr rfl, le_neg]
   have h1 := metric_reflect_mem_mem h ((not_mem_iff_neg w).mp hw)
   apply le_of_le_of_eq h1 ?_
@@ -248,8 +248,8 @@ noncomputable def pathFromTime (u : FuturePointing d) : Path timeVecNormOneFutur
       | Sum.inr i => t * u.1.1.toSpace i},
     by
       rw [NormOne.mem_iff, contrContrContractField.as_sum_toSpace]
-      simp only [ContrMod.toSpace, Function.comp_apply, PiLp.inner_apply, RCLike.inner_apply, map_mul,
+      simp only [ContrMod.toSpace, Function.comp_apply, PiLp.inner_apply, RCLike.inner_apply,
-        conj_trivial]
+        map_mul, conj_trivial]
       rw [Real.mul_self_sqrt, ← @real_inner_self_eq_norm_sq, @PiLp.inner_apply]
       · simp only [Function.comp_apply, RCLike.inner_apply, conj_trivial]
         refine Eq.symm (eq_sub_of_add_eq (congrArg (HAdd.hAdd _) ?_))

HepLean/Lorentz/SL2C/Basic.lean

@@ -76,6 +76,8 @@ lemma toLinearMapSelfAdjointMatrix_det (M : SL(2, ℂ)) (A : selfAdjoint (Matrix
     selfAdjoint.mem_iff, det_conjTranspose, det_mul, det_one, RingHom.id_apply]
   simp only [SpecialLinearGroup.det_coe, one_mul, star_one, mul_one]
 
+/-- The monoid homomorphisms from `SL(2, ℂ)` to matrices indexed by `Fin 1 ⊕ Fin 3`
+  formed by the action `M A Mᴴ`. -/
 def toMatrix : SL(2, ℂ) →* Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ where
   toFun M := LinearMap.toMatrix PauliMatrix.σSAL PauliMatrix.σSAL (toLinearMapSelfAdjointMatrix M)
   map_one' := by