From 2ad7fc3cea0bd51fe7dbd52cfaa4fb6625674424 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Thu, 18 Apr 2024 08:47:45 -0400
Subject: [PATCH] refactor: Lint

---
 HepLean.lean                                  |  1 +
 HepLean/AnomalyCancellation/SMNu/Basic.lean   | 27 ++++++-----
 .../AnomalyCancellation/SMNu/FamilyMaps.lean  | 45 +++++++++++--------
 .../SMNu/Permutations.lean                    |  8 ++--
 4 files changed, 48 insertions(+), 33 deletions(-)

diff --git a/HepLean.lean b/HepLean.lean
index 8075639..6dd8813 100644
--- a/HepLean.lean
+++ b/HepLean.lean
@@ -18,3 +18,4 @@ import HepLean.AnomalyCancellation.SM.NoGrav.One.LinearParameterization
 import HepLean.AnomalyCancellation.SM.Permutations
 import HepLean.AnomalyCancellation.SMNu.Basic
 import HepLean.AnomalyCancellation.SMNu.FamilyMaps
+import HepLean.AnomalyCancellation.SMNu.Permutations
diff --git a/HepLean/AnomalyCancellation/SMNu/Basic.lean b/HepLean/AnomalyCancellation/SMNu/Basic.lean
index edcc91a..9d06fc7 100644
--- a/HepLean/AnomalyCancellation/SMNu/Basic.lean
+++ b/HepLean/AnomalyCancellation/SMNu/Basic.lean
@@ -49,7 +49,7 @@ lemma charges_eq_toSpecies_eq (S T : (SMνCharges n).charges) :
   apply Iff.intro
   intro h
   rw [h]
-  simp
+  simp only [forall_const]
   intro h
   apply toSpeciesEquiv.injective
   funext i
@@ -115,7 +115,8 @@ def accGrav : (SMνCharges n).charges →ₗ[ℚ] ℚ where
 lemma accGrav_decomp (S : (SMνCharges n).charges) :
     accGrav S = 6 * ∑ i, Q S i + 3 * ∑ i, U S i + 3 * ∑ i, D S i + 2 * ∑ i, L S i + ∑ i, E S i +
       ∑ i, N S i := by
-  simp
+  simp only [accGrav, SMνSpecies_numberCharges, toSpecies_apply, Fin.isValue, LinearMap.coe_mk,
+    AddHom.coe_mk]
   repeat erw [Finset.sum_add_distrib]
   repeat erw [← Finset.mul_sum]
 
@@ -148,7 +149,8 @@ def accSU2 : (SMνCharges n).charges →ₗ[ℚ] ℚ where
 
 lemma accSU2_decomp (S : (SMνCharges n).charges) :
     accSU2 S = 3 * ∑ i, Q S i + ∑ i, L S i := by
-  simp
+  simp only [accSU2, SMνSpecies_numberCharges, toSpecies_apply, Fin.isValue, LinearMap.coe_mk,
+    AddHom.coe_mk]
   repeat erw [Finset.sum_add_distrib]
   repeat erw [← Finset.mul_sum]
 
@@ -180,7 +182,8 @@ def accSU3 : (SMνCharges n).charges →ₗ[ℚ] ℚ where
 
 lemma accSU3_decomp (S : (SMνCharges n).charges) :
     accSU3 S = 2 * ∑ i, Q S i + ∑ i, U S i + ∑ i, D S i := by
-  simp
+  simp only [accSU3, SMνSpecies_numberCharges, toSpecies_apply, Fin.isValue, LinearMap.coe_mk,
+    AddHom.coe_mk]
   repeat rw [Finset.sum_add_distrib]
   repeat rw [← Finset.mul_sum]
 
@@ -213,7 +216,8 @@ def accYY : (SMνCharges n).charges →ₗ[ℚ] ℚ where
 
 lemma accYY_decomp (S : (SMνCharges n).charges) :
     accYY S = ∑ i, Q S i + 8 * ∑ i, U S i + 2 * ∑ i, D S i + 3 * ∑ i, L S i + 6 * ∑ i, E S i := by
-  simp
+  simp only [accYY, SMνSpecies_numberCharges, toSpecies_apply, Fin.isValue, LinearMap.coe_mk,
+    AddHom.coe_mk]
   repeat rw [Finset.sum_add_distrib]
   repeat rw [← Finset.mul_sum]
 
