From 2792027a7faa7615e2fb98b5109030bf7f1bf7d9 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Mon, 9 Sep 2024 06:01:25 -0400
Subject: [PATCH] refactor: more simp to simp only

---
 .../PureU1/Even/Parameterization.lean         |  7 ++---
 .../PureU1/Permutations.lean                  | 30 +++++++++----------
 HepLean/AnomalyCancellation/PureU1/Sorts.lean |  2 +-
 HepLean/AnomalyCancellation/SM/Basic.lean     | 27 ++++++++++-------
 .../AnomalyCancellation/SM/FamilyMaps.lean    |  3 +-
 .../SM/NoGrav/One/LinearParameterization.lean | 30 ++++++++++---------
 .../SMNu/PlusU1/BoundPlaneDim.lean            |  4 +--
 .../SMNu/PlusU1/QuadSolToSol.lean             |  3 +-
 .../FlavorPhysics/CKMMatrix/Invariants.lean   |  3 +-
 9 files changed, 59 insertions(+), 50 deletions(-)

diff --git a/HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean b/HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean
index cfbef73..3ea4c90 100644
--- a/HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean
@@ -129,7 +129,7 @@ theorem generic_case {S : (PureU1 (2 * n.succ)).Sols} (h : GenericCase S) :
   · exact hS
   · have h := h g f hS
     rw [anomalyFree_param _ _ hS] at h
-    simp at h
+    simp only [Nat.succ_eq_add_one, accCubeTriLinSymm_toFun_apply_apply, ne_eq, neg_eq_zero] at h
     exact h
 
 lemma special_case_lineInCubic {S : (PureU1 (2 * n.succ)).Sols}
@@ -141,10 +141,9 @@ lemma special_case_lineInCubic {S : (PureU1 (2 * n.succ)).Sols}
   have h := h g f hS
   rw [accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂,
     accCubeTriLinSymm.map_smul₃, accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂,
-    accCubeTriLinSymm.map_smul₃]
-  rw [h]
+    accCubeTriLinSymm.map_smul₃, h]
   rw [anomalyFree_param _ _ hS] at h
-  simp at h
+  simp only [Nat.succ_eq_add_one, accCubeTriLinSymm_toFun_apply_apply, neg_eq_zero] at h
   change accCubeTriLinSymm (P! f) (P! f) (P g) = 0 at h
   erw [h]
   simp
diff --git a/HepLean/AnomalyCancellation/PureU1/Permutations.lean b/HepLean/AnomalyCancellation/PureU1/Permutations.lean
index 5b758fe..4a375d6 100644
--- a/HepLean/AnomalyCancellation/PureU1/Permutations.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Permutations.lean
@@ -26,9 +26,7 @@ namespace PureU1
 @[simp]
 def PermGroup (n : ℕ) := Equiv.Perm (Fin n)
 
-instance {n : ℕ} : Group (PermGroup n) := by
-  simp [PermGroup]
-  infer_instance
+instance {n : ℕ} : Group (PermGroup n) := Equiv.Perm.permGroup
 
 section Charges
 
@@ -74,12 +72,12 @@ def FamilyPermutations (n : ℕ) : ACCSystemGroupAction (PureU1 n) where
   rep := permCharges
   linearInvariant := by
     intro i
-    simp at i
+    simp only [PureU1_numberLinear] at i
     match i with
     | 0 => exact accGrav_invariant
   quadInvariant := by
     intro i
-    simp at i
+    simp only [PureU1_numberQuadratic] at i
     exact Fin.elim0 i
   cubicInvariant := accCube_invariant
 
@@ -134,7 +132,7 @@ lemma pairSwap_inv_snd {n : ℕ} (i j : Fin n) : (pairSwap i j).invFun j = i :=
 
 lemma pairSwap_other {n : ℕ} (i j k : Fin n) (hik : i ≠ k) (hjk : j ≠ k) :
     (pairSwap i j).toFun k = k := by
-  simp [pairSwap]
+  simp only [pairSwap, Equiv.toFun_as_coe, Equiv.coe_fn_mk]
   split
   · rename_i h
     exact False.elim (hik (id (Eq.symm h)))
