refactor: Lint

HepLean/AnomalyCancellation/SM/Basic.lean

@@ -51,7 +51,7 @@ lemma charges_eq_toSpecies_eq (S T : (SMCharges n).charges) :
   apply Iff.intro
   intro h
   rw [h]
-  simp
+  simp only [forall_const]
   intro h
   apply toSpeciesEquiv.injective
   funext i
@@ -108,7 +108,8 @@ def accGrav : (SMCharges n).charges →ₗ[ℚ] ℚ where
 lemma accGrav_ext {S T : (SMCharges n).charges}
     (hj : ∀ (j : Fin 5),  ∑ i, (toSpecies j) S i = ∑ i, (toSpecies j) T i) :
     accGrav S = accGrav T := by
-  simp
+  simp only [accGrav, SMSpecies_numberCharges, toSpecies_apply, Fin.isValue, LinearMap.coe_mk,
+    AddHom.coe_mk]
   repeat erw [Finset.sum_add_distrib]
   repeat erw [← Finset.mul_sum]
   repeat erw [hj]
@@ -137,7 +138,8 @@ def accSU2 : (SMCharges n).charges →ₗ[ℚ] ℚ where
 lemma accSU2_ext {S T : (SMCharges n).charges}
     (hj : ∀ (j : Fin 5),  ∑ i, (toSpecies j) S i = ∑ i, (toSpecies j) T i) :
     accSU2 S = accSU2 T := by
-  simp
+  simp only [accSU2, SMSpecies_numberCharges, toSpecies_apply, Fin.isValue, LinearMap.coe_mk,
+    AddHom.coe_mk]
   repeat erw [Finset.sum_add_distrib]
   repeat erw [← Finset.mul_sum]
   repeat erw [hj]
@@ -166,7 +168,8 @@ def accSU3 : (SMCharges n).charges →ₗ[ℚ] ℚ where
 lemma accSU3_ext {S T : (SMCharges n).charges}
     (hj : ∀ (j : Fin 5),  ∑ i, (toSpecies j) S i = ∑ i, (toSpecies j) T i) :
     accSU3 S = accSU3 T := by
-  simp
+  simp only [accSU3, SMSpecies_numberCharges, toSpecies_apply, Fin.isValue, LinearMap.coe_mk,
+    AddHom.coe_mk]
   repeat erw [Finset.sum_add_distrib]
   repeat erw [← Finset.mul_sum]
   repeat erw [hj]
@@ -196,7 +199,8 @@ def accYY : (SMCharges n).charges →ₗ[ℚ] ℚ where
 lemma accYY_ext {S T : (SMCharges n).charges}
     (hj : ∀ (j : Fin 5),  ∑ i, (toSpecies j) S i = ∑ i, (toSpecies j) T i) :
     accYY S = accYY T := by
-  simp
+  simp only [accYY, SMSpecies_numberCharges, toSpecies_apply, Fin.isValue, LinearMap.coe_mk,
+    AddHom.coe_mk]
   repeat erw [Finset.sum_add_distrib]
   repeat erw [← Finset.mul_sum]
   repeat erw [hj]
@@ -224,10 +228,11 @@ def quadBiLin : BiLinearSymm (SMCharges n).charges where
     apply Fintype.sum_congr
     intro i
     repeat erw [map_add]
-    simp
+    simp only [ACCSystemCharges.chargesAddCommMonoid_add, toSpecies_apply, Fin.isValue, neg_mul,
+      one_mul]
     ring
   swap' S T := by
-    simp
+    simp only [SMSpecies_numberCharges, toSpecies_apply, Fin.isValue, neg_mul, one_mul]
     apply Fintype.sum_congr
     intro i
     ring
@@ -274,15 +279,15 @@ def cubeTriLin : TriLinearSymm (SMCharges n).charges where
     apply Fintype.sum_congr
     intro i
     repeat erw [map_add]
-    simp
+    simp only [ACCSystemCharges.chargesAddCommMonoid_add, toSpecies_apply, Fin.isValue]
     ring
   swap₁' S T L := by
-    simp
+    simp only [SMSpecies_numberCharges, toSpecies_apply, Fin.isValue]
     apply Fintype.sum_congr
     intro i
     ring
   swap₂' S T L := by
-    simp
+    simp only [SMSpecies_numberCharges, toSpecies_apply, Fin.isValue]
     apply Fintype.sum_congr
     intro i
     ring

