From d62d59ace2d11b4d732f42f83642f0f3ec141ad3 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Tue, 3 Sep 2024 15:16:06 -0400
Subject: [PATCH] refactor: Replace tactics with rfl if allowed.

---
 .../MSSMNu/OrthogY3B3/ToSols.lean             |  6 ++---
 .../PureU1/Even/BasisLinear.lean              | 15 ++++++++-----
 .../PureU1/Odd/LineInCubic.lean               |  7 +-----
 HepLean/AnomalyCancellation/SM/Basic.lean     |  6 ++---
 .../SM/NoGrav/One/LinearParameterization.lean |  4 ++--
 .../AnomalyCancellation/SM/Permutations.lean  |  2 +-
 HepLean/AnomalyCancellation/SMNu/Basic.lean   |  4 ++--
 .../AnomalyCancellation/SMNu/FamilyMaps.lean  | 14 +++++-------
 .../SMNu/Ordinary/DimSevenPlane.lean          | 21 ++++++------------
 .../SMNu/PlusU1/BMinusL.lean                  | 10 ++++-----
 .../SMNu/PlusU1/BoundPlaneDim.lean            | 15 +++----------
 .../SMNu/PlusU1/FamilyMaps.lean               |  8 ++-----
 .../SMNu/PlusU1/HyperCharge.lean              |  9 +++-----
 .../SMNu/PlusU1/PlaneNonSols.lean             |  2 +-
 HepLean/FeynmanDiagrams/Instances/Phi4.lean   |  2 +-
 HepLean/FlavorPhysics/CKMMatrix/Basic.lean    | 22 ++++++++++---------
 .../FlavorPhysics/CKMMatrix/PhaseFreedom.lean |  4 ++--
 HepLean/SpaceTime/LorentzTensor/Basic.lean    | 15 ++++++-------
 .../SpaceTime/LorentzTensor/Contraction.lean  |  2 --
 .../LorentzTensor/IndexNotation/Basic.lean    |  3 +--
 .../IndexNotation/IndexList/Color.lean        |  5 +----
 .../IndexNotation/IndexList/Contraction.lean  |  1 -
 .../IndexNotation/IndexList/CountId.lean      |  7 +++---
 .../IndexNotation/IndexList/Equivs.lean       |  8 ++++---
 .../IndexNotation/TensorIndex.lean            |  8 ++-----
 HepLean/SpaceTime/MinkowskiMetric.lean        |  5 +++--
 26 files changed, 82 insertions(+), 123 deletions(-)

diff --git a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean
index 184855d..cdfc4e8 100644
--- a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean
@@ -97,8 +97,7 @@ def quadCoeff (T : MSSMACC.Sols) : ℚ :=
 lemma inQuadSolProp_iff_quadCoeff_zero (T : MSSMACC.Sols) : InQuadSolProp T ↔ quadCoeff T = 0 := by
   refine Iff.intro (fun h => ?_) (fun h => ?_)
   · rw [quadCoeff, h.1, h.2]
-    simp only [Fin.isValue, Fin.reduceFinMk, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true,
-      zero_pow, add_zero, mul_zero]
+    rfl
   · rw [quadCoeff, show dot Y₃.val B₃.val = 108 by rfl] at h
     simp only [Fin.isValue, Fin.reduceFinMk, mul_eq_zero, OfNat.ofNat_ne_zero, ne_eq,
       not_false_eq_true, pow_eq_zero_iff, or_self, false_or] at h
@@ -145,8 +144,7 @@ lemma inCubeSolProp_iff_cubicCoeff_zero (T : MSSMACC.Sols) :
     InCubeSolProp T ↔ cubicCoeff T = 0 := by
   refine Iff.intro (fun h => ?_) (fun h => ?_)
   · rw [cubicCoeff, h.1, h.2]
-    simp only [Fin.isValue, Fin.reduceFinMk, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true,
-      zero_pow, add_zero, mul_zero]
+    rfl
   · rw [cubicCoeff, show dot Y₃.val B₃.val = 108 by rfl] at h
     simp only [Fin.isValue, Fin.reduceFinMk, mul_eq_zero, OfNat.ofNat_ne_zero, ne_eq,
       not_false_eq_true, pow_eq_zero_iff, or_self, false_or] at h
diff --git a/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean b/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean
index d5d844d..7eaec5e 100644
--- a/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean
@@ -209,14 +209,17 @@ lemma basis_δ₂_eq_minus_δ₁ (j i : Fin n.succ) :
   simp [basisAsCharges, δ₂, δ₁]
   split <;> split
   any_goals split
+  any_goals rfl
   any_goals split
   any_goals rfl