@@ -207,8 +205,8 @@ lemma permTwo_snd : (permTwo hij hij').toFun j' = j := by
   have ht := Equiv.extendSubtype_apply_of_mem
     ((permTwoInj hij').toEquivRange.symm.trans
     (permTwoInj hij).toEquivRange) j' (permTwoInj_snd hij')
-  simp at ht
-  simp [ht, permTwoInj_snd_apply]
+  simp only [Equiv.trans_apply, Function.Embedding.toEquivRange_apply] at ht
+  simp only [Equiv.toFun_as_coe, ht, permTwoInj_snd_apply, Fin.isValue]
   rfl
 
 end permTwo
@@ -266,8 +264,8 @@ lemma permThree_fst : (permThree hij hjk hik hij' hjk' hik').toFun i' = i := by
   have ht := Equiv.extendSubtype_apply_of_mem
     ((permThreeInj hij' hjk' hik').toEquivRange.symm.trans
     (permThreeInj hij hjk hik).toEquivRange) i' (permThreeInj_fst hij' hjk' hik')
-  simp at ht
-  simp [ht, permThreeInj_fst_apply]
+  simp only [Equiv.trans_apply, Function.Embedding.toEquivRange_apply] at ht
+  simp only [Equiv.toFun_as_coe, ht, permThreeInj_fst_apply, Fin.isValue]
   rfl
 
 lemma permThree_snd : (permThree hij hjk hik hij' hjk' hik').toFun j' = j := by
@@ -275,8 +273,8 @@ lemma permThree_snd : (permThree hij hjk hik hij' hjk' hik').toFun j' = j := by
   have ht := Equiv.extendSubtype_apply_of_mem
     ((permThreeInj hij' hjk' hik').toEquivRange.symm.trans
     (permThreeInj hij hjk hik).toEquivRange) j' (permThreeInj_snd hij' hjk' hik')
-  simp at ht
-  simp [ht, permThreeInj_snd_apply]
+  simp only [Equiv.trans_apply, Function.Embedding.toEquivRange_apply] at ht
+  simp only [Equiv.toFun_as_coe, ht, permThreeInj_snd_apply, Fin.isValue]
   rfl
 
 lemma permThree_thd : (permThree hij hjk hik hij' hjk' hik').toFun k' = k := by
@@ -284,8 +282,8 @@ lemma permThree_thd : (permThree hij hjk hik hij' hjk' hik').toFun k' = k := by
   have ht := Equiv.extendSubtype_apply_of_mem
     ((permThreeInj hij' hjk' hik').toEquivRange.symm.trans
     (permThreeInj hij hjk hik).toEquivRange) k' (permThreeInj_thd hij' hjk' hik')
-  simp at ht
-  simp [ht, permThreeInj_thd_apply]
+  simp only [Equiv.trans_apply, Function.Embedding.toEquivRange_apply] at ht
+  simp only [Equiv.toFun_as_coe, ht, permThreeInj_thd_apply, Fin.isValue]
   rfl
 
 end permThree
@@ -299,7 +297,7 @@ lemma Prop_two (P : ℚ × ℚ → Prop) {S : (PureU1 n).LinSols}
   intro i j hij
   have h1 := h (permTwo hij hab).symm
   rw [FamilyPermutations_anomalyFreeLinear_apply, FamilyPermutations_anomalyFreeLinear_apply] at h1
-  simp at h1
+  simp only [Equiv.invFun_as_coe, Equiv.symm_symm] at h1
   change P
     (S.val ((permTwo hij hab).toFun a),
     S.val ((permTwo hij hab).toFun b)) at h1
@@ -317,7 +315,7 @@ lemma Prop_three (P : ℚ × ℚ × ℚ → Prop) {S : (PureU1 n).LinSols}
   have h1 := h (permThree hij hjk hik hab hbc hac).symm
   rw [FamilyPermutations_anomalyFreeLinear_apply, FamilyPermutations_anomalyFreeLinear_apply,
     FamilyPermutations_anomalyFreeLinear_apply] at h1
-  simp at h1
+  simp only [Equiv.invFun_as_coe, Equiv.symm_symm] at h1
   change P
     (S.val ((permThree hij hjk hik hab hbc hac).toFun a),
     S.val ((permThree hij hjk hik hab hbc hac).toFun b),
diff --git a/HepLean/AnomalyCancellation/PureU1/Sorts.lean b/HepLean/AnomalyCancellation/PureU1/Sorts.lean
index fa3c36a..426a056 100644
--- a/HepLean/AnomalyCancellation/PureU1/Sorts.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Sorts.lean
@@ -53,7 +53,7 @@ lemma sort_zero {n : ℕ} (S : (PureU1 n).Charges) (hS : sort S = 0) : S = 0 :=
     rfl
   have hi := hj ((Tuple.sort S).invFun i)
   rw [sort_apply] at hi
-  simp at hi
+  simp only [PureU1_numberCharges, Equiv.invFun_as_coe, Equiv.apply_symm_apply] at hi
   rw [hi]
   rfl
 
diff --git a/HepLean/AnomalyCancellation/SM/Basic.lean b/HepLean/AnomalyCancellation/SM/Basic.lean
index f4c1820..b0ab436 100644
--- a/HepLean/AnomalyCancellation/SM/Basic.lean
+++ b/HepLean/AnomalyCancellation/SM/Basic.lean
@@ -87,13 +87,15 @@ def accGrav : (SMCharges n).Charges →ₗ[ℚ] ℚ where
   map_add' S T := by
     simp only
     repeat rw [map_add]
-    simp [Pi.add_apply, mul_add]
+    simp only [SMSpecies_numberCharges, ACCSystemCharges.chargesAddCommMonoid_add, toSpecies_apply,
+      Fin.isValue, mul_add]
     repeat erw [Finset.sum_add_distrib]
     ring
   map_smul' a S := by
     simp only
     repeat erw [map_smul]
-    simp [HSMul.hSMul, SMul.smul]
+    simp only [SMSpecies_numberCharges, HSMul.hSMul, SMul.smul, toSpecies_apply, Fin.isValue,
+      eq_ratCast, Rat.cast_eq_id, id_eq]
     repeat erw [Finset.sum_add_distrib]
     repeat erw [← Finset.mul_sum]
     --rw [show Rat.cast a = a from rfl]
@@ -117,13 +119,15 @@ def accSU2 : (SMCharges n).Charges →ₗ[ℚ] ℚ where
   map_add' S T := by
     simp only
     repeat rw [map_add]
-    simp [Pi.add_apply, mul_add]
+    simp only [SMSpecies_numberCharges, ACCSystemCharges.chargesAddCommMonoid_add, toSpecies_apply,
+      Fin.isValue, mul_add]
     repeat erw [Finset.sum_add_distrib]
     ring
   map_smul' a S := by
     simp only
     repeat erw [map_smul]
-    simp [HSMul.hSMul, SMul.smul]
+    simp only [SMSpecies_numberCharges, HSMul.hSMul, SMul.smul, toSpecies_apply, Fin.isValue,
+      eq_ratCast, Rat.cast_eq_id, id_eq]
     repeat erw [Finset.sum_add_distrib]
     repeat erw [← Finset.mul_sum]
     --rw [show Rat.cast a = a from rfl]
@@ -146,13 +150,15 @@ def accSU3 : (SMCharges n).Charges →ₗ[ℚ] ℚ where
   map_add' S T := by
     simp only
     repeat rw [map_add]
-    simp [Pi.add_apply, mul_add]
+    simp only [SMSpecies_numberCharges, ACCSystemCharges.chargesAddCommMonoid_add, toSpecies_apply,
+      Fin.isValue, mul_add]
     repeat erw [Finset.sum_add_distrib]
     ring
   map_smul' a S := by
     simp only
     repeat erw [map_smul]
-    simp [HSMul.hSMul, SMul.smul]
+    simp only [SMSpecies_numberCharges, HSMul.hSMul, SMul.smul, toSpecies_apply, Fin.isValue,
+      eq_ratCast, Rat.cast_eq_id, id_eq]
     repeat erw [Finset.sum_add_distrib]
     repeat erw [← Finset.mul_sum]
     --rw [show Rat.cast a = a from rfl]
@@ -177,16 +183,17 @@ def accYY : (SMCharges n).Charges →ₗ[ℚ] ℚ where
   map_add' S T := by
     simp only
     repeat rw [map_add]
-    simp [Pi.add_apply, mul_add]
+    simp only [SMSpecies_numberCharges, ACCSystemCharges.chargesAddCommMonoid_add, toSpecies_apply,
+      Fin.isValue, mul_add]
     repeat erw [Finset.sum_add_distrib]
     ring
   map_smul' a S := by
     simp only
     repeat erw [map_smul]
-    simp [HSMul.hSMul, SMul.smul]
+    simp only [SMSpecies_numberCharges, HSMul.hSMul, SMul.smul, toSpecies_apply, Fin.isValue,
+      eq_ratCast, Rat.cast_eq_id, id_eq]
     repeat erw [Finset.sum_add_distrib]
     repeat erw [← Finset.mul_sum]
-    --rw [show Rat.cast a = a from rfl]
     ring
 
 /-- Extensionality lemma for `accYY`. -/
@@ -215,7 +222,7 @@ def quadBiLin : BiLinearSymm (SMCharges n).Charges := BiLinearSymm.mk₂
     apply Fintype.sum_congr
     intro i
     repeat erw [map_smul]
-    simp [HSMul.hSMul, SMul.smul]
+    simp only [HSMul.hSMul, SMul.smul, toSpecies_apply, Fin.isValue, neg_mul, one_mul]
     ring)
   (by
     intro S1 S2 T
diff --git a/HepLean/AnomalyCancellation/SM/FamilyMaps.lean b/HepLean/AnomalyCancellation/SM/FamilyMaps.lean
index 0d14dfe..ac3a282 100644
--- a/HepLean/AnomalyCancellation/SM/FamilyMaps.lean
+++ b/HepLean/AnomalyCancellation/SM/FamilyMaps.lean
@@ -68,7 +68,8 @@ def speciesEmbed (m n : ℕ) :
       rfl
   map_smul' a S := by
     funext i
-    simp [HSMul.hSMul]
+    simp only [SMSpecies_numberCharges, HSMul.hSMul, ACCSystemCharges.chargesModule_smul,
+      eq_ratCast, Rat.cast_eq_id, id_eq]
     by_cases hi : i.val < m
     · erw [dif_pos hi, dif_pos hi]
     · erw [dif_neg hi, dif_neg hi]
diff --git a/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean b/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
index c58838b..790604b 100644
--- a/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
+++ b/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
@@ -95,20 +95,20 @@ lemma cubic (S : linearParameters) :
 lemma cubic_zero_Q'_zero (S : linearParameters) (hc : accCube (S.asCharges) = 0)
     (h : S.Q' = 0) : S.E' = 0 := by
   rw [cubic, h] at hc
-  simp at hc
-  exact hc
+  simpa using hc
 
 lemma cubic_zero_E'_zero (S : linearParameters) (hc : accCube (S.asCharges) = 0)
     (h : S.E' = 0) : S.Q' = 0 := by
   rw [cubic, h] at hc
-  simp at hc
+  simp only [neg_mul, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, add_zero] at hc
   have h1 : -(54 * S.Q' ^ 3) - 18 * S.Q' * S.Y ^ 2 = - 18 * (3 * S.Q' ^ 2 + S.Y ^ 2) * S.Q' := by
     ring
   rw [h1] at hc
-  simp at hc
+  simp only [neg_mul, neg_eq_zero, mul_eq_zero, OfNat.ofNat_ne_zero, false_or] at hc
   cases' hc with hc hc
   · have h2 := (add_eq_zero_iff_of_nonneg (by nlinarith) (sq_nonneg S.Y)).mp hc
-    simp at h2
+    simp only [mul_eq_zero, OfNat.ofNat_ne_zero, ne_eq, not_false_eq_true, pow_eq_zero_iff,
+      false_or] at h2
     exact h2.1
   · exact hc
 
@@ -140,9 +140,13 @@ def bijection : linearParameters ≃ (SMNoGrav 1).LinSols where
     subst hj
     erw [speciesVal]
     have h1 := SU3Sol S
-    simp at h1
+    simp only [accSU3, SMSpecies_numberCharges, Finset.univ_unique, Fin.default_eq_zero,
+      Fin.isValue, toSpecies_apply, Nat.reduceMul, Finset.sum_singleton, Prod.mk_zero_zero,
+      LinearMap.coe_mk, AddHom.coe_mk] at h1
     have h2 := SU2Sol S
-    simp at h2
+    simp only [accSU2, SMSpecies_numberCharges, Finset.univ_unique, Fin.default_eq_zero,
+      Fin.isValue, toSpecies_apply, Nat.reduceMul, Finset.sum_singleton, Prod.mk_zero_zero,
+      LinearMap.coe_mk, AddHom.coe_mk] at h2
     match i with
     | 0 => rfl
     | 1 =>
@@ -282,14 +286,14 @@ lemma cubic_v_or_w_zero (S : linearParametersQENeqZero) (h : accCube (bijection
   have h1 : (-1)^3 = (-1 : ℚ) := by rfl
   rw [← h1] at h
   by_contra hn
-  simp [not_or] at hn
+  rw [not_or] at hn
   have h2 := FLTThree S.v S.w (-1) hn.1 hn.2 (Ne.symm (ne_of_beq_false (by rfl)))
   exact h2 h
 
 lemma cubic_v_zero (S : linearParametersQENeqZero) (h : accCube (bijection S).1.val = 0)
     (hv : S.v = 0) : S.w = -1 := by
   rw [S.cubic, hv] at h
-  simp at h
+  simp only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, zero_add] at h
   have h' : (S.w + 1) * (1 * S.w * S.w + (-1) * S.w + 1) = 0 := by
     ring_nf
     exact add_eq_zero_iff_neg_eq.mpr (id (Eq.symm h))
@@ -307,7 +311,7 @@ lemma cubic_v_zero (S : linearParametersQENeqZero) (h : accCube (bijection S).1.
 lemma cube_w_zero (S : linearParametersQENeqZero) (h : accCube (bijection S).1.val = 0)
     (hw : S.w = 0) : S.v = -1 := by
   rw [S.cubic, hw] at h
-  simp at h
+  simp only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, add_zero] at h
   have h' : (S.v + 1) * (1 * S.v * S.v + (-1) * S.v + 1) = 0 := by
     ring_nf
     exact add_eq_zero_iff_neg_eq.mpr (id (Eq.symm h))
@@ -327,10 +331,8 @@ lemma cube_w_v (S : linearParametersQENeqZero) (h : accCube (bijection S).1.val
     (S.v = -1 ∧ S.w = 0) ∨ (S.v = 0 ∧ S.w = -1) := by
   have h' := cubic_v_or_w_zero S h FLTThree
   cases' h' with hx hx
-  · simp [hx]
-    exact cubic_v_zero S h hx
-  · simp [hx]
-    exact cube_w_zero S h hx
+  · simpa [hx] using cubic_v_zero S h hx
+  · simpa [hx] using cube_w_zero S h hx
 
 lemma grav (S : linearParametersQENeqZero) : accGrav (bijection S).1.val = 0 ↔ S.v + S.w = -1 := by
   erw [linearParameters.grav]
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean
index e864dac..ecbff0c 100644
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean
@@ -48,7 +48,7 @@ lemma exists_plane_exists_basis {n : ℕ} (hE : ExistsPlane n) :
   have h3 : ∀ i, g (Sum.inl i) = 0 := hB1 (fun i => (g (Sum.inl i))) h2
   rw [h2] at hg
   have h4 : ∀ i, - g (Sum.inr i) = 0 := hE1 (fun i => (- g (Sum.inr i))) hg.symm
-  simp at h4
+  simp only [neg_eq_zero] at h4
   intro i
   match i with
   | Sum.inl i => exact h3 i
@@ -57,7 +57,7 @@ lemma exists_plane_exists_basis {n : ℕ} (hE : ExistsPlane n) :
 theorem plane_exists_dim_le_7 {n : ℕ} (hn : ExistsPlane n) : n ≤ 7 := by
   obtain ⟨B, hB⟩ := exists_plane_exists_basis hn
   have h1 := LinearIndependent.fintype_card_le_finrank hB
-  simp at h1
+  simp only [Fintype.card_sum, Fintype.card_fin] at h1
   rw [show FiniteDimensional.finrank ℚ (PlusU1 3).Charges = 18 from
     FiniteDimensional.finrank_fin_fun ℚ] at h1
   exact Nat.le_of_add_le_add_left h1
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSolToSol.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSolToSol.lean
index 8afbf9d..c334b3a 100644
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSolToSol.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSolToSol.lean
@@ -100,7 +100,8 @@ def quadSolToSolInv {n : ℕ} : (PlusU1 n).Sols → (PlusU1 n).QuadSols × ℚ 
 
 lemma quadSolToSolInv_1 (S : (PlusU1 n).Sols) :
     (quadSolToSolInv S).1 = S.1 := by
-  simp [quadSolToSolInv]
+  simp only [quadSolToSolInv, α₁, BL_val, SMνACCs.cubeTriLin_toFun_apply_apply, Fin.isValue,
+    neg_mul, neg_eq_zero, mul_eq_zero, OfNat.ofNat_ne_zero, false_or]
   split <;> rfl
 
 lemma quadSolToSolInv_α₁_α₂_zero (S : (PlusU1 n).Sols) (h : α₁ S.1 = 0) :
diff --git a/HepLean/FlavorPhysics/CKMMatrix/Invariants.lean b/HepLean/FlavorPhysics/CKMMatrix/Invariants.lean
index 9aaa3b3..afe9dad 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/Invariants.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/Invariants.lean
@@ -35,7 +35,8 @@ lemma jarlskogℂCKM_equiv (V U : CKMMatrix) (h : V ≈ U) :
   rw [h]
   simp only [jarlskogℂCKM, Fin.isValue, phaseShiftApply.ub,
   phaseShiftApply.us, phaseShiftApply.cb, phaseShiftApply.cs]
-  simp [← exp_conj, conj_ofReal, exp_add, exp_neg]
+  simp only [exp_add, Fin.isValue, _root_.map_mul, ← exp_conj, conj_ofReal, conj_I, mul_neg,
+    exp_neg]
   have ha : cexp (↑a * I) ≠ 0 := exp_ne_zero _
   have hb : cexp (↑b * I) ≠ 0 := exp_ne_zero _
   have hf : cexp (↑f * I) ≠ 0 := exp_ne_zero _