HepLean/AnomalyCancellation/SM/FamilyMaps.lean

@@ -66,7 +66,7 @@ def speciesEmbed (m n : ℕ) :
       0
   map_add' S T := by
     funext i
-    simp
+    simp only [SMSpecies_numberCharges, ACCSystemCharges.chargesAddCommMonoid_add]
     by_cases hi : i.val < m
     erw [dif_pos hi, dif_pos hi, dif_pos hi]
     erw [dif_neg hi, dif_neg hi, dif_neg hi]

HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean

@@ -6,7 +6,6 @@ Authors: Joseph Tooby-Smith
 import HepLean.AnomalyCancellation.SM.Basic
 import HepLean.AnomalyCancellation.SM.NoGrav.Basic
 import HepLean.AnomalyCancellation.SM.NoGrav.One.LinearParameterization
-universe v u
 /-!
 # Lemmas for 1 family SM Accs
 
@@ -16,6 +15,7 @@ https://arxiv.org/abs/1907.00514
 That eveery solution to the ACCs without gravity satifies for free the gravitational anomaly.
 -/
 
+universe v u
 namespace SM
 namespace SMNoGrav
 namespace One

HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean

@@ -9,8 +9,6 @@ import Mathlib.Tactic.FieldSimp
 import Mathlib.Tactic.Linarith
 import Mathlib.NumberTheory.FLT.Basic
 import Mathlib.Algebra.QuadraticDiscriminant
-
-universe v u
 /-!
 # Parameterizations for solutions to the linear ACCs for 1 family
 
@@ -22,7 +20,7 @@ These parameterizations are based on:
 https://arxiv.org/abs/1907.00514
 -/
 
-
+universe v u
 namespace SM
 namespace SMNoGrav
 namespace One
@@ -43,7 +41,8 @@ structure linearParameters where
 namespace linearParameters
 
 @[ext]
-lemma ext {S T : linearParameters} (hQ : S.Q' = T.Q') (hY : S.Y = T.Y) (hE : S.E' = T.E')  : S = T := by
+lemma ext {S T : linearParameters} (hQ : S.Q' = T.Q') (hY : S.Y = T.Y) (hE : S.E' = T.E') :
+    S = T := by
   cases' S
   simp_all only
 
@@ -57,7 +56,8 @@ def asCharges (S : linearParameters) : (SMNoGrav 1).charges := fun i =>
   | (3: Fin 5) => - 3 * S.Q'
   | (4 : Fin 5) => S.E'
 
-lemma speciesVal (S : linearParameters) : (toSpecies i) S.asCharges (0 : Fin 1) = S.asCharges i := by
+lemma speciesVal (S : linearParameters) :
+    (toSpecies i) S.asCharges (0 : Fin 1) = S.asCharges i := by
   match i with
   | 0 => rfl
   | 1 => rfl
@@ -76,7 +76,7 @@ def asLinear (S : linearParameters) : (SMNoGrav 1).LinSols :=
     simp only [accSU3, SMSpecies_numberCharges, Finset.univ_unique, Fin.default_eq_zero,
       Fin.isValue, Finset.sum_singleton, LinearMap.coe_mk, AddHom.coe_mk]
     repeat erw [speciesVal]
-    simp
+    simp only [asCharges, neg_add_rev]
     ring)
 
 lemma asLinear_val (S : linearParameters) : S.asLinear.val = S.asCharges := by
@@ -92,7 +92,7 @@ lemma cubic (S : linearParameters) :
   simp only [SMSpecies_numberCharges, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
     Finset.sum_singleton]
   repeat erw [speciesVal]
-  simp
+  simp only [asCharges, neg_add_rev, neg_mul, mul_neg, neg_neg]
   ring
 
 lemma cubic_zero_Q'_zero (S : linearParameters) (hc : accCube (S.asCharges) = 0)
@@ -129,13 +129,13 @@ def bijection : linearParameters ≃ (SMNoGrav 1).LinSols where
     repeat erw [speciesVal]
     simp only [Fin.isValue]
     repeat erw [speciesVal]
-    simp
+    simp only [asCharges, neg_add_rev]
     ring
     simp only [toSpecies_apply]
     repeat erw [speciesVal]
     rfl
   right_inv S := by
-    simp
+    simp only [Fin.isValue, toSpecies_apply]
     apply ACCSystemLinear.LinSols.ext
     rw [charges_eq_toSpecies_eq]
     intro i
