From 1651b265e7a4cb271bcca50a2e3e0a17ea814220 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Sat, 12 Oct 2024 07:57:35 +0000
Subject: [PATCH] refactor: Simp lemmas

---
 HepLean/AnomalyCancellation/PureU1/Basic.lean | 10 +--
 .../PureU1/Even/LineInCubic.lean              |  7 ++-
 .../PureU1/LineInPlaneCond.lean               | 16 +++--
 .../PureU1/Odd/Parameterization.lean          | 19 +++---
 .../SMNu/PlusU1/HyperCharge.lean              |  4 +-
 HepLean/FlavorPhysics/CKMMatrix/Basic.lean    |  4 +-
 .../FlavorPhysics/CKMMatrix/PhaseFreedom.lean | 63 +++++++++++--------
 .../FlavorPhysics/CKMMatrix/Relations.lean    |  3 +-
 HepLean/FlavorPhysics/CKMMatrix/Rows.lean     | 19 +++---
 .../StandardParameterization/Basic.lean       | 11 ++--
 .../StandardModel/HiggsBoson/Potential.lean   | 10 +--
 HepLean/Tensors/ComplexLorentz/ColorFun.lean  | 24 +++++--
 .../ComplexLorentz/ContrNatTransform.lean     |  3 +-
 HepLean/Tensors/ComplexLorentz/Examples.lean  |  3 +-
 HepLean/Tensors/OverColor/Basic.lean          |  4 +-
 HepLean/Tensors/Tree/Elab.lean                |  2 -
 16 files changed, 116 insertions(+), 86 deletions(-)

diff --git a/HepLean/AnomalyCancellation/PureU1/Basic.lean b/HepLean/AnomalyCancellation/PureU1/Basic.lean
index 023c70c..4be184b 100644
--- a/HepLean/AnomalyCancellation/PureU1/Basic.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Basic.lean
@@ -31,7 +31,7 @@ def accGrav (n : ℕ) : ((PureU1Charges n).Charges →ₗ[ℚ] ℚ) where
   toFun S := ∑ i : Fin n, S i
   map_add' S T := Finset.sum_add_distrib
   map_smul' a S := by
-    simp [HSMul.hSMul, SMul.smul]
+    simp only [HSMul.hSMul, SMul.smul, eq_ratCast, Rat.cast_eq_id, id_eq]
     rw [← Finset.mul_sum]
 
 /-- The symmetric trilinear form used to define the cubic anomaly. -/