@@ -246,10 +250,11 @@ def quadBiLin : BiLinearSymm (SMνCharges 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 [SMνSpecies_numberCharges, toSpecies_apply, Fin.isValue, neg_mul, one_mul]
     apply Fintype.sum_congr
     intro i
     ring
@@ -262,7 +267,7 @@ lemma quadBiLin_decomp (S T : (SMνCharges n).charges) :
   simp only
   repeat erw [Finset.sum_add_distrib]
   repeat erw [← Finset.mul_sum]
-  simp
+  simp only [SMνSpecies_numberCharges, toSpecies_apply, Fin.isValue, neg_mul, one_mul, add_left_inj]
   ring
 
 /-- The quadratic anomaly cancellation condition. -/
@@ -308,15 +313,15 @@ def cubeTriLin : TriLinearSymm (SMνCharges 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 [SMνSpecies_numberCharges, toSpecies_apply, Fin.isValue]
     apply Fintype.sum_congr
     intro i
     ring
   swap₂' S T L := by
-    simp
+    simp only [SMνSpecies_numberCharges, toSpecies_apply, Fin.isValue]
     apply Fintype.sum_congr
     intro i
     ring
diff --git a/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean b/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean
index c6eca99..91786d7 100644
--- a/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean
+++ b/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean
@@ -71,7 +71,7 @@ def speciesEmbed (m n : ℕ) :
       0
   map_add' S T := by
     funext i
-    simp
+    simp only [SMνSpecies_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]
@@ -116,13 +116,15 @@ lemma toSpecies_familyUniversal {n : ℕ} (j : Fin 6) (S : (SMνCharges 1).charg
 lemma sum_familyUniversal {n : ℕ} (m : ℕ) (S : (SMνCharges 1).charges) (j : Fin 6) :
     ∑ i, ((fun a => a ^ m) ∘ toSpecies j (familyUniversal n S)) i =
     n * (toSpecies j S ⟨0, by simp⟩) ^ m := by
-  simp
-  have h1 : (n : ℚ) * (toSpecies j S ⟨0, by simp⟩) ^ m = ∑ _i : Fin n,  (toSpecies j S ⟨0, by simp⟩) ^ m:= by
+  simp only [SMνSpecies_numberCharges, Function.comp_apply, toSpecies_apply, Fin.zero_eta,
+    Fin.isValue]
+  have h1 : (n : ℚ) * (toSpecies j S ⟨0, by simp⟩) ^ m =
+      ∑ _i : Fin n, (toSpecies j S ⟨0, by simp⟩) ^ m := by
     rw [Fin.sum_const]
     simp
   erw [h1]
   apply Finset.sum_congr
-  simp
+  simp only
   intro i _
   erw [toSpecies_familyUniversal]
 
@@ -134,10 +136,10 @@ lemma sum_familyUniversal_two {n : ℕ} (S : (SMνCharges 1).charges)
     (T : (SMνCharges n).charges) (j : Fin 6) :
     ∑ i, (toSpecies j (familyUniversal n S) i * toSpecies j T i) =
     (toSpecies j S ⟨0, by simp⟩) * ∑ i, toSpecies j T i := by
-  simp
+  simp only [SMνSpecies_numberCharges, toSpecies_apply, Fin.zero_eta, Fin.isValue]
   rw [Finset.mul_sum]
   apply Finset.sum_congr
-  simp
+  simp only
   intro i _
   erw [toSpecies_familyUniversal]
   rfl
@@ -146,41 +148,45 @@ lemma sum_familyUniversal_three  {n : ℕ} (S : (SMνCharges 1).charges)
     (T L : (SMνCharges n).charges) (j : Fin 6) :
     ∑ i, (toSpecies j (familyUniversal n S) i * toSpecies j T i * toSpecies j L i) =
     (toSpecies j S ⟨0, by simp⟩) * ∑ i, toSpecies j T i * toSpecies j L i := by
-  simp
+  simp only [SMνSpecies_numberCharges, toSpecies_apply, Fin.zero_eta, Fin.isValue]
   rw [Finset.mul_sum]
   apply Finset.sum_congr
-  simp
+  simp only
   intro i _
   erw [toSpecies_familyUniversal]
-  simp
+  simp only [SMνSpecies_numberCharges, Fin.zero_eta, Fin.isValue, toSpecies_apply]
   ring
 
 lemma familyUniversal_accGrav (S : (SMνCharges 1).charges) :
     accGrav (familyUniversal n S)  = n * (accGrav S) := by
   rw [accGrav_decomp, accGrav_decomp]
   repeat rw [sum_familyUniversal_one]
-  simp
+  simp only [Fin.isValue, SMνSpecies_numberCharges, Fin.zero_eta, toSpecies_apply,
+    Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton]
   ring
 
 lemma familyUniversal_accSU2 (S : (SMνCharges 1).charges) :
     accSU2 (familyUniversal n S)  = n * (accSU2 S) := by
   rw [accSU2_decomp, accSU2_decomp]
   repeat rw [sum_familyUniversal_one]
-  simp
+  simp only [Fin.isValue, SMνSpecies_numberCharges, Fin.zero_eta, toSpecies_apply,
+    Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton]
   ring
 
 lemma familyUniversal_accSU3 (S : (SMνCharges 1).charges) :
     accSU3 (familyUniversal n S)  = n * (accSU3 S) := by
   rw [accSU3_decomp, accSU3_decomp]
   repeat rw [sum_familyUniversal_one]
-  simp
+  simp only [Fin.isValue, SMνSpecies_numberCharges, Fin.zero_eta, toSpecies_apply,
+    Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton]
   ring
 
 lemma familyUniversal_accYY (S : (SMνCharges 1).charges) :
     accYY (familyUniversal n S)  = n * (accYY S) := by
   rw [accYY_decomp, accYY_decomp]
   repeat rw [sum_familyUniversal_one]
-  simp
+  simp only [Fin.isValue, SMνSpecies_numberCharges, Fin.zero_eta, toSpecies_apply,
+    Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton]
   ring
 
 lemma familyUniversal_quadBiLin (S : (SMνCharges 1).charges) (T : (SMνCharges n).charges) :
@@ -190,7 +196,8 @@ lemma familyUniversal_quadBiLin (S : (SMνCharges 1).charges) (T : (SMνCharges
   rw [quadBiLin_decomp]
   repeat rw [sum_familyUniversal_two]
   repeat rw [toSpecies_one]
-  simp
+  simp only [Fin.isValue, SMνSpecies_numberCharges, toSpecies_apply, add_left_inj, sub_left_inj,
+    sub_right_inj]
   ring
 
 lemma familyUniversal_accQuad (S : (SMνCharges 1).charges) :
@@ -198,7 +205,8 @@ lemma familyUniversal_accQuad (S : (SMνCharges 1).charges) :
   rw [accQuad_decomp]
   repeat erw [sum_familyUniversal]
   rw [accQuad_decomp]
-  simp
+  simp only [Fin.isValue, SMνSpecies_numberCharges, Fin.zero_eta, toSpecies_apply,
+    Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton]
   ring
 
 lemma familyUniversal_cubeTriLin (S : (SMνCharges 1).charges) (T R : (SMνCharges n).charges) :
@@ -209,7 +217,7 @@ lemma familyUniversal_cubeTriLin (S : (SMνCharges 1).charges) (T R : (SMνCharg
   rw [cubeTriLin_decomp]
   repeat rw [sum_familyUniversal_three]
   repeat rw [toSpecies_one]
-  simp
+  simp only [Fin.isValue, SMνSpecies_numberCharges, toSpecies_apply, add_left_inj]
   ring
 
 lemma familyUniversal_cubeTriLin' (S T : (SMνCharges 1).charges) (R : (SMνCharges n).charges) :
@@ -222,7 +230,7 @@ lemma familyUniversal_cubeTriLin' (S T : (SMνCharges 1).charges) (R : (SMνChar
   rw [familyUniversal_cubeTriLin]
   repeat rw [sum_familyUniversal_two]
   repeat rw [toSpecies_one]
-  simp
+  simp only [Fin.isValue, SMνSpecies_numberCharges, toSpecies_apply]
   ring
 
 lemma familyUniversal_accCube (S : (SMνCharges 1).charges) :
@@ -230,7 +238,8 @@ lemma familyUniversal_accCube (S : (SMνCharges 1).charges) :
   rw [accCube_decomp]
   repeat erw [sum_familyUniversal]
   rw [accCube_decomp]
-  simp
+  simp only [Fin.isValue, SMνSpecies_numberCharges, Fin.zero_eta, toSpecies_apply,
+    Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton]
   ring
 
 end SMRHN
diff --git a/HepLean/AnomalyCancellation/SMNu/Permutations.lean b/HepLean/AnomalyCancellation/SMNu/Permutations.lean
index 36878c4..2d05f3a 100644
--- a/HepLean/AnomalyCancellation/SMNu/Permutations.lean
+++ b/HepLean/AnomalyCancellation/SMNu/Permutations.lean
@@ -30,7 +30,7 @@ def permGroup (n : ℕ) := Fin 6 → Equiv.Perm (Fin n)
 
 variable {n : ℕ}
 
-@[simps!]
+@[simp]
 instance : Group (permGroup n) := Pi.group
 
 /-- The image of an element of `permGroup n` under the representation on charges. -/
@@ -52,16 +52,16 @@ def chargeMap (f : permGroup n) : (SMνCharges n).charges →ₗ[ℚ] (SMνCharg
     rfl
 
 /-- The representation of `(permGroup n)` acting on the vector space of charges. -/
-@[simps!]
+@[simp]
 def repCharges {n : ℕ} : Representation ℚ (permGroup n) (SMνCharges n).charges where
   toFun f := chargeMap f⁻¹
   map_mul' f g :=by
-    simp
+    simp only [permGroup, mul_inv_rev]
     apply LinearMap.ext
     intro S
     rw [charges_eq_toSpecies_eq]
     intro i
-    simp
+    simp only [chargeMap_apply, Pi.mul_apply, Pi.inv_apply, Equiv.Perm.coe_mul, LinearMap.mul_apply]
     repeat erw [toSMSpecies_toSpecies_inv]
     rfl
   map_one' := by