-  all_goals rename_i h1 h2
-  all_goals rw [Fin.ext_iff] at h1 h2
-  all_goals simp_all
-  all_goals rename_i h3
-  all_goals rw [Fin.ext_iff] at h3
-  all_goals simp_all
+  all_goals
+    rename_i h1 h2
+    rw [Fin.ext_iff] at h1 h2
+    simp_all
+  all_goals
+    rename_i h3
+    rw [Fin.ext_iff] at h3
+    simp_all
   all_goals omega
 
 lemma basis!_δ!₂_eq_minus_δ!₁ (j i : Fin n) :
diff --git a/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean b/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean
index eb5429e..d2832a5 100644
--- a/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean
@@ -111,12 +111,7 @@ lemma P_P_P!_accCube' {S : (PureU1 (2 * n.succ.succ + 1)).LinSols}
   simp at h2
   have h5 : f 1 = S.val (δa₂ 0) + S.val δa₁ + S.val (δa₄ 0) := by
     linear_combination -(1 * h1) - 1 * h4 - 1 * h2
-  rw [h5]
-  rw [δa₄_δ!₂]
-  have h0 : (δa₂ (0 : Fin n.succ)) = δ!₁ 0 := by
-    rw [δa₂_δ!₁]
-    exact ht
-  rw [h0, δa₁_δ!₃]
+  rw [h5, δa₄_δ!₂, show (δa₂ (0 : Fin n.succ)) = δ!₁ 0 from rfl, δa₁_δ!₃]
   ring
 
 lemma lineInCubicPerm_last_cond {S : (PureU1 (2 * n.succ.succ+1)).LinSols}
diff --git a/HepLean/AnomalyCancellation/SM/Basic.lean b/HepLean/AnomalyCancellation/SM/Basic.lean
index f72c73b..73e0865 100644
--- a/HepLean/AnomalyCancellation/SM/Basic.lean
+++ b/HepLean/AnomalyCancellation/SM/Basic.lean
@@ -107,7 +107,7 @@ lemma accGrav_ext {S T : (SMCharges n).Charges}
     AddHom.coe_mk]
   repeat erw [Finset.sum_add_distrib]
   repeat erw [← Finset.mul_sum]
-  repeat erw [hj]
+  erw [hj, hj, hj, hj, hj]
   rfl
 
 /-- The `SU(2)` anomaly equation. -/
@@ -166,7 +166,7 @@ lemma accSU3_ext {S T : (SMCharges n).Charges}
     AddHom.coe_mk]
   repeat erw [Finset.sum_add_distrib]
   repeat erw [← Finset.mul_sum]
-  repeat erw [hj]
+  erw [hj, hj, hj]
   rfl
 
 /-- The `Y²` anomaly equation. -/
@@ -197,7 +197,7 @@ lemma accYY_ext {S T : (SMCharges n).Charges}
     AddHom.coe_mk]
   repeat erw [Finset.sum_add_distrib]
   repeat erw [← Finset.mul_sum]
-  repeat erw [hj]
+  erw [hj, hj, hj, hj, hj]
   rfl
 
 /-- The quadratic bilinear map. -/