@@ -40,7 +40,7 @@ def accCubeTriLinSymm {n : ℕ} : TriLinearSymm (PureU1Charges n).Charges := Tri
   (fun S => ∑ i, S.1 i * S.2.1 i * S.2.2 i)
   (by
     intro a S L T
-    simp [HSMul.hSMul]
+    simp only [PureU1Charges_numberCharges, HSMul.hSMul, ACCSystemCharges.chargesModule_smul]
     rw [Finset.mul_sum]
     apply Fintype.sum_congr
     intro i
@@ -108,7 +108,7 @@ open BigOperators
 lemma pureU1_linear {n : ℕ} (S : (PureU1 n.succ).LinSols) :
     ∑ i, S.val i = 0 := by
   have hS := S.linearSol
-  simp at hS
+  simp only [succ_eq_add_one, PureU1_numberLinear, PureU1_linearACCs] at hS
   exact hS 0
 
 lemma pureU1_cube {n : ℕ} (S : (PureU1 n.succ).Sols) :
@@ -120,7 +120,7 @@ lemma pureU1_cube {n : ℕ} (S : (PureU1 n.succ).Sols) :
 lemma pureU1_last {n : ℕ} (S : (PureU1 n.succ).LinSols) :
     S.val (Fin.last n) = - ∑ i : Fin n, S.val i.castSucc := by
   have hS := pureU1_linear S
-  simp at hS
+  simp only [succ_eq_add_one, PureU1_numberCharges] at hS
   rw [Fin.sum_univ_castSucc] at hS
   linear_combination hS
 
@@ -134,7 +134,7 @@ lemma pureU1_anomalyFree_ext {n : ℕ} {S T : (PureU1 n.succ).LinSols}
     obtain ⟨j, hj⟩ := hiCast
     rw [← hj]
     exact h j
-  · simp at hi
+  · simp only [succ_eq_add_one, PureU1_numberCharges, ne_eq, Decidable.not_not] at hi
     rw [hi, pureU1_last, pureU1_last]
     simp only [neg_inj]
     apply Finset.sum_congr
diff --git a/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean b/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean
index 24591e5..ccec70b 100644
--- a/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean
@@ -113,7 +113,7 @@ lemma P_P_P!_accCube' {S : (PureU1 (2 * n.succ.succ)).LinSols}
   have h1 := Pa_δ!₄ f g
   have h2 := Pa_δ!₁ f g (Fin.last n)
   have h3 := Pa_δ!₂ f g (Fin.last n)
-  simp at h1 h2 h3
+  simp only [Fin.succ_last, Nat.succ_eq_add_one] at h1 h2 h3
   have hl : f (Fin.succ (Fin.last n)) = - Pa f g δ!₄ := by
     simp_all only [Fin.succ_last, neg_neg]
   erw [hl] at h2
@@ -133,7 +133,7 @@ lemma lineInCubicPerm_last_cond {S : (PureU1 (2 * n.succ.succ)).LinSols}
   obtain ⟨g, f, hfg⟩ := span_basis S
   have h1 := lineInCubicPerm_swap LIC (Fin.last n) g f hfg
   rw [P_P_P!_accCube' g f hfg] at h1
-  simp at h1
+  simp only [Nat.succ_eq_add_one, neg_add_rev, mul_eq_zero] at h1
   cases h1 <;> rename_i h1
   · apply Or.inl
     linear_combination h1
@@ -148,7 +148,8 @@ lemma lineInCubicPerm_last_perm {S : (PureU1 (2 * n.succ.succ)).LinSols}
     δ!₄ ?_ ?_ ?_ ?_
   · simp [Fin.ext_iff, δ!₂, δ!₁]
   · simp [Fin.ext_iff, δ!₂, δ!₄]
-  · simp [Fin.ext_iff, δ!₁, δ!₄]
+  · simp only [Nat.succ_eq_add_one, δ!₁, δ!₄, Fin.isValue, ne_eq, Fin.ext_iff, Fin.coe_cast,
+    Fin.coe_natAdd, Fin.coe_castAdd, Fin.val_last, Fin.coe_fin_one, add_zero, add_right_inj]
     omega
   · exact fun M => lineInCubicPerm_last_cond (lineInCubicPerm_permute LIC M)
 
diff --git a/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean b/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean
index dcc7205..a37070f 100644
--- a/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean
+++ b/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean
@@ -58,14 +58,18 @@ lemma lineInPlaneCond_eq_last' {S : (PureU1 (n.succ.succ)).LinSols} (hS : LineIn
   erw [sq_eq_sq_iff_eq_or_eq_neg] at h
   rw [LineInPlaneCond] at hS
   simp only [LineInPlaneProp] at hS
-  simp [not_or] at h
+  simp only [Nat.succ_eq_add_one, Fin.succ_last, not_or] at h
   have h1 (i : Fin n) : S.val i.castSucc.castSucc =
       - (S.val ((Fin.last n).castSucc) + (S.val ((Fin.last n).succ))) / 2 := by
     have h1S := hS (Fin.last n).castSucc ((Fin.last n).succ) i.castSucc.castSucc
-      (by simp; rw [Fin.ext_iff]; exact Nat.ne_add_one ↑(Fin.last n).castSucc)
-      (by simp; rw [Fin.ext_iff]; simp; omega)
-      (by simp; rw [Fin.ext_iff]; simp; omega)
-    simp_all
+      (by simp only [Fin.ext_iff, Nat.succ_eq_add_one, Fin.succ_last, ne_eq]
+          exact Nat.ne_add_one ↑(Fin.last n).castSucc)
+      (by simp only [Nat.succ_eq_add_one, Fin.succ_last, ne_eq, Fin.ext_iff, Fin.val_last,
+        Fin.coe_castSucc]
+          omega)
+      (by simp only [Nat.succ_eq_add_one, ne_eq, Fin.ext_iff, Fin.coe_castSucc, Fin.val_last]
+          omega)
+    simp_all only [Nat.succ_eq_add_one, ne_eq, Fin.succ_last, false_or, neg_add_rev]
     field_simp
     linear_combination h1S
   have h2 := pureU1_last S
@@ -152,7 +156,7 @@ lemma linesInPlane_four (S : (PureU1 4).Sols) (hS : LineInPlaneCond S.1.1) :
       rw [h4, h5] at hcube
       have h6 : S.val (3 : Fin 4) ^ 3 = 0 := by
         linear_combination -1 * hcube / 24
-      simp at h6
+      simp only [Fin.isValue, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, pow_eq_zero_iff] at h6
       simp_all
 
 lemma linesInPlane_eq_sq_four {S : (PureU1 4).Sols}
diff --git a/HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean b/HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean
index 67c139a..c3108ae 100644
--- a/HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean
@@ -60,7 +60,7 @@ lemma parameterizationCharge_cube (g f : Fin n → ℚ) (a : ℚ) :
 /-- Given a `g f : Fin n → ℚ` and a `a : ℚ` we form a solution. -/
 def parameterization (g f : Fin n → ℚ) (a : ℚ) :
     (PureU1 (2 * n + 1)).Sols :=
-  ⟨⟨parameterizationAsLinear g f a, by intro i; simp at i; exact Fin.elim0 i⟩,
+  ⟨⟨parameterizationAsLinear g f a, fun i => Fin.elim0 i⟩,
   parameterizationCharge_cube g f a⟩
 
 lemma anomalyFree_param {S : (PureU1 (2 * n + 1)).Sols}
@@ -125,13 +125,10 @@ theorem generic_case {S : (PureU1 (2 * n.succ + 1)).Sols} (h : GenericCase S) :
   apply ACCSystem.Sols.ext
   rw [parameterizationAsLinear_val]
   change S.val = _ • (_ • P g + _• P! f)
-  rw [anomalyFree_param _ _ hS]
-  rw [neg_neg, ← smul_add, smul_smul, inv_mul_cancel₀, one_smul]
+  rw [anomalyFree_param _ _ hS, neg_neg, ← smul_add, smul_smul, inv_mul_cancel₀, one_smul]
   · exact hS
-  · have h := h g f hS
-    rw [anomalyFree_param _ _ hS] at h
-    simp at h
-    exact h
+  · simpa only [Nat.succ_eq_add_one, accCubeTriLinSymm_toFun_apply_apply, ne_eq,
+      anomalyFree_param _ _ hS, neg_eq_zero] using h g f hS
 
 lemma special_case_lineInCubic {S : (PureU1 (2 * n.succ + 1)).Sols}
     (h : SpecialCase S) :
@@ -139,15 +136,13 @@ lemma special_case_lineInCubic {S : (PureU1 (2 * n.succ + 1)).Sols}
   intro g f hS a b
   erw [TriLinearSymm.toCubic_add]
   rw [HomogeneousCubic.map_smul, HomogeneousCubic.map_smul]
-  erw [P_accCube]
-  erw [P!_accCube]
+  erw [P_accCube, P!_accCube]
   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/SMNu/PlusU1/HyperCharge.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.lean
index 4c2d0c1..dd5a6fb 100644
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.lean
@@ -33,7 +33,7 @@ def Y₁ : (PlusU1 1).Sols where
     | (5 : Fin 6) => 0
   linearSol := by
     intro i
-    simp at i
+    simp only [PlusU1_numberLinear] at i
     match i with
     | 0 => rfl
     | 1 => rfl
@@ -41,7 +41,7 @@ def Y₁ : (PlusU1 1).Sols where
     | 3 => rfl
   quadSol := by
     intro i
-    simp at i
+    simp only [PlusU1_numberQuadratic] at i
     match i with
     | 0 => rfl
   cubicSol := by rfl
diff --git a/HepLean/FlavorPhysics/CKMMatrix/Basic.lean b/HepLean/FlavorPhysics/CKMMatrix/Basic.lean
index 2fd035a..3f8a423 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/Basic.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/Basic.lean
@@ -116,8 +116,8 @@ lemma phaseShiftRelation_equiv : Equivalence PhaseShiftRelation where
 def CKMMatrix : Type := unitaryGroup (Fin 3) ℂ
 
 lemma CKMMatrix_ext {U V : CKMMatrix} (h : U.val = V.val) : U = V := by
-  cases U; cases V
-  simp at h
+  cases U
+  cases V
   subst h
   rfl
 
diff --git a/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean b/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean
index e9a067c..c5a8d89 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean
@@ -62,7 +62,8 @@ lemma shift_ub_phase_zero {V : CKMMatrix} (h1 : u + b = - arg [V]ub) :
     simp only [Fin.isValue, ofReal_add]
     ring
   rw [h2, h1]
-  simp
+  simp only [Fin.isValue, add_neg_cancel, ofReal_zero, zero_mul, exp_zero, mul_one, VubAbs,
+    ofReal_inj]
   rfl
 
 lemma shift_cs_phase_zero {V : CKMMatrix} (h1 : c + s = - arg [V]cs) :
@@ -71,10 +72,11 @@ lemma shift_cs_phase_zero {V : CKMMatrix} (h1 : c + s = - arg [V]cs) :
   rw [← abs_mul_exp_arg_mul_I [V]cs]
   rw [mul_comm, mul_assoc, ← exp_add]
   have h2 : ↑(arg [V]cs) * I + (↑c * I + ↑s * I) = ↑(arg [V]cs + (c + s)) * I := by
-    simp [add_assoc]
+    simp only [Fin.isValue, ofReal_add]
     ring
   rw [h2, h1]
-  simp
+  simp only [Fin.isValue, add_neg_cancel, ofReal_zero, zero_mul, exp_zero, mul_one, VcsAbs,
+    ofReal_inj]
   rfl
 
 lemma shift_cb_phase_zero {V : CKMMatrix} (h1 : c + b = - arg [V]cb) :
@@ -83,10 +85,11 @@ lemma shift_cb_phase_zero {V : CKMMatrix} (h1 : c + b = - arg [V]cb) :
   rw [← abs_mul_exp_arg_mul_I [V]cb]
   rw [mul_comm, mul_assoc, ← exp_add]
   have h2 : ↑(arg [V]cb) * I + (↑c * I + ↑b * I) = ↑(arg [V]cb + (c + b)) * I := by
-    simp [add_assoc]
+    simp only [Fin.isValue, ofReal_add]
     ring
   rw [h2, h1]
-  simp
+  simp only [Fin.isValue, add_neg_cancel, ofReal_zero, zero_mul, exp_zero, mul_one, VcbAbs,
+    ofReal_inj]
   rfl
 
 lemma shift_tb_phase_zero {V : CKMMatrix} (h1 : t + b = - arg [V]tb) :
@@ -95,10 +98,11 @@ lemma shift_tb_phase_zero {V : CKMMatrix} (h1 : t + b = - arg [V]tb) :
   rw [← abs_mul_exp_arg_mul_I [V]tb]
   rw [mul_comm, mul_assoc, ← exp_add]
   have h2 : ↑(arg [V]tb) * I + (↑t * I + ↑b * I) = ↑(arg [V]tb + (t + b)) * I := by
-    simp [add_assoc]
+    simp only [Fin.isValue, ofReal_add]
     ring
   rw [h2, h1]
-  simp
+  simp only [Fin.isValue, add_neg_cancel, ofReal_zero, zero_mul, exp_zero, mul_one, VtbAbs,
+    ofReal_inj]
   rfl
 
 lemma shift_cd_phase_pi {V : CKMMatrix} (h1 : c + d = Real.pi - arg [V]cd) :
@@ -110,7 +114,8 @@ lemma shift_cd_phase_pi {V : CKMMatrix} (h1 : c + d = Real.pi - arg [V]cd) :
     simp [add_assoc]
     ring
   rw [h2, h1]
-  simp
+  simp only [Fin.isValue, add_sub_cancel, exp_pi_mul_I, mul_neg, mul_one, VcdAbs, neg_inj,
+    ofReal_inj]
   rfl
 
 lemma shift_cross_product_phase_zero {V : CKMMatrix} {τ : ℝ}
@@ -120,33 +125,35 @@ lemma shift_cross_product_phase_zero {V : CKMMatrix} {τ : ℝ}
   change _ = phaseShiftApply.ucCross _ _ _ _ _ _ _
   funext i
   fin_cases i
-  · simp
+  · simp only [Fin.zero_eta, Fin.isValue]
     rw [phaseShiftApply.ucCross_fst]
     simp [tRow, phaseShiftApply.td]
     have hτ0 := congrFun hτ 0
-    simp [tRow] at hτ0
+    simp only [Fin.isValue, Pi.smul_apply, smul_eq_mul, tRow, cons_val_zero] at hτ0
     rw [← hτ0]
     rw [← mul_assoc, ← exp_add, h1]
     congr 2
     simp only [ofReal_sub, ofReal_neg]
     ring
-  · simp
+  · simp only [Fin.mk_one, Fin.isValue]
     rw [phaseShiftApply.ucCross_snd]
-    simp [tRow, phaseShiftApply.ts]
+    simp only [tRow, Fin.isValue, phaseShiftApply_coe, phaseShiftApply.ts, cons_val_one, head_cons,
+      neg_mul]
     have hτ0 := congrFun hτ 1
-    simp [tRow] at hτ0
+    simp only [Fin.isValue, Pi.smul_apply, smul_eq_mul, tRow, cons_val_one, head_cons] at hτ0
     rw [← hτ0]
     rw [← mul_assoc, ← exp_add, h1]
     congr 2
     simp only [ofReal_sub, ofReal_neg]
     ring
-  · simp
+  · simp only [Fin.reduceFinMk, Fin.isValue]
     rw [phaseShiftApply.ucCross_thd]
-    simp [tRow, phaseShiftApply.tb]
+    simp only [tRow, Fin.isValue, phaseShiftApply_coe, phaseShiftApply.tb, cons_val_two,
+      Nat.succ_eq_add_one, Nat.reduceAdd, tail_cons, head_cons, neg_mul]
     have hτ0 := congrFun hτ 2
-    simp [tRow] at hτ0
-    rw [← hτ0]
-    rw [← mul_assoc, ← exp_add, h1]
+    simp only [Fin.isValue, Pi.smul_apply, smul_eq_mul, tRow, cons_val_two, Nat.succ_eq_add_one,
+      Nat.reduceAdd, tail_cons, head_cons] at hτ0
+    rw [← hτ0, ← mul_assoc, ← exp_add, h1]
     congr 2
     simp only [ofReal_sub, ofReal_neg]
     ring
@@ -271,21 +278,21 @@ lemma ubOnePhaseCond_hold_up_to_equiv_of_ub_one {V : CKMMatrix} (hb : ¬ ([V]ud
   apply And.intro
   · exact phaseShiftApply.equiv _ _ _ _ _ _ _
   · apply And.intro
-    · simp [not_or] at hb
+    · simp only [Fin.isValue, ne_eq, not_or, Decidable.not_not] at hb
       have h1 : VudAbs ⟦U⟧ = 0 := by
         rw [hUV]
         simp [VAbs, hb]
-      simp [VAbs] at h1
+      simp only [VudAbs, VAbs, VAbs', Fin.isValue, Quotient.lift_mk, map_eq_zero] at h1
       exact h1
     apply And.intro
-    · simp [not_or] at hb
+    · simp only [Fin.isValue, ne_eq, not_or, Decidable.not_not] at hb
       have h1 : VusAbs ⟦U⟧ = 0 := by
         rw [hUV]
         simp [VAbs, hb]
       simp [VAbs] at h1
       exact h1
     apply And.intro
-    · simp [not_or] at hb
+    · simp only [Fin.isValue, ne_eq, not_or, Decidable.not_not] at hb
       have h3 := cb_eq_zero_of_ud_us_zero hb
       have h1 : VcbAbs ⟦U⟧ = 0 := by
         rw [hUV]
@@ -325,7 +332,8 @@ lemma cd_of_fstRowThdColRealCond {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠
     exact hV.2.2.2.2
   rw [cd_of_ud_us_ub_cb_tb hb hτ]
   rw [hV.1, hV.2.1, hV.2.2.1, hV.2.2.2.1]
-  simp [sq, conj_ofReal]
+  simp only [Fin.isValue, VudAbs, VcbAbs, ofReal_zero, zero_mul, exp_zero, VtbAbs, conj_ofReal,
+    one_mul, VusAbs, neg_add_rev, normSq_ofReal, ofReal_mul, neg_mul, sq, VubAbs]
   have hx := Vabs_sq_add_neq_zero hb
   field_simp
   have h1 : conj [V]ub = VubAbs ⟦V⟧ * cexp (- arg [V]ub * I) := by
@@ -343,15 +351,16 @@ lemma cs_of_fstRowThdColRealCond {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠
   have hτ : [V]t = cexp ((0 : ℝ) * I) • (conj ([V]u) ×₃ conj ([V]c)) := by
     simp only [ofReal_zero, zero_mul, exp_zero, one_smul]
     exact hV.2.2.2.2
-  rw [cs_of_ud_us_ub_cb_tb hb hτ]
-  rw [hV.1, hV.2.1, hV.2.2.1, hV.2.2.2.1]
-  simp [sq, conj_ofReal]
+  rw [cs_of_ud_us_ub_cb_tb hb hτ, hV.1, hV.2.1, hV.2.2.1, hV.2.2.2.1]
+  simp only [Fin.isValue, VusAbs, neg_mul, VcbAbs, ofReal_zero, zero_mul, exp_zero, VtbAbs,
+    conj_ofReal, one_mul, VudAbs, normSq_ofReal, ofReal_mul, sq, VubAbs]
   have hx := Vabs_sq_add_neq_zero hb
   field_simp
   have h1 : conj [V]ub = VubAbs ⟦V⟧ * cexp (- arg [V]ub * I) := by
     nth_rewrite 1 [← abs_mul_exp_arg_mul_I [V]ub]
     rw [@RingHom.map_mul]
-    simp [conj_ofReal, ← exp_conj, VAbs]
+    simp only [Fin.isValue, conj_ofReal, ← exp_conj, _root_.map_mul, conj_I, mul_neg, VubAbs, VAbs,
+      VAbs', Quotient.lift_mk, neg_mul]
   rw [h1]
   ring_nf
 
diff --git a/HepLean/FlavorPhysics/CKMMatrix/Relations.lean b/HepLean/FlavorPhysics/CKMMatrix/Relations.lean
index 28e9d34..3ad2980 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/Relations.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/Relations.lean
@@ -30,7 +30,8 @@ lemma VAbs_sum_sq_row_eq_one (V : Quotient CKMMatrixSetoid) (i : Fin 3) :
   have hV := V.prop
   rw [mem_unitaryGroup_iff] at hV
   have ht := congrFun (congrFun hV i) i
-  simp [Matrix.mul_apply, Fin.sum_univ_three] at ht
+  simp only [mul_apply, star_apply, RCLike.star_def, Fin.sum_univ_three, Fin.isValue,
+    one_apply_eq] at ht
   rw [mul_conj, mul_conj, mul_conj] at ht
   repeat rw [← Complex.sq_abs] at ht
   rw [← ofReal_inj]
diff --git a/HepLean/FlavorPhysics/CKMMatrix/Rows.lean b/HepLean/FlavorPhysics/CKMMatrix/Rows.lean
index 39620ff..c124c2b 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/Rows.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/Rows.lean
@@ -308,21 +308,26 @@ def ucCross : Fin 3 → ℂ :=
 
 lemma ucCross_fst (V : CKMMatrix) : (ucCross V a b c d e f) 0 =
     cexp ((- a * I) + (- b * I) + (- e * I) + (- f * I)) * (conj [V]u ×₃ conj [V]c) 0 := by
-  simp [ucCross, crossProduct, Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue,
-    LinearMap.mk₂_apply, Pi.conj_apply, cons_val_zero, neg_mul, uRow, us, ub, cRow, cs, cb,
-    exp_add, exp_sub, ← exp_conj, conj_ofReal]
+  simp only [ucCross, crossProduct, Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, uRow,
+    phaseShiftApply_coe, us, exp_add, ub, cRow, cs, cb, LinearMap.mk₂_apply, Pi.conj_apply,
+    cons_val_one, head_cons, _root_.map_mul, ← exp_conj, conj_ofReal, conj_I, mul_neg, cons_val_two,
+    tail_cons, cons_val_zero, neg_mul]
   ring
 
 lemma ucCross_snd (V : CKMMatrix) : (ucCross V a b c d e f) 1 =
     cexp ((- a * I) + (- b * I) + (- d * I) + (- f * I)) * (conj [V]u ×₃ conj [V]c) 1 := by
-  simp [ucCross, crossProduct, uRow, us, ub, cRow, cs, cb, ud, cd, exp_add,
-    exp_sub, ← exp_conj, conj_ofReal]
+  simp only [ucCross, crossProduct, Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, uRow, ud,
+    exp_add, us, ub, cRow, cd, cs, cb, LinearMap.mk₂_apply, Pi.conj_apply, cons_val_one, head_cons,
+    _root_.map_mul, ← exp_conj, conj_ofReal, conj_I, mul_neg, cons_val_two, tail_cons,
+    cons_val_zero, neg_mul]
   ring
 
 lemma ucCross_thd (V : CKMMatrix) : (ucCross V a b c d e f) 2 =
     cexp ((- a * I) + (- b * I) + (- d * I) + (- e * I)) * (conj [V]u ×₃ conj [V]c) 2 := by
-  simp [ucCross, crossProduct, uRow, us, ub, cRow, cs, cb, ud, cd, exp_add, exp_sub,
-    ← exp_conj, conj_ofReal]
+  simp only [ucCross, crossProduct, Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, uRow, ud,
+    exp_add, us, ub, cRow, cd, cs, cb, LinearMap.mk₂_apply, Pi.conj_apply, cons_val_one, head_cons,
+    _root_.map_mul, ← exp_conj, conj_ofReal, conj_I, mul_neg, cons_val_two, tail_cons,
+    cons_val_zero, neg_mul]
   ring
 
 lemma uRow_mul (V : CKMMatrix) (a b c : ℝ) :
diff --git a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean
index e3b188b..5d0bac9 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean
@@ -47,7 +47,7 @@ lemma standParamAsMatrix_unitary (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) :
     empty_val', cons_val_fin_one, star_mul', RCLike.star_def, conj_ofReal, cons_val_one, head_cons,
     star_sub, star_neg, ← exp_conj, _root_.map_mul, conj_I, neg_mul, cons_val_two, tail_cons,
     head_fin_const]
-    simp [conj_ofReal]
+    simp only [ofReal_cos, ofReal_sin]
     rw [exp_neg]
     fin_cases i <;> simp
     · ring_nf
@@ -65,7 +65,7 @@ lemma standParamAsMatrix_unitary (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) :
   · simp only [Fin.mk_one, Fin.isValue, conjTranspose_apply, cons_val', cons_val_one, head_cons,
     empty_val', cons_val_fin_one, cons_val_zero, star_mul', RCLike.star_def, conj_ofReal, star_sub,
     ← exp_conj, _root_.map_mul, conj_I, neg_mul, cons_val_two, tail_cons, head_fin_const, star_neg]
-    simp [conj_ofReal]
+    simp only [ofReal_sin, ofReal_cos]
     rw [exp_neg]
     fin_cases i <;> simp
     · ring_nf
@@ -169,15 +169,16 @@ lemma VusVubVcdSq_eq (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) (h1 : 0 ≤ Rea
       neg_zero, Real.exp_zero, mul_one, _root_.sq_abs]
     rw [_root_.abs_of_nonneg h1, _root_.abs_of_nonneg h3, _root_.abs_of_nonneg h2,
       _root_.abs_of_nonneg h4]
-    simp [sq]
+    simp only [sq]
     ring_nf
     nth_rewrite 2 [Real.sin_sq θ₁₂]
     ring_nf
     field_simp
     ring
-  · simp at hx
+  · simp only [ne_eq, Decidable.not_not] at hx
     rw [hx]
-    simp
+    simp only [abs_zero, mul_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow,
+      zero_mul, add_zero, div_zero]
 
 open Invariant in
 lemma mulExpδ₁₃_eq (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) (h1 : 0 ≤ Real.sin θ₁₂)
diff --git a/HepLean/StandardModel/HiggsBoson/Potential.lean b/HepLean/StandardModel/HiggsBoson/Potential.lean
index d2eca21..938a4b3 100644
--- a/HepLean/StandardModel/HiggsBoson/Potential.lean
+++ b/HepLean/StandardModel/HiggsBoson/Potential.lean
@@ -62,7 +62,7 @@ def neg : Potential where
 
 @[simp]
 lemma toFun_neg (φ : HiggsField) (x : SpaceTime) : P.neg.toFun φ x = - P.toFun φ x := by
-  simp [neg, toFun]
+  simp only [toFun, neg, neg_neg, normSq, neg_mul, neg_add_rev]
   ring
 
 @[simp]
@@ -247,7 +247,8 @@ lemma neg_𝓵_sol_exists_iff (h𝓵 : P.𝓵 < 0) (c : ℝ) : (∃ φ x, P.toFu
 lemma pos_𝓵_sol_exists_iff (h𝓵 : 0 < P.𝓵) (c : ℝ) : (∃ φ x, P.toFun φ x = c) ↔ (P.μ2 < 0 ∧ 0 ≤ c) ∨
     (0 ≤ P.μ2 ∧ - P.μ2 ^ 2 / (4 * P.𝓵) ≤ c) := by
   have h1 := P.neg.neg_𝓵_sol_exists_iff (by simpa using h𝓵) (- c)
-  simp at h1
+  simp only [toFun_neg, neg_inj, μ2_neg, Left.neg_pos_iff, Left.neg_nonpos_iff, even_two,
+    Even.neg_pow, 𝓵_neg, mul_neg, neg_div_neg_eq] at h1
   rw [neg_le, neg_div'] at h1
   exact h1
 
@@ -310,7 +311,7 @@ lemma isBounded_of_𝓵_pos (h : 0 < P.𝓵) : P.IsBounded := by
   simp only [IsBounded]
   have h2 := P.pos_𝓵_quadDiscrim_zero_bound h
   by_contra hn
-  simp at hn
+  simp only [not_exists, not_forall, not_le] at hn
   obtain ⟨φ, x, hx⟩ := hn (-P.μ2 ^ 2 / (4 * P.𝓵))
   have h2' := h2 φ x
   linarith
@@ -342,7 +343,6 @@ lemma isMinOn_iff_of_μSq_nonpos_𝓵_pos (h𝓵 : 0 < P.𝓵) (hμ2 : P.μ2 ≤
     (x : SpaceTime) : IsMinOn (fun (φ, x) => P.toFun φ x) Set.univ (φ, x)
     ↔ P.toFun φ x = 0 := by
   have h1 := P.pos_𝓵_sol_exists_iff h𝓵
-  simp [hμ2] at h1
   rw [isMinOn_univ_iff]
   simp only [Prod.forall]
   refine Iff.intro (fun h => ?_) (fun h => ?_)
@@ -375,7 +375,7 @@ lemma isMinOn_iff_of_μSq_nonneg_𝓵_pos (h𝓵 : 0 < P.𝓵) (hμ2 : 0 ≤ P.
     (x : SpaceTime) : IsMinOn (fun (φ, x) => P.toFun φ x) Set.univ (φ, x) ↔
     P.toFun φ x = - P.μ2 ^ 2 / (4 * P.𝓵) := by
   have h1 := P.pos_𝓵_sol_exists_iff h𝓵
-  simp [hμ2, not_lt.mpr hμ2] at h1
+  simp only [not_lt.mpr hμ2, false_and, hμ2, true_and, false_or] at h1
   rw [isMinOn_univ_iff]
   simp only [Prod.forall]
   refine Iff.intro (fun h => ?_) (fun h => ?_)
diff --git a/HepLean/Tensors/ComplexLorentz/ColorFun.lean b/HepLean/Tensors/ComplexLorentz/ColorFun.lean
index 5ca0076..66c7287 100644
--- a/HepLean/Tensors/ComplexLorentz/ColorFun.lean
+++ b/HepLean/Tensors/ComplexLorentz/ColorFun.lean
@@ -152,7 +152,7 @@ lemma map_tprod {X Y : OverColor Color} (p : (i : X.left) → (colorToRep (X.hom
     PiTensorProduct.tprod ℂ fun (i : Y.left) => colorToRepCongr
     (OverColor.Hom.toEquiv_comp_inv_apply f i) (p ((OverColor.Hom.toEquiv f).symm i)) := by
   change (colorFun.map' f).hom ((PiTensorProduct.tprod ℂ) p) = _
-  simp [colorFun.map', mapToLinearEquiv']
+  simp only [map', mapToLinearEquiv', Functor.id_obj]
   erw [LinearEquiv.trans_apply]
   change (PiTensorProduct.congr fun i => colorToRepCongr _)
     ((PiTensorProduct.reindex ℂ (fun x => _) (OverColor.Hom.toEquiv f))
@@ -276,7 +276,9 @@ def μ (X Y : OverColor Color) : colorFun.obj X ⊗ colorFun.obj Y ≅ colorFun.
   inv := {
     hom := (μModEquiv X Y).symm.toLinearMap
     comm := fun M => by
-      simp [CategoryStruct.comp]
+      simp only [Action.instMonoidalCategory_tensorObj_V, CategoryStruct.comp,
+        colorFun_obj_V_carrier, OverColor.instMonoidalCategoryStruct_tensorObj_left,
+        OverColor.instMonoidalCategoryStruct_tensorObj_hom, Action.tensor_ρ']
       erw [LinearEquiv.eq_comp_toLinearMap_symm,LinearMap.comp_assoc,
       LinearEquiv.toLinearMap_symm_comp_eq]
       refine HepLean.PiTensorProduct.induction_tmul (fun p q => ?_)
@@ -428,7 +430,14 @@ lemma left_unitality (X : OverColor Color) : (leftUnitor (colorFun.obj X)).hom =
   change TensorProduct.lid ℂ (colorFun.obj X) (x ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) q) =
     (colorFun.map (λ_ X).hom).hom ((μ (𝟙_ (OverColor Color)) X).hom.hom
     ((((PiTensorProduct.isEmptyEquiv Empty).symm x) ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) q)))
-  simp [PiTensorProduct.isEmptyEquiv]
+  simp only [Functor.id_obj, lid_tmul, colorFun_obj_V_carrier,
+    OverColor.instMonoidalCategoryStruct_tensorObj_left,
+    OverColor.instMonoidalCategoryStruct_tensorUnit_left,
+    OverColor.instMonoidalCategoryStruct_tensorObj_hom, Action.instMonoidalCategory_tensorObj_V,
+    Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
+    Action.FunctorCategoryEquivalence.functor_obj_obj,
+    OverColor.instMonoidalCategoryStruct_tensorUnit_hom, PiTensorProduct.isEmptyEquiv,
+    LinearEquiv.coe_symm_mk]
   rw [TensorProduct.smul_tmul, TensorProduct.tmul_smul]
   erw [LinearMap.map_smul, LinearMap.map_smul]
   apply congrArg
@@ -454,7 +463,14 @@ lemma right_unitality (X : OverColor Color) : (MonoidalCategory.rightUnitor (col
   change TensorProduct.rid ℂ (colorFun.obj X) ((PiTensorProduct.tprod ℂ) p ⊗ₜ[ℂ] x) =
     (colorFun.map (ρ_ X).hom).hom ((μ X (𝟙_ (OverColor Color))).hom.hom
     ((((PiTensorProduct.tprod ℂ) p ⊗ₜ[ℂ] ((PiTensorProduct.isEmptyEquiv Empty).symm x)))))
-  simp [PiTensorProduct.isEmptyEquiv]
+  simp only [Functor.id_obj, rid_tmul, colorFun_obj_V_carrier,
+    OverColor.instMonoidalCategoryStruct_tensorObj_left,
+    OverColor.instMonoidalCategoryStruct_tensorUnit_left,
+    OverColor.instMonoidalCategoryStruct_tensorObj_hom, Action.instMonoidalCategory_tensorObj_V,
+    Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
+    Action.FunctorCategoryEquivalence.functor_obj_obj,
+    OverColor.instMonoidalCategoryStruct_tensorUnit_hom, PiTensorProduct.isEmptyEquiv,
+    LinearEquiv.coe_symm_mk, tmul_smul]
   erw [LinearMap.map_smul, LinearMap.map_smul]
   apply congrArg
   change _ = (colorFun.map (ρ_ X).hom).hom ((μ X (𝟙_ (OverColor Color))).hom.hom
diff --git a/HepLean/Tensors/ComplexLorentz/ContrNatTransform.lean b/HepLean/Tensors/ComplexLorentz/ContrNatTransform.lean
index c7af9e2..6ea9e11 100644
--- a/HepLean/Tensors/ComplexLorentz/ContrNatTransform.lean
+++ b/HepLean/Tensors/ComplexLorentz/ContrNatTransform.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.Tensors.OverColor.Basic
-import HepLean.Tensors.OverColor.Functors
 import HepLean.Tensors.ComplexLorentz.ColorFun
 import HepLean.Mathematics.PiTensorProduct
 /-!
@@ -59,7 +58,7 @@ lemma mapToLinearEquiv'_tprod {f g : OverColor Color} (m : f ⟶ g)
     PiTensorProduct.tprod ℂ fun i =>
     (TensorProduct.congr (colorToRepCongr (OverColor.Hom.toEquiv_symm_apply m i))
     (colorToRepCongr (mapToLinearEquiv'.proof_4 m i))) (x ((OverColor.Hom.toEquiv m).symm i)) := by
-  simp [mapToLinearEquiv']
+  simp only [mapToLinearEquiv', Functor.id_obj, LinearEquiv.trans_apply]
   change (PiTensorProduct.congr fun i => TensorProduct.congr (colorToRepCongr _)
     (colorToRepCongr _)) ((PiTensorProduct.reindex ℂ
     (fun x => ↑(colorToRep (f.hom x)).V ⊗[ℂ] ↑(colorToRep (τ (f.hom x))).V)
diff --git a/HepLean/Tensors/ComplexLorentz/Examples.lean b/HepLean/Tensors/ComplexLorentz/Examples.lean
index 82c0305..d589460 100644
--- a/HepLean/Tensors/ComplexLorentz/Examples.lean
+++ b/HepLean/Tensors/ComplexLorentz/Examples.lean
@@ -5,7 +5,6 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.Tensors.Tree.Basic
 import HepLean.Tensors.ComplexLorentz.TensorStruct
-import HepLean.Tensors.Tree.Elab
 /-!
 
 ## The tensor structure for complex Lorentz tensors
@@ -33,6 +32,8 @@ def upDown : Fin 2 → complexLorentzTensor.C
 variable (T S : complexLorentzTensor.F.obj (OverColor.mk upDown))
 
 /-
+import HepLean.Tensors.Tree.Elab
+
 #check {T | i m ⊗ S | m l}ᵀ.dot
 #check {T | i m ⊗ S | l τ(m)}ᵀ.dot
 -/
diff --git a/HepLean/Tensors/OverColor/Basic.lean b/HepLean/Tensors/OverColor/Basic.lean
index 4b8dd72..efc247c 100644
--- a/HepLean/Tensors/OverColor/Basic.lean
+++ b/HepLean/Tensors/OverColor/Basic.lean
@@ -54,13 +54,13 @@ def toEquiv (m : f ⟶ g) : f.left ≃ g.left where
 @[simp]
 lemma toEquiv_id (f : OverColor C) : toEquiv (𝟙 f) = Equiv.refl f.left := by
   ext x
-  simp [toEquiv]
+  simp only [toEquiv, Equiv.coe_fn_mk, Equiv.refl_apply]
   rfl
 
 @[simp]
 lemma toEquiv_comp (m : f ⟶ g) (n : g ⟶ h) : toEquiv (m ≫ n) = (toEquiv m).trans (toEquiv n) := by
   ext x
-  simp [toEquiv]
+  simp only [toEquiv, Equiv.coe_fn_mk, Equiv.trans_apply]
   rfl
 
 lemma toEquiv_symm_apply (m : f ⟶ g) (i : g.left) :
diff --git a/HepLean/Tensors/Tree/Elab.lean b/HepLean/Tensors/Tree/Elab.lean
index 69c193a..d11f8e2 100644
--- a/HepLean/Tensors/Tree/Elab.lean
+++ b/HepLean/Tensors/Tree/Elab.lean
@@ -5,7 +5,6 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.Tensors.Tree.Basic
 import Lean.Elab.Term
-import HepLean.Tensors.Tree.Dot
 /-!
 
 ## Elaboration of tensor trees
@@ -21,7 +20,6 @@ open Lean.Meta
 open Lean.Elab
 open Lean.Elab.Term
 open Lean Meta Elab Tactic
-open IndexNotation
 
 namespace TensorTree