@@ -167,7 +167,7 @@ def bijection : linearParameters ≃ (SMNoGrav 1).LinSols where
 /-- The bijection between the linear parameters and `(SMNoGrav 1).LinSols` in the special
 case when Q and E are both not zero. -/
 def bijectionQEZero : {S : linearParameters // S.Q' ≠ 0 ∧ S.E' ≠ 0} ≃
-  {S : (SMNoGrav 1).LinSols // Q S.val (0 : Fin 1) ≠ 0 ∧ E S.val (0 : Fin 1) ≠ 0} where
+    {S : (SMNoGrav 1).LinSols // Q S.val (0 : Fin 1) ≠ 0 ∧ E S.val (0 : Fin 1) ≠ 0} where
   toFun S := ⟨bijection S, S.2⟩
   invFun S := ⟨bijection.symm S, S.2⟩
   left_inv S := by
@@ -183,7 +183,7 @@ lemma grav (S : linearParameters) :
   simp only [SMSpecies_numberCharges, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
     Finset.sum_singleton, LinearMap.coe_mk, AddHom.coe_mk]
   repeat erw [speciesVal]
-  simp
+  simp only [asCharges, neg_add_rev, neg_mul, mul_neg]
   ring_nf
   rw [add_comm, add_eq_zero_iff_eq_neg]
   simp
@@ -217,7 +217,8 @@ def toLinearParameters (S : linearParametersQENeqZero) :
   ⟨⟨S.x,   3 * S.x * (S.v - S.w) / (S.v + S.w),  - 6 * S.x  / (S.v + S.w)⟩,
     by
       apply And.intro S.hx
-      simp
+      simp only [neg_mul, ne_eq, div_eq_zero_iff, neg_eq_zero, mul_eq_zero, OfNat.ofNat_ne_zero,
+        false_or]
       rw [not_or]
       exact And.intro S.hx S.hvw⟩
 
@@ -228,11 +229,11 @@ def tolinearParametersQNeqZero (S : {S : linearParameters //  S.Q' ≠  0 ∧ S.
     linearParametersQENeqZero :=
   ⟨S.1.Q', - (3 * S.1.Q' + S.1.Y) / S.1.E', - (3 * S.1.Q' - S.1.Y)/ S.1.E',  S.2.1,
     by
-      simp
+      simp only [ne_eq, neg_add_rev, neg_sub]
       field_simp
       rw [not_or]
       ring_nf
-      simp
+      simp only [neg_eq_zero, mul_eq_zero, OfNat.ofNat_ne_zero, or_false]
       exact S.2⟩
 
 /-- A bijection between the type `linearParametersQENeqZero` and linear parameters
@@ -246,10 +247,11 @@ def bijectionLinearParameters :
     have hvw := S.hvw
     have hQ := S.hx
     apply linearParametersQENeqZero.ext
-    simp
+    simp only [tolinearParametersQNeqZero_x, toLinearParameters_coe_Q']
     field_simp
     ring
-    simp
+    simp only [tolinearParametersQNeqZero_w, toLinearParameters_coe_Y, toLinearParameters_coe_Q',
+      toLinearParameters_coe_E']
     field_simp
     ring
   right_inv S := by
@@ -257,7 +259,7 @@ def bijectionLinearParameters :
     have hQ := S.2.1
     have hE := S.2.2
     apply linearParameters.ext
-    simp
+    simp only [ne_eq, toLinearParameters_coe_Q', tolinearParametersQNeqZero_x]
     field_simp
     ring_nf
     field_simp [hQ, hE]
@@ -275,7 +277,8 @@ def bijection : linearParametersQENeqZero ≃
 lemma cubic (S : linearParametersQENeqZero) :
     accCube (bijection S).1.val = 0 ↔ S.v ^ 3 + S.w ^ 3 = -1 := by
   erw [linearParameters.cubic]
-  simp
+  simp only [ne_eq, bijectionLinearParameters_apply_coe_Q', neg_mul,
+    bijectionLinearParameters_apply_coe_Y, div_pow, bijectionLinearParameters_apply_coe_E']
   have hvw := S.hvw
   have hQ := S.hx
   field_simp
@@ -365,7 +368,7 @@ lemma grav_of_cubic (S : linearParametersQENeqZero) (h : accCube (bijection S).1
   have h' := cube_w_v S h
   cases' h' with h h
   rw [h.1, h.2]
-  simp
+  simp only [add_zero]
   rw [h.1, h.2]
   simp