diff --git a/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean b/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
index 3340f02..331ca63 100644
--- a/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
+++ b/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
@@ -303,7 +303,7 @@ lemma cubic_v_zero (S : linearParametersQENeqZero) (h : accCube (bijection S).1.
     by_contra hn
     have h : s ^ 2 < 0 := by
       rw [← hn]
-      simp [discrim]
+      rfl
     nlinarith
   simp_all
   exact eq_neg_of_add_eq_zero_left h'
@@ -321,7 +321,7 @@ lemma cube_w_zero (S : linearParametersQENeqZero) (h : accCube (bijection S).1.v
     by_contra hn
     have h : s ^ 2 < 0 := by
       rw [← hn]
-      simp [discrim]
+      rfl
     nlinarith
   simp_all
   exact eq_neg_of_add_eq_zero_left h'
diff --git a/HepLean/AnomalyCancellation/SM/Permutations.lean b/HepLean/AnomalyCancellation/SM/Permutations.lean
index 2619530..3f3f9f4 100644
--- a/HepLean/AnomalyCancellation/SM/Permutations.lean
+++ b/HepLean/AnomalyCancellation/SM/Permutations.lean
@@ -51,7 +51,7 @@ def repCharges {n : ℕ} : Representation ℚ (PermGroup n) (SMCharges n).Charge
     rw [charges_eq_toSpecies_eq]
     intro i
     simp only [chargeMap_apply, Pi.mul_apply, Pi.inv_apply, Equiv.Perm.coe_mul, LinearMap.mul_apply]
-    repeat erw [toSMSpecies_toSpecies_inv]
+    rw [toSMSpecies_toSpecies_inv, toSMSpecies_toSpecies_inv, toSMSpecies_toSpecies_inv]
     rfl
   map_one' := by
     apply LinearMap.ext
diff --git a/HepLean/AnomalyCancellation/SMNu/Basic.lean b/HepLean/AnomalyCancellation/SMNu/Basic.lean
index 2a393d4..92321f8 100644
--- a/HepLean/AnomalyCancellation/SMNu/Basic.lean
+++ b/HepLean/AnomalyCancellation/SMNu/Basic.lean
@@ -40,8 +40,8 @@ def toSpeciesEquiv : (SMνCharges n).Charges ≃ (Fin 6 → Fin n → ℚ) :=
 @[simps!]
 def toSpecies (i : Fin 6) : (SMνCharges n).Charges →ₗ[ℚ] (SMνSpecies n).Charges where
   toFun S := toSpeciesEquiv S i
-  map_add' _ _ := by aesop
-  map_smul' _ _ := by aesop
+  map_add' _ _ := by rfl
+  map_smul' _ _ := by rfl
 
 lemma charges_eq_toSpecies_eq (S T : (SMνCharges n).Charges) :
     S = T ↔ ∀ i, toSpecies i S = toSpecies i T := by
diff --git a/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean b/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean
index 748d2b4..790d2ef 100644
--- a/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean
+++ b/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean
@@ -113,10 +113,8 @@ lemma sum_familyUniversal {n : ℕ} (m : ℕ) (S : (SMνCharges 1).Charges) (j :
     rw [Fin.sum_const]
     simp
   erw [h1]
-  apply Finset.sum_congr
-  · simp only
-  · intro i _
-    erw [toSpecies_familyUniversal]
+  refine Finset.sum_congr rfl (fun i _ => ?_)
+  erw [toSpecies_familyUniversal]
 
 lemma sum_familyUniversal_one {n : ℕ} (S : (SMνCharges 1).Charges) (j : Fin 6) :
     ∑ i, toSpecies j (familyUniversal n S) i = n * (toSpecies j S ⟨0, by simp⟩) := by
@@ -128,11 +126,9 @@ lemma sum_familyUniversal_two {n : ℕ} (S : (SMνCharges 1).Charges)
     (toSpecies j S ⟨0, by simp⟩) * ∑ i, toSpecies j T i := by
   simp only [SMνSpecies_numberCharges, toSpecies_apply, Fin.zero_eta, Fin.isValue]
   rw [Finset.mul_sum]
-  apply Finset.sum_congr
-  · simp only
-  · intro i _
-    erw [toSpecies_familyUniversal]
-    rfl
+  refine Finset.sum_congr rfl (fun i _ => ?_)
+  erw [toSpecies_familyUniversal]
+  rfl
 
 lemma sum_familyUniversal_three {n : ℕ} (S : (SMνCharges 1).Charges)
     (T L : (SMνCharges n).Charges) (j : Fin 6) :
diff --git a/HepLean/AnomalyCancellation/SMNu/Ordinary/DimSevenPlane.lean b/HepLean/AnomalyCancellation/SMNu/Ordinary/DimSevenPlane.lean
index f707764..038a8b2 100644
--- a/HepLean/AnomalyCancellation/SMNu/Ordinary/DimSevenPlane.lean
+++ b/HepLean/AnomalyCancellation/SMNu/Ordinary/DimSevenPlane.lean
@@ -193,50 +193,43 @@ lemma B₀_B₀_Bi_cubic {i : Fin 7} :
     cubeTriLin (B 0) (B 0) (B i) = 0 := by
   change cubeTriLin (B₀) (B₀) (B i) = 0
   rw [B₀_cubic]
-  fin_cases i <;>
-  simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
+  fin_cases i <;> rfl
 
 lemma B₁_B₁_Bi_cubic {i : Fin 7} :
     cubeTriLin (B 1) (B 1) (B i) = 0 := by
   change cubeTriLin (B₁) (B₁) (B i) = 0
   rw [B₁_cubic]
-  fin_cases i <;>
-  simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
+  fin_cases i <;> rfl
 
 lemma B₂_B₂_Bi_cubic {i : Fin 7} :
     cubeTriLin (B 2) (B 2) (B i) = 0 := by
   change cubeTriLin (B₂) (B₂) (B i) = 0
   rw [B₂_cubic]
-  fin_cases i <;>
-  simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
+  fin_cases i <;> rfl
 
 lemma B₃_B₃_Bi_cubic {i : Fin 7} :
     cubeTriLin (B 3) (B 3) (B i) = 0 := by
   change cubeTriLin (B₃) (B₃) (B i) = 0
   rw [B₃_cubic]
-  fin_cases i <;>
-  simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
+  fin_cases i <;> rfl
 
 lemma B₄_B₄_Bi_cubic {i : Fin 7} :
     cubeTriLin (B 4) (B 4) (B i) = 0 := by
   change cubeTriLin (B₄) (B₄) (B i) = 0
   rw [B₄_cubic]
-  fin_cases i <;>
-  simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
+  fin_cases i <;> rfl
 
 lemma B₅_B₅_Bi_cubic {i : Fin 7} :
     cubeTriLin (B 5) (B 5) (B i) = 0 := by
   change cubeTriLin (B₅) (B₅) (B i) = 0
   rw [B₅_cubic]
-  fin_cases i <;>
-  simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
+  fin_cases i <;> rfl
 
 lemma B₆_B₆_Bi_cubic {i : Fin 7} :
     cubeTriLin (B 6) (B 6) (B i) = 0 := by
   change cubeTriLin (B₆) (B₆) (B i) = 0
   rw [B₆_cubic]
-  fin_cases i <;>
-  simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
+  fin_cases i <;> rfl
 
 lemma Bi_Bi_Bj_cubic (i j : Fin 7) :
     cubeTriLin (B i) (B i) (B j) = 0 := by
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean
index 846ef0e..7a57929 100644
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean
@@ -66,9 +66,8 @@ lemma on_quadBiLin (S : (PlusU1 n).Charges) :
   ring
 
 lemma on_quadBiLin_AFL (S : (PlusU1 n).LinSols) : quadBiLin (BL n).val S.val = 0 := by
-  rw [on_quadBiLin]
-  rw [YYsol S, SU2Sol S, SU3Sol S]
-  simp
+  rw [on_quadBiLin, YYsol S, SU2Sol S, SU3Sol S]
+  rfl
 
 lemma add_AFL_quad (S : (PlusU1 n).LinSols) (a b : ℚ) :
     accQuad (a • S.val + b • (BL n).val) = a ^ 2 * accQuad S.val := by
@@ -100,9 +99,8 @@ lemma on_cubeTriLin (S : (PlusU1 n).Charges) :
 
 lemma on_cubeTriLin_AFL (S : (PlusU1 n).LinSols) :
     cubeTriLin (BL n).val (BL n).val S.val = 0 := by
-  rw [on_cubeTriLin]
-  rw [gravSol S, SU3Sol S]
-  simp
+  rw [on_cubeTriLin, gravSol S, SU3Sol S]
+  rfl
 
 lemma add_AFL_cube (S : (PlusU1 n).LinSols) (a b : ℚ) :
     accCube (a • S.val + b • (BL n).val) =
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean
index e0f92b1..4363a09 100644
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean
@@ -32,18 +32,9 @@ lemma exists_plane_exists_basis {n : ℕ} (hE : ExistsPlane n) :
   obtain ⟨B, hB1, hB2⟩ := eleven_dim_plane_of_no_sols_exists
   let Y := Sum.elim B E
   use Y
-  apply Fintype.linearIndependent_iff.mpr
-  intro g hg
-  rw [@Fintype.sum_sum_type] at hg
-  rw [@add_eq_zero_iff_eq_neg] at hg
-  rw [← @Finset.sum_neg_distrib] at hg
-  have h1 : ∑ x : Fin n, -(g (Sum.inr x) • Y (Sum.inr x)) =
-      ∑ x : Fin n, (-g (Sum.inr x)) • Y (Sum.inr x) := by
-    apply Finset.sum_congr
-    simp only
-    intro i _
-    simp
-  rw [h1] at hg
+  refine Fintype.linearIndependent_iff.mpr (fun g hg => ?_)
+  rw [Fintype.sum_sum_type, add_eq_zero_iff_eq_neg, ← Finset.sum_neg_distrib] at hg
+  rw [Finset.sum_congr rfl (fun i _ => (neg_smul (g (Sum.inr i)) (Y (Sum.inr i))).symm)] at hg
   have h2 : ∑ a₁ : Fin 11, g (Sum.inl a₁) • Y (Sum.inl a₁) = 0 := by
     apply hB2
     erw [hg]
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/FamilyMaps.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/FamilyMaps.lean
index fde5f3f..5fc9296 100644
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/FamilyMaps.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/FamilyMaps.lean
@@ -30,12 +30,8 @@ def familyUniversalLinear (n : ℕ) :
     (by rw [familyUniversal_accSU2, SU2Sol S, mul_zero])
     (by rw [familyUniversal_accSU3, SU3Sol S, mul_zero])
     (by rw [familyUniversal_accYY, YYsol S, mul_zero])
-  map_add' S T := by
-    apply ACCSystemLinear.LinSols.ext
-    exact (familyUniversal n).map_add' _ _
-  map_smul' a S := by
-    apply ACCSystemLinear.LinSols.ext
-    exact (familyUniversal n).map_smul' _ _
+  map_add' S T := rfl
+  map_smul' a S := rfl
 
 /-- The family universal maps on `QuadSols`. -/
 def familyUniversalQuad (n : ℕ) :
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.lean
index d2fce6f..22a24f8 100644
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.lean
@@ -98,9 +98,8 @@ lemma on_cubeTriLin (S : (PlusU1 n).Charges) :
 
 lemma on_cubeTriLin_AFL (S : (PlusU1 n).LinSols) :
     cubeTriLin (Y n).val (Y n).val S.val = 0 := by
-  rw [on_cubeTriLin]
-  rw [YYsol S]
-  simp
+  rw [on_cubeTriLin, YYsol S]
+  rfl
 
 lemma on_cubeTriLin' (S : (PlusU1 n).Charges) :
     cubeTriLin (Y n).val S S = 6 * accQuad S := by
@@ -112,9 +111,7 @@ lemma on_cubeTriLin' (S : (PlusU1 n).Charges) :
 
 lemma on_cubeTriLin'_ALQ (S : (PlusU1 n).QuadSols) :
     cubeTriLin (Y n).val S.val S.val = 0 := by
-  rw [on_cubeTriLin']
-  rw [quadSol S]
-  simp
+  rw [on_cubeTriLin', quadSol S, mul_zero]
 
 lemma add_AFL_cube (S : (PlusU1 n).LinSols) (a b : ℚ) :
     accCube (a • S.val + b • (Y n).val) =
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/PlaneNonSols.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/PlaneNonSols.lean
index bce1d3d..9d6b201 100644
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/PlaneNonSols.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/PlaneNonSols.lean
@@ -213,7 +213,7 @@ lemma isSolution_f9 (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f i
 lemma isSolution_f10 (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f i • B i)) :
     f 10 = 0 := by
   rw [isSolution_grav f hS, isSolution_f9 f hS]
-  simp
+  rfl
 
 lemma isSolution_f_zero (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f i • B i))
     (k : Fin 11) : f k = 0 := by
diff --git a/HepLean/FeynmanDiagrams/Instances/Phi4.lean b/HepLean/FeynmanDiagrams/Instances/Phi4.lean
index 6ee2510..14a318a 100644
--- a/HepLean/FeynmanDiagrams/Instances/Phi4.lean
+++ b/HepLean/FeynmanDiagrams/Instances/Phi4.lean
@@ -85,7 +85,7 @@ lemma figureEight_connected : Connected figureEight := by decide
 
 /-- The symmetry factor of `figureEight` is 8. We can get this from
   `#eval symmetryFactor figureEight`. -/
-lemma figureEight_symmetryFactor : symmetryFactor figureEight = 8 := by decide
+lemma figureEight_symmetryFactor : symmetryFactor figureEight = 8 := by rfl
 
 end Example
 
diff --git a/HepLean/FlavorPhysics/CKMMatrix/Basic.lean b/HepLean/FlavorPhysics/CKMMatrix/Basic.lean
index 6b24b7a..9ded779 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/Basic.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/Basic.lean
@@ -31,9 +31,15 @@ def phaseShiftMatrix (a b c : ℝ) : Matrix (Fin 3) (Fin 3) ℂ :=
 
 lemma phaseShiftMatrix_one : phaseShiftMatrix 0 0 0 = 1 := by
   ext i j
-  fin_cases i <;> fin_cases j <;>
-  simp [Matrix.one_apply, phaseShiftMatrix]
-  rfl
+  fin_cases i <;> fin_cases j
+  any_goals rfl
+  · simp only [phaseShiftMatrix, ofReal_zero, mul_zero, exp_zero, Fin.zero_eta, Fin.isValue,
+    cons_val', cons_val_zero, empty_val', cons_val_fin_one, vecCons_const, one_apply_eq]
+  · simp only [phaseShiftMatrix, ofReal_zero, mul_zero, exp_zero, Fin.mk_one, Fin.isValue,
+    cons_val', cons_val_one, head_cons, empty_val', cons_val_fin_one, one_apply_eq]
+  · simp only [phaseShiftMatrix, ofReal_zero, mul_zero, exp_zero, Fin.reduceFinMk, cons_val',
+    Fin.isValue, cons_val_two, Nat.succ_eq_add_one, Nat.reduceAdd, tail_cons, head_cons, empty_val',
+    cons_val_fin_one, head_fin_const, one_apply_eq]
 
 lemma phaseShiftMatrix_star (a b c : ℝ) :
     (phaseShiftMatrix a b c)ᴴ = phaseShiftMatrix (- a) (- b) (- c) := by
@@ -96,14 +102,10 @@ lemma phaseShiftRelation_trans {U V W : unitaryGroup (Fin 3) ℂ} :
   obtain ⟨a, b, c, e, f, g, hUV⟩ := hUV
   obtain ⟨d, i, j, k, l, m, hVW⟩ := hVW
   use (a + d), (b + i), (c + j), (e + k), (f + l), (g + m)
-  rw [Subtype.ext_iff_val]
-  rw [hUV, hVW]
+  rw [Subtype.ext_iff_val, hUV, hVW]
   simp only [Submonoid.coe_mul, phaseShift_coe_matrix]
-  repeat rw [mul_assoc]
-  rw [phaseShiftMatrix_mul]
-  repeat rw [← mul_assoc]
-  rw [phaseShiftMatrix_mul]
-  rw [add_comm k e, add_comm l f, add_comm m g]
+  rw [mul_assoc, mul_assoc, phaseShiftMatrix_mul, ← mul_assoc, ← mul_assoc, phaseShiftMatrix_mul,
+    add_comm k e, add_comm l f, add_comm m g]
 
 lemma phaseShiftRelation_equiv : Equivalence PhaseShiftRelation where
   refl := phaseShiftRelation_refl
diff --git a/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean b/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean
index cc1c441..28c916e 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean
@@ -215,12 +215,12 @@ lemma ubOnePhaseCond_shift_solution {V : CKMMatrix} (h1 : a + f = - arg [V]ub)
   have hd : d = Real.pi - arg [V]cd - b := by
     linear_combination h3
   subst he hd
-  simp_all
+  simp_all only [add_sub_cancel, and_self, and_true]
   ring_nf at h2
   have hc : c = - Real.pi + arg [V]cd + arg [V]cs + arg [V]ub + b := by
     linear_combination h2
   subst hc
-  ring
+  rfl
 
 lemma fstRowThdColRealCond_holds_up_to_equiv (V : CKMMatrix) :
     ∃ (U : CKMMatrix), V ≈ U ∧ FstRowThdColRealCond U:= by
diff --git a/HepLean/SpaceTime/LorentzTensor/Basic.lean b/HepLean/SpaceTime/LorentzTensor/Basic.lean
index b510c00..dc7187a 100644
--- a/HepLean/SpaceTime/LorentzTensor/Basic.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Basic.lean
@@ -200,7 +200,6 @@ lemma contrRightAux_comp {V1 V2 V3 V4 V5 : Type} [AddCommMonoid V1] [AddCommMono
     by simp [add_tmul, tmul_add, LinearMap.map_add, h1, h2])
   intro x3 x4
   simp [contrRightAux, contrMidAux, contrLeftAux]
-  erw [TensorProduct.map_tmul]
   rfl
 
 end TensorStructure
@@ -433,7 +432,7 @@ lemma elimPureTensor_update_left (p : 𝓣.PureTensor cX) (q : 𝓣.PureTensor c
     split_ifs
     · rename_i h
       subst h
-      simp_all only
+      rfl
     · rfl
   | Sum.inr y => rfl
 
@@ -453,10 +452,10 @@ lemma inlPureTensor_update_left [DecidableEq (X ⊕ Y)] (f : 𝓣.PureTensor (Su
   funext y
   simp [inlPureTensor, Function.update, Sum.inl.injEq, Sum.elim_inl]
   split
-  next h =>
+  · rename_i h
     subst h
-    simp_all only
-  rfl
+    rfl
+  · rfl
 
 @[simp]
 lemma inrPureTensor_update_left [DecidableEq (X ⊕ Y)] (f : 𝓣.PureTensor (Sum.elim cX cY)) (x : X)
@@ -473,10 +472,10 @@ lemma inrPureTensor_update_right [DecidableEq (X ⊕ Y)] (f : 𝓣.PureTensor (S
   funext y
   simp [inrPureTensor, Function.update, Sum.inl.injEq, Sum.elim_inl]
   split
-  next h =>
+  · rename_i h
     subst h
-    simp_all only
-  rfl
+    rfl
+  · rfl
 
 @[simp]
 lemma inlPureTensor_update_right [DecidableEq (X ⊕ Y)] (f : 𝓣.PureTensor (Sum.elim cX cY)) (y : Y)
diff --git a/HepLean/SpaceTime/LorentzTensor/Contraction.lean b/HepLean/SpaceTime/LorentzTensor/Contraction.lean
index 772c602..857067b 100644
--- a/HepLean/SpaceTime/LorentzTensor/Contraction.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Contraction.lean
@@ -289,7 +289,6 @@ lemma contrAll_mapIso_right_tmul (e : X ≃ Y) (e' : Z ≃ Y)
     𝓣.contrAll e h (x ⊗ₜ[R] 𝓣.mapIso e' h' z) =
     𝓣.contrAll (e.trans e'.symm) (h.trans_mapIso h') (x ⊗ₜ[R] z) := by
   simp only [contrAll_tmul, mapIso_mapIso]
-  apply congrArg
   rfl
 
 @[simp]
@@ -429,7 +428,6 @@ lemma contr_tprod (e : (C ⊕ C) ⊕ P ≃ X) (h : cX.ContrCond e) (f : (i : X)
     Function.comp_apply, LinearEquiv.trans_apply, mapIso_tprod, Equiv.symm_symm_apply,
     tensoratorEquiv_symm_tprod, congr_tmul, LinearEquiv.refl_apply, map_tmul, LinearMap.id_coe,
     id_eq, lid_tmul]
-  rw [contrAll_tmul]
   rfl
 
 open PiTensorProduct in
diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean
index ce4ac53..b3e1b62 100644
--- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean
+++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean
@@ -86,8 +86,7 @@ lemma listCharIndex_iff (l : List Char) : listCharIndex X l
     ↔ (if h : l = [] then True else
     let sfst := l.head h
     if ¬ isNotationChar X sfst then False
-    else listCharIndexTail sfst l.tail) := by
-  rw [listCharIndex]
+    else listCharIndexTail sfst l.tail) := by rfl
 
 instance : Decidable (listCharIndex X l) :=
   @decidable_of_decidable_of_iff _ _
diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexList/Color.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexList/Color.lean
index d326c66..3aadeae 100644
--- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexList/Color.lean
+++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexList/Color.lean
@@ -457,12 +457,9 @@ lemma mem_iff_dual_mem (hl : l.OnlyUniqueDuals) (hc : l.ColorCond) (I : Index 
     omega
   · have hIdd : l.countId I.dual = 2 := by
       rw [← hId]
-      apply countId_congr
       rfl
     have hc' := (hc I.dual h hIdd).2
-    simp at hc'
-    rw [← countSelf_neq_zero]
-    rw [← countSelf_neq_zero] at h
+    rw [← countSelf_neq_zero] at h ⊢
     rw [countDual_eq_countSelf_Dual] at hc'
     simp at hc'
     exact Ne.symm (ne_of_ne_of_eq (id (Ne.symm h)) hc')
diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexList/Contraction.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexList/Contraction.lean
index 83b4dad..c2af0d5 100644
--- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexList/Contraction.lean
+++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexList/Contraction.lean
@@ -45,7 +45,6 @@ def contrIndexList : IndexList X where
 
 @[simp]
 lemma contrIndexList_empty : (⟨[]⟩ : IndexList X).contrIndexList = { val := [] } := by
-  apply ext
   rfl
 
 lemma contrIndexList_val : l.contrIndexList.val =
diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexList/CountId.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexList/CountId.lean
index 986013d..09550cb 100644
--- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexList/CountId.lean
+++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexList/CountId.lean
@@ -113,8 +113,7 @@ lemma countId_get_other (i : Fin l.length) : l2.countId (l.val.get i) =
     simp only [length, List.finRange_map_get]
   nth_rewrite 1 [hl2]
   rw [List.filter_map, List.length_map]
-  apply congrArg
-  refine List.filter_congr (fun j _ => rfl)
+  rfl
 
 /-! TODO: Replace with mathlib lemma. -/
 lemma filter_finRange (i : Fin l.length) :
@@ -269,7 +268,7 @@ lemma countId_eq_two_of_mem_withUniqueDual (i : Fin l.length) (h : i ∈ l.withU
       ((List.finRange l.length).filter fun j => l.AreDualInSelf i j)
     · exact List.filter_comm (fun j => l.AreDualInSelf i j) (fun j => j = i')
         (List.finRange l.length)
-    · simp
+    · simp only [List.filter_filter, decide_eq_true_eq, Bool.decide_and]
       refine List.filter_congr (fun j _ => ?_)
       simp only [Bool.and_iff_right_iff_imp, decide_eq_true_eq]
       simp [withUniqueDual] at h
@@ -279,7 +278,7 @@ lemma countId_eq_two_of_mem_withUniqueDual (i : Fin l.length) (h : i ∈ l.withU
       rw [hj']
       simp [i']
   rw [List.countP_eq_length_filter, ← h1]
-  simp
+  rfl
 
 lemma mem_withUniqueDual_of_countId_eq_two (i : Fin l.length)
     (h : l.countId (l.val.get i) = 2) : i ∈ l.withUniqueDual := by
diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexList/Equivs.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexList/Equivs.lean
index 25f0fcd..7c016ed 100644
--- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexList/Equivs.lean
+++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexList/Equivs.lean
@@ -141,10 +141,12 @@ lemma getDualInOtherEquiv_self_refl : l.getDualInOtherEquiv l = Equiv.refl _ :=
   apply Subtype.eq
   simp only
   have hx2 := x.2
-  simp [withUniqueDualInOther] at hx2
+  simp only [withUniqueDualInOther, mem_withDual_iff_isSome, Bool.not_eq_true, Option.not_isSome,
+    Option.isNone_iff_eq_none, mem_withInDualOther_iff_isSome, getDualInOther?_self_isSome,
+    true_and, Finset.mem_filter, Finset.mem_univ] at hx2
   apply Option.some_injective
-  rw [hx2.2 x.1 (by simp [AreDualInOther])]
-  simp
+  rw [hx2.2 x.1 (by rfl)]
+  exact Option.some_get (getDualInOtherEquiv.proof_1 l l x)
 
 @[simp]
 lemma getDualInOtherEquiv_symm : (l.getDualInOtherEquiv l2).symm = l2.getDualInOtherEquiv l := by
diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean
index 046ec88..2c81bf1 100644
--- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean
+++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean
@@ -215,8 +215,7 @@ lemma symm {T₁ T₂ : 𝓣.TensorIndex} (h : Rel T₁ T₂) : Rel T₂ T₁ :=
   · symm
     erw [LinearEquiv.symm_apply_eq]
     rw [h.2]
-    · apply congrFun
-      congr
+    · rfl
     exact h'.symm
 
 /-- Rel is transitive. -/
@@ -282,10 +281,7 @@ lemma rel_contr (T : 𝓣.TensorIndex) : T ≈ T.contr := by
       Fin.symm_castOrderIso, mapIso_mapIso, tensorIso]
     trans 𝓣.mapIso (Equiv.refl _) (by rfl) T.contr.tensor
     · simp only [contr_toColorIndexList, mapIso_refl, LinearEquiv.refl_apply]
-    · apply congrFun
-      apply congrArg
-      apply congrArg
-      rfl
+    · rfl
 
 /-!
 
diff --git a/HepLean/SpaceTime/MinkowskiMetric.lean b/HepLean/SpaceTime/MinkowskiMetric.lean
index c478753..fbc2553 100644
--- a/HepLean/SpaceTime/MinkowskiMetric.lean
+++ b/HepLean/SpaceTime/MinkowskiMetric.lean
@@ -142,7 +142,7 @@ lemma as_sum :
     Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, Sum.elim_inl, one_mul,
     Finset.sum_singleton, Sum.elim_inr, neg_mul, mul_neg, Finset.sum_neg_distrib, time, space,
     Function.comp_apply, minkowskiMatrix]
-  ring
+  rfl
 
 /-- The Minkowski metric expressed as a sum for a single vector. -/
 lemma as_sum_self : ⟪v, v⟫ₘ = v.time ^ 2 - ‖v.space‖ ^ 2 := by
@@ -151,7 +151,7 @@ lemma as_sum_self : ⟪v, v⟫ₘ = v.time ^ 2 - ‖v.space‖ ^ 2 := by
 
 lemma eq_time_minus_inner_prod : ⟪v, w⟫ₘ = v.time * w.time - ⟪v.space, w.space⟫_ℝ := by
   rw [as_sum, @PiLp.inner_apply]
-  noncomm_ring
+  rfl
 
 lemma self_eq_time_minus_norm : ⟪v, v⟫ₘ = v.time ^ 2 - ‖v.space‖ ^ 2 := by
   rw [← real_inner_self_eq_norm_sq, PiLp.inner_apply, as_sum]
@@ -192,6 +192,7 @@ lemma self_spaceReflection_eq_zero_iff : ⟪v, v.spaceReflection⟫ₘ = 0 ↔ v
     · simpa using congrFun h4 i
   · rw [h]
     exact LinearMap.map_zero₂ minkowskiMetric (spaceReflection 0)
+
 /-!
 
 # Non degeneracy of the Minkowski metric