refactor: Lint

HepLean/SpaceTime/WeylFermion/Basic.lean

@@ -55,7 +55,7 @@ def leftBasis : Basis (Fin 2) ℂ leftHanded := Basis.ofEquivFun
 lemma leftBasis_ρ_apply (M : SL(2,ℂ)) (i j : Fin 2) :
     (LinearMap.toMatrix leftBasis leftBasis) (leftHanded.ρ M) i j = M.1 i j := by
   rw [LinearMap.toMatrix_apply]
-  simp [leftBasis]
+  simp only [leftBasis, Basis.coe_ofEquivFun, Basis.ofEquivFun_repr_apply]
   change (M.1 *ᵥ (Pi.single j 1)) i = _
   simp only [mulVec_single, mul_one]
 

HepLean/SpaceTime/WeylFermion/Contraction.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.SpaceTime.WeylFermion.Basic
-import LLMlean
 /-!
 
 # Contraction of Weyl fermions

HepLean/SpaceTime/WeylFermion/Metric.lean

@@ -26,6 +26,7 @@ open Complex
 open TensorProduct
 open CategoryTheory.MonoidalCategory
 
+/-- The raw `2x2` matrix corresponding to the metric for fermions. -/
 def metricRaw : Matrix (Fin 2) (Fin 2) ℂ := !![0, 1; -1, 0]
 
 lemma comm_metricRaw (M : SL(2,ℂ)) : M.1 * metricRaw = metricRaw * (M.1⁻¹)ᵀ := by
@@ -91,7 +92,7 @@ def leftMetric : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ leftHanded ⊗ leftHanded where
       (TensorProduct.map (leftHanded.ρ M) (leftHanded.ρ M)) (x' • leftMetricVal)
     simp only [Action.instMonoidalCategory_tensorObj_V, _root_.map_smul]
     apply congrArg
-    simp [leftMetricVal]
+    simp only [Action.instMonoidalCategory_tensorObj_V, leftMetricVal, map_neg, neg_inj]
     erw [leftLeftToMatrix_ρ_symm]
     apply congrArg
     rw [comm_metricRaw, mul_assoc, ← @transpose_mul]
@@ -124,7 +125,7 @@ def altLeftMetric : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altLeftHanded ⊗ altLeftHande
       (TensorProduct.map (altLeftHanded.ρ M) (altLeftHanded.ρ M)) (x' • altLeftMetricVal)
     simp only [Action.instMonoidalCategory_tensorObj_V, _root_.map_smul]
     apply congrArg
-    simp [altLeftMetricVal]
+    simp only [Action.instMonoidalCategory_tensorObj_V, altLeftMetricVal]
     erw [altLeftaltLeftToMatrix_ρ_symm]
     apply congrArg
     rw [← metricRaw_comm, mul_assoc]

HepLean/SpaceTime/WeylFermion/Unit.lean

@@ -81,7 +81,7 @@ def altLeftLeftUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altLeftHanded ⊗ leftHanded
       (TensorProduct.map (altLeftHanded.ρ M) (leftHanded.ρ M)) (x' • altLeftLeftUnitVal)
     simp only [Action.instMonoidalCategory_tensorObj_V, _root_.map_smul]
     apply congrArg
-    simp [altLeftLeftUnitVal]
+    simp only [Action.instMonoidalCategory_tensorObj_V, altLeftLeftUnitVal]
     erw [altLeftLeftToMatrix_ρ_symm]
     apply congrArg
     simp only [mul_one, ← transpose_mul, SpecialLinearGroup.det_coe, isUnit_iff_ne_zero, ne_eq,
@@ -154,7 +154,7 @@ def altRightRightUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altRightHanded ⊗ rightHa
       (TensorProduct.map (altRightHanded.ρ M) (rightHanded.ρ M)) (x' • altRightRightUnitVal)
     simp only [Action.instMonoidalCategory_tensorObj_V, _root_.map_smul]
     apply congrArg
-    simp [altRightRightUnitVal]
+    simp only [Action.instMonoidalCategory_tensorObj_V, altRightRightUnitVal]
     erw [altRightRightToMatrix_ρ_symm]
     apply congrArg
     simp only [mul_one, RCLike.star_def]