Merge pull request #132 from HEPLean/simp_replace

refactor: Replace some simp with exact

HepLean/AnomalyCancellation/Basic.lean

@@ -200,7 +200,7 @@ def IsSolution (χ : ACCSystem) (S : χ.Charges) : Prop :=
 instance solsMulAction (χ : ACCSystem) : MulAction ℚ χ.Sols where
   smul a S := ⟨a • S.toQuadSols, by
     erw [(χ.cubicACC).map_smul, S.cubicSol]
-    simp⟩
+    exact Rat.mul_zero (a ^ 3)⟩
   mul_smul a b S := Sols.ext (mul_smul _ _ _)
   one_smul S := Sols.ext (one_smul _ _)
 

HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean

@@ -73,7 +73,7 @@ lemma linEqPropSol_iff_proj_linEqProp (R : MSSMACC.Sols) :
     rw [α₁_proj, α₂_proj, h]
     simp only [neg_zero, Fin.isValue, Fin.reduceFinMk, zero_mul, and_self]
   · rw [h.2.2]
-    simp
+    exact Rat.mul_zero ((dot Y₃.val) B₃.val)
 
 /-- A condition which is satisfied if the plane spanned by `R`, `Y₃` and `B₃` lies
 entirely in the quadratic surface. -/
@@ -119,7 +119,7 @@ lemma inQuadSolProp_iff_proj_inQuadProp (R : MSSMACC.Sols) :
     simp only [Fin.isValue, Fin.reduceFinMk, mul_eq_zero,
       OfNat.ofNat_ne_zero, or_self, false_or] at h
     rw [h.2.1, h.2.2]
-    simp
+    exact Prod.mk_eq_zero.mp rfl
 
 /-- A condition which is satisfied if the plane spanned by `R`, `Y₃` and `B₃` lies
 entirely in the cubic surface. -/
@@ -166,7 +166,7 @@ lemma inCubeSolProp_iff_proj_inCubeProp (R : MSSMACC.Sols) :
     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
     rw [h.2.1, h.2.2]
-    simp
+    exact Prod.mk_eq_zero.mp rfl
 
 /-- Those charge assignments perpendicular to `Y₃` and `B₃` which satisfy the condition
 `lineEqProp`. -/
@@ -215,7 +215,7 @@ lemma toSolNSQuad_eq_planeY₃B₃_on_α (R : MSSMACC.AnomalyFreePerp) :
   apply planeY₃B₃_eq
   rw [α₁, α₂, α₃]
   ring_nf
-  simp
+  exact ⟨trivial, trivial, trivial⟩
 
 /-- Given an `R` perpendicular to `Y₃` and `B₃`, an element of `Sols`. This map is
 not surjective. -/
@@ -243,7 +243,7 @@ lemma toSolNS_proj (T : NotInLineEqSol) : toSolNS (toSolNSProj T.val) = T.val :=
   rw [h1]
   have h1 := (lineEqPropSol_iff_lineEqCoeff_zero T.val).mpr.mt T.prop
   rw [← MulAction.mul_smul, mul_comm, mul_inv_cancel h1]
-  simp
+  exact MulAction.one_smul T.1.val
 
 /-- A solution to the ACCs, given an element of `inLineEq × ℚ × ℚ × ℚ`. -/
 def inLineEqToSol : InLineEq × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R, c₁, c₂, c₃) =>
@@ -286,7 +286,7 @@ lemma inLineEqToSol_proj (T : InLineEqSol) : inLineEqToSol (inLineEqProj T) = T.
   rw [h1]
   have h2 := (inQuadSolProp_iff_quadCoeff_zero T.val).mpr.mt T.prop.2
   rw [← MulAction.mul_smul, mul_comm, mul_inv_cancel h2]
-  simp
+  exact MulAction.one_smul T.1.val
 
 /-- Given an element of `inQuad × ℚ × ℚ × ℚ`, a solution to the ACCs. -/
 def inQuadToSol : InQuad × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R, a₁, a₂, a₃) =>
@@ -331,7 +331,7 @@ lemma inQuadToSol_proj (T : InQuadSol) : inQuadToSol (inQuadProj T) = T.val := b
   rw [h1]
   have h2 := (inCubeSolProp_iff_cubicCoeff_zero T.val).mpr.mt T.prop.2.2
   rw [← MulAction.mul_smul, mul_comm, mul_inv_cancel h2]
-  simp
+  exact MulAction.one_smul T.1.val
 
 /-- Given a element of `inQuadCube × ℚ × ℚ × ℚ`, a solution to the ACCs. -/
 def inQuadCubeToSol : InQuadCube × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R, b₁, b₂, b₃) =>
@@ -371,9 +371,9 @@ lemma inQuadCubeToSol_proj (T : InQuadCubeSol) :
   ring_nf
   simp only [Fin.isValue, Fin.reduceFinMk, zero_smul, add_zero, zero_add]
   rw [← MulAction.mul_smul, mul_comm, mul_inv_cancel]
-  · simp only [one_smul]
+  · exact MulAction.one_smul (T.1).val
   · rw [show dot Y₃.val B₃.val = 108 by rfl]
-    simp
+    exact Ne.symm (OfNat.zero_ne_ofNat 108)
 
 /-- A solution from an element of `MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ`. We will
 show that this map is a surjection. -/

HepLean/AnomalyCancellation/PureU1/Basic.lean

@@ -138,7 +138,7 @@ lemma pureU1_anomalyFree_ext {n : ℕ} {S T : (PureU1 n.succ).LinSols}
     rw [hi, pureU1_last, pureU1_last]
     simp only [neg_inj]
     apply Finset.sum_congr
-    · simp only
+    · rfl
     · exact fun j _ => h j
 
 namespace PureU1
@@ -146,23 +146,21 @@ namespace PureU1
 lemma sum_of_charges {n : ℕ} (f : Fin k → (PureU1 n).Charges) (j : Fin n) :
     (∑ i : Fin k, (f i)) j = ∑ i : Fin k, (f i) j := by
   induction k
-  · simp only [univ_eq_empty, sum_empty]
-    rfl
+  · rfl
   · rename_i k hl
     rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]
     have hlt := hl (f ∘ Fin.castSucc)
     erw [← hlt]
-    simp
+    rfl
 
 lemma sum_of_anomaly_free_linear {n : ℕ} (f : Fin k → (PureU1 n).LinSols) (j : Fin n) :
     (∑ i : Fin k, (f i)).1 j = (∑ i : Fin k, (f i).1 j) := by
   induction k
-  · simp only [univ_eq_empty, sum_empty, ACCSystemLinear.linSolsAddCommMonoid_zero_val]
-    rfl
+  · rfl
   · rename_i k hl
     rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]
     have hlt := hl (f ∘ Fin.castSucc)
     erw [← hlt]
-    simp
+    rfl
 
 end PureU1

HepLean/AnomalyCancellation/PureU1/ConstAbs.lean

@@ -61,7 +61,7 @@ lemma lt_eq {k i : Fin n.succ} (hk : S k ≤ 0) (hik : i ≤ k) : S i = S k := b
 lemma val_le_zero {i : Fin n.succ} (hi : S i ≤ 0) : S i = S (0 : Fin n.succ) := by
   symm
   apply lt_eq hS hi
-  simp
+  exact Fin.zero_le i
 
 lemma gt_eq {k i: Fin n.succ} (hk : 0 ≤ S k) (hik : k ≤ i) : S i = S k := by
   have hSS := hS.2 k i hik
@@ -73,8 +73,7 @@ lemma gt_eq {k i: Fin n.succ} (hk : 0 ≤ S k) (hik : k ≤ i) : S i = S k := by
 
 lemma zero_gt (h0 : 0 ≤ S (0 : Fin n.succ)) (i : Fin n.succ) : S (0 : Fin n.succ) = S i := by
   symm
-  refine gt_eq hS h0 ?_
-  simp
+  refine gt_eq hS h0 (Fin.zero_le i)
 
 lemma opposite_signs_eq_neg {i j : Fin n.succ} (hi : S i ≤ 0) (hj : 0 ≤ S j) : S i = - S j := by
   have hSS := hS.1 i j
@@ -98,7 +97,7 @@ is defined as a element of `k ∈ Fin n` such that `S k.castSucc` and `S k.succ`
 def Boundary (S : (PureU1 n.succ).Charges) (k : Fin n) : Prop := S k.castSucc < 0 ∧ 0 < S k.succ
 
 lemma boundary_castSucc {k : Fin n} (hk : Boundary S k) : S k.castSucc = S (0 : Fin n.succ) :=
-  (lt_eq hS (le_of_lt hk.left) (by simp : 0 ≤ k.castSucc)).symm
+  (lt_eq hS (le_of_lt hk.left) (Fin.zero_le k.castSucc : 0 ≤ k.castSucc)).symm
 
 lemma boundary_succ {k : Fin n} (hk : Boundary S k) : S k.succ = - S (0 : Fin n.succ) := by
   have hn := boundary_castSucc hS hk
@@ -114,8 +113,7 @@ lemma boundary_accGrav' (k : Fin n) : accGrav n.succ S =
   erw [Finset.sum_equiv (Fin.castOrderIso (boundary_split k)).toEquiv]
   · intro i
     simp only [Fin.val_succ, mem_univ, RelIso.coe_fn_toEquiv]
-  · intro i
-    simp
+  · exact fun _ _ => rfl
 
 lemma boundary_accGrav'' (k : Fin n) (hk : Boundary S k) :
     accGrav n.succ S = (2 * ↑↑k + 1 - ↑n) * S (0 : Fin n.succ) := by
@@ -123,10 +121,10 @@ lemma boundary_accGrav'' (k : Fin n) (hk : Boundary S k) :
   rw [Fin.sum_univ_add]
   have hfst (i : Fin k.succ.val) :
       S (Fin.cast (boundary_split k) (Fin.castAdd (n.succ - k.succ.val) i)) = S k.castSucc := by
-    apply lt_eq hS (le_of_lt hk.left) (by rw [Fin.le_def]; simp; omega)
+    apply lt_eq hS (le_of_lt hk.left) (Fin.is_le i)
   have hsnd (i : Fin (n.succ - k.succ.val)) :
       S (Fin.cast (boundary_split k) (Fin.natAdd (k.succ.val) i)) = S k.succ := by
-    apply gt_eq hS (le_of_lt hk.right) (by rw [Fin.le_def]; simp)
+    apply gt_eq hS (le_of_lt hk.right) (by rw [Fin.le_def]; exact le.intro rfl)
   simp only [hfst, hsnd]
   simp only [Fin.val_succ, sum_const, card_fin, nsmul_eq_mul, cast_add, cast_one,
     succ_sub_succ_eq_sub, Fin.is_le', cast_sub]
@@ -145,8 +143,8 @@ lemma not_hasBoundary_zero_le (hnot : ¬ (HasBoundary S)) (h0 : S (0 : Fin n.suc
   induction i
   · rfl
   · rename_i i hii
-    have hnott := hnot ⟨i, by {simp at hi; linarith}⟩
-    have hii := hii (by omega)
+    have hnott := hnot ⟨i, succ_lt_succ_iff.mp hi⟩
+    have hii := hii (lt_of_succ_lt hi)
     erw [← hii] at hnott
     exact (val_le_zero hS (hnott h0)).symm
 
@@ -214,7 +212,7 @@ lemma AFL_even_below' {A : (PureU1 (2 * n.succ)).LinSols} (h : ConstAbsSorted A.
   rw [Fin.le_def]
   simp only [PureU1_numberCharges, Fin.coe_cast, Fin.coe_castAdd, mul_eq, Fin.coe_castSucc]
   rw [AFL_even_Boundary h hA hk]
-  omega
+  exact Fin.is_le i
 
 lemma AFL_even_below (A : (PureU1 (2 * n.succ)).LinSols) (h : ConstAbsSorted A.val)
     (i : Fin n.succ) :
@@ -235,7 +233,7 @@ lemma AFL_even_above' {A : (PureU1 (2 * n.succ)).LinSols} (h : ConstAbsSorted A.
   rw [Fin.le_def]
   simp only [mul_eq, Fin.val_succ, PureU1_numberCharges, Fin.coe_cast, Fin.coe_natAdd]
   rw [AFL_even_Boundary h hA hk]
-  omega
+  exact Nat.le_add_right (n + 1) ↑i
 
 lemma AFL_even_above (A : (PureU1 (2 * n.succ)).LinSols) (h : ConstAbsSorted A.val)
     (i : Fin n.succ) :
@@ -265,7 +263,7 @@ theorem boundary_value_even (S : (PureU1 (2 * n.succ)).LinSols) (hs : ConstAbs S
   have h2 := ConstAbsSorted.AFL_even_above (sortAFL S) hS
   rw [sortAFL_val] at h1 h2
   rw [h1, h2]
-  simp
+  exact (InvolutiveNeg.neg_neg (sort S.val _)).symm
 
 end ConstAbs
 

HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean

@@ -56,8 +56,7 @@ lemma ext_δ (S T : Fin (2 * n.succ) → ℚ) (h1 : ∀ i, S (δ₁ i) = T (δ
   by_cases hi : i.val < n.succ
   · let j : Fin n.succ := ⟨i, hi⟩
     have h2 := h1 j
-    have h3 : δ₁ j = i := by
-      simp [δ₁, Fin.ext_iff]
+    have h3 : δ₁ j = i := rfl
     rw [h3] at h2
     exact h2
   · let j : Fin n.succ := ⟨i - n.succ, by omega⟩
@@ -72,10 +71,9 @@ lemma sum_δ₁_δ₂ (S : Fin (2 * n.succ) → ℚ) :
     ∑ i, S i = ∑ i : Fin n.succ, ((S ∘ δ₁) i + (S ∘ δ₂) i) := by
   have h1 : ∑ i, S i = ∑ i : Fin (n.succ + n.succ), S (Fin.cast (split_equal n.succ) i) := by
     rw [Finset.sum_equiv (Fin.castOrderIso (split_equal n.succ)).symm.toEquiv]
-    intro i
-    simp only [mem_univ, Fin.symm_castOrderIso, RelIso.coe_fn_toEquiv]
-    intro i
-    simp
+    · intro i
+      simp only [mem_univ, Fin.symm_castOrderIso, RelIso.coe_fn_toEquiv]
+    · exact fun _ _=> rfl
   rw [h1]
   rw [Fin.sum_univ_add, Finset.sum_add_distrib]
   rfl
@@ -84,10 +82,9 @@ lemma sum_δ₁_δ₂' (S : Fin (2 * n.succ) → ℚ) :
     ∑ i, S i = ∑ i : Fin n.succ, ((S ∘ δ₁) i + (S ∘ δ₂) i) := by
   have h1 : ∑ i, S i = ∑ i : Fin (n.succ + n.succ), S (Fin.cast (split_equal n.succ) i) := by
     rw [Finset.sum_equiv (Fin.castOrderIso (split_equal n.succ)).symm.toEquiv]
-    intro i
-    simp only [mem_univ, Fin.symm_castOrderIso, RelIso.coe_fn_toEquiv]
-    intro i
-    simp
+    · intro i
+      simp only [mem_univ, Fin.symm_castOrderIso, RelIso.coe_fn_toEquiv]
+    · exact fun _ _ => rfl
   rw [h1]
   rw [Fin.sum_univ_add, Finset.sum_add_distrib]
   rfl
@@ -96,10 +93,9 @@ lemma sum_δ!₁_δ!₂ (S : Fin (2 * n.succ) → ℚ) :
     ∑ i, S i = S δ!₃ + S δ!₄ + ∑ i : Fin n, ((S ∘ δ!₁) i + (S ∘ δ!₂) i) := by
   have h1 : ∑ i, S i = ∑ i : Fin (1 + ((n + n) + 1)), S (Fin.cast (n_cond₂ n) i) := by
     rw [Finset.sum_equiv (Fin.castOrderIso (n_cond₂ n)).symm.toEquiv]
-    intro i
-    simp only [mem_univ, Fin.symm_castOrderIso, RelIso.coe_fn_toEquiv]
-    intro i
-    simp
+    · intro i
+      simp only [mem_univ, Fin.symm_castOrderIso, RelIso.coe_fn_toEquiv]
+    · exact fun _ _ => rfl
   rw [h1]
   rw [Fin.sum_univ_add, Fin.sum_univ_add, Fin.sum_univ_add, Finset.sum_add_distrib]
   simp only [univ_unique, Fin.default_eq_zero, Fin.isValue, sum_singleton, Function.comp_apply]
@@ -112,12 +108,12 @@ lemma sum_δ!₁_δ!₂ (S : Fin (2 * n.succ) → ℚ) :
   nth_rewrite 2 [Rat.add_comm]
   rfl
 
-lemma δ!₃_δ₁0 : @δ!₃ n = δ₁ 0 := by
-  rfl
+lemma δ!₃_δ₁0 : @δ!₃ n = δ₁ 0 := rfl
 
 lemma δ!₄_δ₂Last: @δ!₄ n = δ₂ (Fin.last n) := by
   rw [Fin.ext_iff]
-  simp [δ!₄, δ₂]
+  simp only [succ_eq_add_one, δ!₄, Fin.isValue, Fin.coe_cast, Fin.coe_natAdd, Fin.coe_fin_one,
+    add_zero, δ₂, Fin.natAdd_last, Fin.val_last]
   omega
 
 lemma δ!₁_δ₁ (j : Fin n) : δ!₁ j = δ₁ j.succ := by
@@ -367,10 +363,10 @@ lemma P_δ₁ (f : Fin n.succ → ℚ) (j : Fin n.succ) : P f (δ₁ j) = f j :=
   simp [HSMul.hSMul, SMul.smul]
   rw [Finset.sum_eq_single j]
   · rw [basis_on_δ₁_self]
-    simp only [mul_one]
+    exact Rat.mul_one (f j)
   · intro k _ hkj
     rw [basis_on_δ₁_other hkj]
-    simp only [mul_zero]
+    exact Rat.mul_zero (f k)
   · simp only [mem_univ, not_true_eq_false, _root_.mul_eq_zero, IsEmpty.forall_iff]
 
 lemma P!_δ!₁ (f : Fin n → ℚ) (j : Fin n) : P! f (δ!₁ j) = f j := by
@@ -378,10 +374,10 @@ lemma P!_δ!₁ (f : Fin n → ℚ) (j : Fin n) : P! f (δ!₁ j) = f j := by
   simp [HSMul.hSMul, SMul.smul]
   rw [Finset.sum_eq_single j]
   · rw [basis!_on_δ!₁_self]
-    simp only [mul_one]
+    exact Rat.mul_one (f j)
   · intro k _ hkj
     rw [basis!_on_δ!₁_other hkj]
-    simp only [mul_zero]
+    exact Rat.mul_zero (f k)
   · simp only [mem_univ, not_true_eq_false, _root_.mul_eq_zero, IsEmpty.forall_iff]
 
 lemma Pa_δ!₁ (f : Fin n.succ → ℚ) (g : Fin n → ℚ) (j : Fin n) :
@@ -404,10 +400,10 @@ lemma P!_δ!₂ (f : Fin n → ℚ) (j : Fin n) : P! f (δ!₂ j) = - f j := by
   simp [HSMul.hSMul, SMul.smul]
   rw [Finset.sum_eq_single j]
   · rw [basis!_on_δ!₂_self]
-    simp only [mul_neg, mul_one]
+    exact mul_neg_one (f j)
   · intro k _ hkj
     rw [basis!_on_δ!₂_other hkj]
-    simp only [mul_zero]
+    exact Rat.mul_zero (f k)
   · simp
 
 lemma Pa_δ!₂ (f : Fin n.succ → ℚ) (g : Fin n → ℚ) (j : Fin n) :
@@ -425,7 +421,7 @@ lemma Pa_δ!₃ (f : Fin n.succ → ℚ) (g : Fin n → ℚ) : Pa f g (δ!₃) =
   rw [Pa]
   simp only [ACCSystemCharges.chargesAddCommMonoid_add]
   rw [P!_δ!₃, δ!₃_δ₁0, P_δ₁]
-  simp
+  exact Rat.add_zero (f 0)
 
 lemma P!_δ!₄ (f : Fin n → ℚ) : P! f (δ!₄) = 0 := by
   rw [P!, sum_of_charges]
@@ -435,7 +431,7 @@ lemma Pa_δ!₄ (f : Fin n.succ → ℚ) (g : Fin n → ℚ) : Pa f g (δ!₄) =
   rw [Pa]
   simp only [ACCSystemCharges.chargesAddCommMonoid_add]
   rw [P!_δ!₄, δ!₄_δ₂Last, P_δ₂]
-  simp
+  exact Rat.add_zero (-f (Fin.last n))
 
 lemma P_δ₁_δ₂ (f : Fin n.succ → ℚ) : P f ∘ δ₂ = - P f ∘ δ₁ := by
   funext j
@@ -515,18 +511,17 @@ lemma Pa_zero (f : Fin n.succ → ℚ) (g : Fin n → ℚ) (h : Pa f g = 0) :
     induction iv
     exact h₃.symm
     rename_i iv hi
-    have hivi : iv < n.succ := by omega
+    have hivi : iv < n.succ := lt_of_succ_lt hiv
     have hi2 := hi hivi
-    have h1 := Pa_δ!₁ f g ⟨iv, by omega⟩
-    have h2 := Pa_δ!₂ f g ⟨iv, by omega⟩
+    have h1 := Pa_δ!₁ f g ⟨iv, succ_lt_succ_iff.mp hiv⟩
+    have h2 := Pa_δ!₂ f g ⟨iv, succ_lt_succ_iff.mp hiv⟩
     rw [h] at h1 h2
     simp at h1 h2
     erw [hi2] at h2
     change 0 = _ at h2
     simp at h2
     rw [h2] at h1
-    simp at h1
-    exact h1.symm
+    exact self_eq_add_left.mp h1
   exact hinduc i.val i.prop
 
 lemma Pa_zero! (f : Fin n.succ → ℚ) (g : Fin n → ℚ) (h : Pa f g = 0) :
@@ -554,21 +549,22 @@ lemma P'_val (f : Fin n.succ → ℚ) : (P' f).val = P f := by
   simp [P', P]
   funext i
   rw [sum_of_anomaly_free_linear, sum_of_charges]
-  simp [HSMul.hSMul]
+  rfl
 
 lemma P!'_val (f : Fin n → ℚ) : (P!' f).val = P! f := by
   simp [P!', P!]
   funext i
   rw [sum_of_anomaly_free_linear, sum_of_charges]
-  simp [HSMul.hSMul]
+  rfl
 
 theorem basis_linear_independent : LinearIndependent ℚ (@basis n) := by
   apply Fintype.linearIndependent_iff.mpr
   intro f h
   change P' f = 0 at h
-  have h1 : (P' f).val = 0 := by
-    simp [h]
-    rfl
+  have h1 : (P' f).val = 0 :=
+    (AddSemiconjBy.eq_zero_iff (ACCSystemLinear.LinSols.val 0)
+    (congrFun (congrArg HAdd.hAdd (congrArg ACCSystemLinear.LinSols.val (id (Eq.symm h))))
+    (ACCSystemLinear.LinSols.val 0))).mp rfl
   rw [P'_val] at h1
   exact P_zero f h1
 
@@ -576,9 +572,10 @@ theorem basis!_linear_independent : LinearIndependent ℚ (@basis! n) := by
   apply Fintype.linearIndependent_iff.mpr
   intro f h
   change P!' f = 0 at h
-  have h1 : (P!' f).val = 0 := by
-    simp [h]
-    rfl
+  have h1 : (P!' f).val = 0 :=
+    (AddSemiconjBy.eq_zero_iff (ACCSystemLinear.LinSols.val 0)
+    (congrFun (congrArg HAdd.hAdd (congrArg ACCSystemLinear.LinSols.val (id (Eq.symm h))))
+    (ACCSystemLinear.LinSols.val 0))).mp rfl
   rw [P!'_val] at h1
   exact P!_zero f h1
 
@@ -586,9 +583,10 @@ theorem basisa_linear_independent : LinearIndependent ℚ (@basisa n) := by
   apply Fintype.linearIndependent_iff.mpr
   intro f h
   change Pa' f = 0 at h
-  have h1 : (Pa' f).val = 0 := by
-    simp [h]
-    rfl
+  have h1 : (Pa' f).val = 0 :=
+    (AddSemiconjBy.eq_zero_iff (ACCSystemLinear.LinSols.val 0)
+    (congrFun (congrArg HAdd.hAdd (congrArg ACCSystemLinear.LinSols.val (id (Eq.symm h))))
+    (ACCSystemLinear.LinSols.val 0))).mp rfl
   rw [Pa'_P'_P!'] at h1
   change (P' (f ∘ Sum.inl)).val + (P!' (f ∘ Sum.inr)).val = 0 at h1
   rw [P!'_val, P'_val] at h1
@@ -650,7 +648,7 @@ lemma basisa_card : Fintype.card ((Fin n.succ) ⊕ (Fin n)) =
     FiniteDimensional.finrank ℚ (PureU1 (2 * n.succ)).LinSols := by
   erw [BasisLinear.finrank_AnomalyFreeLinear]
   simp only [Fintype.card_sum, Fintype.card_fin, mul_eq]
-  omega
+  exact split_odd n
 
 /-- The basis formed out of our `basisa` vectors. -/
 noncomputable def basisaAsBasis :
@@ -728,7 +726,6 @@ lemma vectorLikeEven_in_span (S : (PureU1 (2 * n.succ)).LinSols)
       rw [ht]
       ring
     rw [h]
-    simp
     rfl
 
 end VectorLikeEvenPlane

HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean

@@ -62,7 +62,7 @@ lemma lineInPlaneCond_eq_last' {S : (PureU1 (n.succ.succ)).LinSols} (hS : LineIn
   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]; simp)
+      (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
@@ -124,9 +124,9 @@ lemma linesInPlane_four (S : (PureU1 4).Sols) (hS : LineInPlaneCond S.1.1) :
   rw [Fin.sum_univ_four] at hLin hcube
   rw [sq_eq_sq_iff_eq_or_eq_neg] at hn
   simp [not_or] at hn
-  have l012 := hS 0 1 2 (by simp) (by simp) (by simp)
-  have l013 := hS 0 1 3 (by simp) (by simp) (by simp)
-  have l023 := hS 0 2 3 (by simp) (by simp) (by simp)
+  have l012 := hS 0 1 2 (ne_of_beq_false rfl) (ne_of_beq_false rfl) (ne_of_beq_false rfl)
+  have l013 := hS 0 1 3 (ne_of_beq_false rfl) (ne_of_beq_false rfl) (ne_of_beq_false rfl)
+  have l023 := hS 0 2 3 (ne_of_beq_false rfl) (ne_of_beq_false rfl) (ne_of_beq_false rfl)
   simp_all [LineInPlaneProp]
   have h1 : S.val (2 : Fin 4) = S.val (3 : Fin 4) := by
     linear_combination l012 / 2 + -1 * l013 / 2
@@ -158,7 +158,7 @@ lemma linesInPlane_four (S : (PureU1 4).Sols) (hS : LineInPlaneCond S.1.1) :
 lemma linesInPlane_eq_sq_four {S : (PureU1 4).Sols}
     (hS : LineInPlaneCond S.1.1) : ∀ (i j : Fin 4) (_ : i ≠ j),
     ConstAbsProp (S.val i, S.val j) := by
-  refine Prop_two ConstAbsProp (by simp : (0 : Fin 4) ≠ 1) ?_
+  refine Prop_two ConstAbsProp Fin.zero_ne_one ?_
   intro M
   let S' := (FamilyPermutations 4).solAction.toFun S M
   have hS' : LineInPlaneCond S'.1.1 :=

HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean

@@ -82,16 +82,16 @@ lemma δa₁_δ!₃ : @δa₁ n = δ!₃ := by
 lemma δa₂_δ₁ (j : Fin n) : δa₂ j = δ₁ j.succ := by
   rw [Fin.ext_iff]
   simp [δa₂, δ₁]
-  omega
+  exact Nat.add_comm 1 ↑j
 
 lemma δa₂_δ!₁ (j : Fin n) : δa₂ j = δ!₁ j.castSucc := by
   rw [Fin.ext_iff]
-  simp [δa₂, δ!₁]
+  rfl
 
 lemma δa₃_δ₃ : @δa₃ n = δ₃ := by
   rw [Fin.ext_iff]
   simp [δa₃, δ₃]
-  omega
+  exact Nat.add_comm 1 n
 
 lemma δa₃_δ!₁ : δa₃ = δ!₁ (Fin.last n) := by
   rfl
@@ -99,26 +99,24 @@ lemma δa₃_δ!₁ : δa₃ = δ!₁ (Fin.last n) := by
 lemma δa₄_δ₂ (j : Fin n.succ) : δa₄ j = δ₂ j := by
   rw [Fin.ext_iff]
   simp [δa₄, δ₂]
-  omega
+  exact Nat.add_comm 1 n
 
 lemma δa₄_δ!₂ (j : Fin n.succ) : δa₄ j = δ!₂ j := by
   rw [Fin.ext_iff]
-  simp [δa₄, δ!₂]
-  omega
+  rfl
 
 lemma δ₂_δ!₂ (j : Fin n) : δ₂ j = δ!₂ j := by
   rw [Fin.ext_iff]
   simp [δ₂, δ!₂]
-  omega
+  exact Nat.add_comm n 1
 
 lemma sum_δ (S : Fin (2 * n + 1) → ℚ) :
     ∑ i, S i = S δ₃ + ∑ i : Fin n, ((S ∘ δ₁) i + (S ∘ δ₂) i) := by
   have h1 : ∑ i, S i = ∑ i : Fin (n + 1 + n), S (Fin.cast (split_odd n) i) := by
     rw [Finset.sum_equiv (Fin.castOrderIso (split_odd n)).symm.toEquiv]
-    intro i
-    simp only [mem_univ, Fin.symm_castOrderIso, RelIso.coe_fn_toEquiv]
-    intro i
-    simp
+    · intro i
+      simp only [mem_univ, Fin.symm_castOrderIso, RelIso.coe_fn_toEquiv]
+    · exact fun _ _ => rfl
   rw [h1]
   rw [Fin.sum_univ_add, Fin.sum_univ_add]
   simp only [univ_unique, Fin.default_eq_zero, Fin.isValue, sum_singleton, Function.comp_apply]
@@ -131,15 +129,12 @@ lemma sum_δ! (S : Fin (2 * n + 1) → ℚ) :
     ∑ i, S i = S δ!₃ + ∑ i : Fin n, ((S ∘ δ!₁) i + (S ∘ δ!₂) i) := by
   have h1 : ∑ i, S i = ∑ i : Fin ((1+n)+n), S (Fin.cast (split_odd! n) i) := by
     rw [Finset.sum_equiv (Fin.castOrderIso (split_odd! n)).symm.toEquiv]
-    intro i
-    simp only [mem_univ, Fin.castOrderIso, RelIso.coe_fn_toEquiv]
-    intro i
-    simp
-  rw [h1]
-  rw [Fin.sum_univ_add, Fin.sum_univ_add]
+    · intro i
+      simp only [mem_univ, Fin.castOrderIso, RelIso.coe_fn_toEquiv]
+    · exact fun _ _ => rfl
+  rw [h1, Fin.sum_univ_add, Fin.sum_univ_add]
   simp only [univ_unique, Fin.default_eq_zero, Fin.isValue, sum_singleton, Function.comp_apply]
-  rw [add_assoc]
-  rw [Finset.sum_add_distrib]
+  rw [add_assoc, Finset.sum_add_distrib]
   rfl
 
 end theDeltas
@@ -363,10 +358,10 @@ lemma P_δ₁ (f : Fin n → ℚ) (j : Fin n) : P f (δ₁ j) = f j := by
   simp [HSMul.hSMul, SMul.smul]
   rw [Finset.sum_eq_single j]
   · rw [basis_on_δ₁_self]
-    simp only [mul_one]
+    exact Rat.mul_one (f j)
   · intro k _ hkj
     rw [basis_on_δ₁_other hkj]
-    simp only [mul_zero]
+    exact Rat.mul_zero (f k)
   · simp only [mem_univ, not_true_eq_false, _root_.mul_eq_zero, IsEmpty.forall_iff]
 
 lemma P!_δ!₁ (f : Fin n → ℚ) (j : Fin n) : P! f (δ!₁ j) = f j := by
@@ -374,10 +369,10 @@ lemma P!_δ!₁ (f : Fin n → ℚ) (j : Fin n) : P! f (δ!₁ j) = f j := by
   simp [HSMul.hSMul, SMul.smul]
   rw [Finset.sum_eq_single j]
   · rw [basis!_on_δ!₁_self]
-    simp only [mul_one]
+    exact Rat.mul_one (f j)
   · intro k _ hkj
     rw [basis!_on_δ!₁_other hkj]
-    simp only [mul_zero]
+    exact Rat.mul_zero (f k)
   · simp only [mem_univ, not_true_eq_false, _root_.mul_eq_zero, IsEmpty.forall_iff]
 
 lemma P_δ₂ (f : Fin n → ℚ) (j : Fin n) : P f (δ₂ j) = - f j := by
@@ -385,10 +380,10 @@ lemma P_δ₂ (f : Fin n → ℚ) (j : Fin n) : P f (δ₂ j) = - f j := by
   simp [HSMul.hSMul, SMul.smul]
   rw [Finset.sum_eq_single j]
   · rw [basis_on_δ₂_self]
-    simp only [mul_neg, mul_one]
+    exact mul_neg_one (f j)
   · intro k _ hkj
     rw [basis_on_δ₂_other hkj]
-    simp only [mul_zero]
+    exact Rat.mul_zero (f k)
   · simp
 
 lemma P!_δ!₂ (f : Fin n → ℚ) (j : Fin n) : P! f (δ!₂ j) = - f j := by
@@ -396,10 +391,10 @@ lemma P!_δ!₂ (f : Fin n → ℚ) (j : Fin n) : P! f (δ!₂ j) = - f j := by
   simp [HSMul.hSMul, SMul.smul]
   rw [Finset.sum_eq_single j]
   · rw [basis!_on_δ!₂_self]
-    simp only [mul_neg, mul_one]
+    exact mul_neg_one (f j)
   · intro k _ hkj
     rw [basis!_on_δ!₂_other hkj]
-    simp only [mul_zero]
+    exact Rat.mul_zero (f k)
   · simp
 
 lemma P_δ₃ (f : Fin n → ℚ) : P f (δ₃) = 0 := by
@@ -416,7 +411,7 @@ lemma Pa_δa₁ (f g : Fin n.succ → ℚ) : Pa f g δa₁ = f 0 := by
   nth_rewrite 1 [δa₁_δ₁]
   rw [δa₁_δ!₃]
   rw [P_δ₁, P!_δ!₃]
-  simp
+  exact Rat.add_zero (f 0)
 
 lemma Pa_δa₂ (f g : Fin n.succ → ℚ) (j : Fin n) : Pa f g (δa₂ j) = f j.succ + g j.castSucc := by
   rw [Pa]
@@ -431,7 +426,7 @@ lemma Pa_δa₃ (f g : Fin n.succ → ℚ) : Pa f g (δa₃) = g (Fin.last n) :=
   nth_rewrite 1 [δa₃_δ₃]
   rw [δa₃_δ!₁]
   rw [P_δ₃, P!_δ!₁]
-  simp
+  exact Rat.zero_add (g (Fin.last n))
 
 lemma Pa_δa₄ (f g : Fin n.succ → ℚ) (j : Fin n.succ) : Pa f g (δa₄ j) = - f j - g j := by
   rw [Pa]
@@ -506,13 +501,13 @@ lemma Pa_zero (f g : Fin n.succ → ℚ) (h : Pa f g = 0) :
     induction iv
     exact h₃.symm
     rename_i iv hi
-    have hivi : iv < n.succ := by omega
+    have hivi : iv < n.succ := lt_of_succ_lt hiv
     have hi2 := hi hivi
     have h1 := Pa_δa₄ f g ⟨iv, hivi⟩
     rw [h, hi2] at h1
     change 0 = _ at h1
     simp at h1
-    have h2 := Pa_δa₂ f g ⟨iv, by omega⟩
+    have h2 := Pa_δa₂ f g ⟨iv, succ_lt_succ_iff.mp hiv⟩
     simp [h, h1] at h2
     exact h2.symm
   exact hinduc i.val i.prop
@@ -542,21 +537,22 @@ lemma P'_val (f : Fin n → ℚ) : (P' f).val = P f := by
   simp [P', P]
   funext i
   rw [sum_of_anomaly_free_linear, sum_of_charges]
-  simp [HSMul.hSMul]
+  rfl
 
 lemma P!'_val (f : Fin n → ℚ) : (P!' f).val = P! f := by
   simp [P!', P!]
   funext i
   rw [sum_of_anomaly_free_linear, sum_of_charges]
-  simp [HSMul.hSMul]
+  rfl
 
 theorem basis_linear_independent : LinearIndependent ℚ (@basis n) := by
   apply Fintype.linearIndependent_iff.mpr
   intro f h
   change P' f = 0 at h
-  have h1 : (P' f).val = 0 := by
-    simp [h]
-    rfl
+  have h1 : (P' f).val = 0 :=
+    (AddSemiconjBy.eq_zero_iff (ACCSystemLinear.LinSols.val 0)
+    (congrFun (congrArg HAdd.hAdd (congrArg ACCSystemLinear.LinSols.val (id (Eq.symm h))))
+    (ACCSystemLinear.LinSols.val 0))).mp rfl
   rw [P'_val] at h1
   exact P_zero f h1
 
@@ -564,9 +560,10 @@ theorem basis!_linear_independent : LinearIndependent ℚ (@basis! n) := by
   apply Fintype.linearIndependent_iff.mpr
   intro f h
   change P!' f = 0 at h
-  have h1 : (P!' f).val = 0 := by
-    simp [h]
-    rfl
+  have h1 : (P!' f).val = 0 :=
+    (AddSemiconjBy.eq_zero_iff (ACCSystemLinear.LinSols.val 0)
+    (congrFun (congrArg HAdd.hAdd (congrArg ACCSystemLinear.LinSols.val (id (Eq.symm h))))
+    (ACCSystemLinear.LinSols.val 0))).mp rfl
   rw [P!'_val] at h1
   exact P!_zero f h1
 
@@ -574,9 +571,10 @@ theorem basisa_linear_independent : LinearIndependent ℚ (@basisa n.succ) := by
   apply Fintype.linearIndependent_iff.mpr
   intro f h
   change Pa' f = 0 at h
-  have h1 : (Pa' f).val = 0 := by
-    simp [h]
-    rfl
+  have h1 : (Pa' f).val = 0 :=
+    (AddSemiconjBy.eq_zero_iff (ACCSystemLinear.LinSols.val 0)
+    (congrFun (congrArg HAdd.hAdd (congrArg ACCSystemLinear.LinSols.val (id (Eq.symm h))))
+    (ACCSystemLinear.LinSols.val 0))).mp rfl
   rw [Pa'_P'_P!'] at h1
   change (P' (f ∘ Sum.inl)).val + (P!' (f ∘ Sum.inr)).val = 0 at h1
   rw [P!'_val, P'_val] at h1
@@ -643,7 +641,7 @@ lemma basisa_card : Fintype.card ((Fin n.succ) ⊕ (Fin n.succ)) =
     FiniteDimensional.finrank ℚ (PureU1 (2 * n.succ + 1)).LinSols := by
   erw [BasisLinear.finrank_AnomalyFreeLinear]
   simp only [Fintype.card_sum, Fintype.card_fin]
-  omega
+  exact Eq.symm (Nat.two_mul n.succ)
 
 /-- The basis formed out of our basisa vectors. -/
 noncomputable def basisaAsBasis :

HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean

@@ -73,15 +73,8 @@ lemma lineInCubicPerm_self {S : (PureU1 (2 * n + 1)).LinSols} (hS : LineInCubicP
 /-- If `lineInCubicPerm S`, then `lineInCubicPerm (M S)` for all permutations `M`. -/
 lemma lineInCubicPerm_permute {S : (PureU1 (2 * n + 1)).LinSols}
     (hS : LineInCubicPerm S) (M' : (FamilyPermutations (2 * n + 1)).group) :
-    LineInCubicPerm ((FamilyPermutations (2 * n + 1)).linSolRep M' S) := by
-  rw [LineInCubicPerm]
-  intro M
-  have ht : ((FamilyPermutations (2 * n + 1)).linSolRep M)
-    ((FamilyPermutations (2 * n + 1)).linSolRep M' S)
-    = (FamilyPermutations (2 * n + 1)).linSolRep (M * M') S := by
-    simp [(FamilyPermutations (2 * n.succ)).linSolRep.map_mul']
-  rw [ht]
-  exact hS (M * M')
+    LineInCubicPerm ((FamilyPermutations (2 * n + 1)).linSolRep M' S) :=
+  fun M => hS (M * M')
 
 lemma lineInCubicPerm_swap {S : (PureU1 (2 * n.succ + 1)).LinSols}
     (LIC : LineInCubicPerm S) :
@@ -108,10 +101,7 @@ lemma P_P_P!_accCube' {S : (PureU1 (2 * n.succ.succ + 1)).LinSols}
   rw [P_P_P!_accCube f 0]
   rw [← Pa_δa₁ f g]
   rw [← hS]
-  have ht : δ!₁ (0 : Fin n.succ.succ) = δ₁ 1 := by
-    simp [δ!₁, δ₁]
-    rw [Fin.ext_iff]
-    simp
+  have ht : δ!₁ (0 : Fin n.succ.succ) = δ₁ 1 := rfl
   nth_rewrite 1 [ht]
   rw [P_δ₁]
   have h1 := Pa_δa₁ f g
@@ -125,7 +115,7 @@ lemma P_P_P!_accCube' {S : (PureU1 (2 * n.succ.succ + 1)).LinSols}
   rw [δa₄_δ!₂]
   have h0 : (δa₂ (0 : Fin n.succ)) = δ!₁ 0 := by
     rw [δa₂_δ!₁]
-    simp
+    exact ht
   rw [h0, δa₁_δ!₃]
   ring
 
@@ -149,9 +139,9 @@ lemma lineInCubicPerm_last_perm {S : (PureU1 (2 * n.succ.succ + 1)).LinSols}
     (LIC : LineInCubicPerm S) : LineInPlaneCond S := by
   refine @Prop_three (2 * n.succ.succ + 1) LineInPlaneProp S (δ!₂ 0) (δ!₁ 0)
     δ!₃ ?_ ?_ ?_ ?_
-  · simp [Fin.ext_iff, δ!₂, δ!₁]
-  · simp [Fin.ext_iff, δ!₂, δ!₃]
-  · simp [Fin.ext_iff, δ!₁, δ!₃]
+  · exact ne_of_beq_false rfl
+  · exact ne_of_beq_false rfl
+  · exact ne_of_beq_false rfl
   · exact fun M => lineInCubicPerm_last_cond (lineInCubicPerm_permute LIC M)
 
 lemma lineInCubicPerm_constAbs {S : (PureU1 (2 * n.succ.succ + 1)).LinSols}

HepLean/AnomalyCancellation/PureU1/Permutations.lean

@@ -37,13 +37,8 @@ section Charges
 def chargeMap {n : ℕ} (f : PermGroup n) :
     (PureU1 n).Charges →ₗ[ℚ] (PureU1 n).Charges where
   toFun S := S ∘ f.toFun
-  map_add' S T := by
-    funext i
-    simp
-  map_smul' a S := by
-    funext i
-    simp [HSMul.hSMul]
-    -- rw [show Rat.cast a = a from rfl]
+  map_add' _ _ := rfl
+  map_smul' _ _:= rfl
 
 open PureU1Charges in
 
@@ -51,17 +46,8 @@ open PureU1Charges in
 @[simp]
 def permCharges {n : ℕ} : Representation ℚ (PermGroup n) (PureU1 n).Charges where
   toFun f := chargeMap f⁻¹
-  map_mul' f g := by
-    simp only [PermGroup, mul_inv_rev]
-    apply LinearMap.ext
-    intro S
-    funext i
-    rfl
-  map_one' := by
-    apply LinearMap.ext
-    intro S
-    funext i
-    rfl
+  map_mul' f g := by rfl
+  map_one' := by rfl
 
 lemma accGrav_invariant {n : ℕ} (f : (PermGroup n)) (S : (PureU1 n).Charges) :
     PureU1.accGrav n (permCharges f S) = accGrav n S := by

HepLean/AnomalyCancellation/SM/FamilyMaps.lean

@@ -42,13 +42,8 @@ def chargesMapOfSpeciesMap {n m : ℕ} (f : (SMSpecies n).Charges →ₗ[ℚ] (S
 def speciesFamilyProj {m n : ℕ} (h : n ≤ m) :
     (SMSpecies m).Charges →ₗ[ℚ] (SMSpecies n).Charges where
   toFun S := S ∘ Fin.castLE h
-  map_add' S T := by
-    funext i
-    simp
-  map_smul' a S := by
-    funext i
-    simp [HSMul.hSMul]
-    --rw [show Rat.cast a = a from rfl]
+  map_add' _ _ := rfl
+  map_smul' _ _ := rfl
 
 /-- The projection of the `m`-family charges onto the first `n`-family charges. -/
 def familyProjection {m n : ℕ} (h : n ≤ m) : (SMCharges m).Charges →ₗ[ℚ] (SMCharges n).Charges :=
@@ -77,7 +72,7 @@ def speciesEmbed (m n : ℕ) :
     by_cases hi : i.val < m
     · erw [dif_pos hi, dif_pos hi]
     · erw [dif_neg hi, dif_neg hi]
-      simp
+      exact Eq.symm (Rat.mul_zero a)
 
 /-- The embedding of the `m`-family charges onto the `n`-family charges, with all
 other charges zero. -/
@@ -89,14 +84,9 @@ a universal manor. -/
 @[simps!]
 def speciesFamilyUniversial (n : ℕ) :
     (SMSpecies 1).Charges →ₗ[ℚ] (SMSpecies n).Charges where
-  toFun S _ := S ⟨0, by simp⟩
-  map_add' S T := by
-    funext _
-    simp
-  map_smul' a S := by
-    funext i
-    simp [HSMul.hSMul]
-    --rw [show Rat.cast a = a from rfl]
+  toFun S _ := S ⟨0, Nat.zero_lt_succ 0⟩
+  map_add' _ _ := rfl
+  map_smul' _ _ := rfl
 
 /-- The embedding of the `1`-family charges into the `n`-family charges in
 a universal manor. -/

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

@@ -125,8 +125,7 @@ def bijection : linearParameters ≃ (SMNoGrav 1).LinSols where
       repeat erw [speciesVal]
       simp only [asCharges, neg_add_rev]
       ring
-    · simp only [toSpecies_apply]
-      rfl
+    · rfl
   right_inv S := by
     simp only [Fin.isValue, toSpecies_apply]
     apply ACCSystemLinear.LinSols.ext

HepLean/AnomalyCancellation/SMNu/Basic.lean

@@ -56,7 +56,7 @@ lemma toSMSpecies_toSpecies_inv (i : Fin 6) (f : Fin 6 → Fin n → ℚ) :
   simp
 
 lemma toSpecies_one (S : (SMνCharges 1).Charges) (j : Fin 6) :
-    toSpecies j S ⟨0, by simp⟩ = S j := by
+    toSpecies j S ⟨0, zero_lt_succ 0⟩ = S j := by
   match j with
   | 0 => rfl
   | 1 => rfl

HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean

@@ -141,7 +141,7 @@ lemma sum_familyUniversal_three {n : ℕ} (S : (SMνCharges 1).Charges)
   simp only [SMνSpecies_numberCharges, toSpecies_apply, Fin.zero_eta, Fin.isValue]
   rw [Finset.mul_sum]
   apply Finset.sum_congr
-  · simp only
+  · rfl
   · intro i _
     erw [toSpecies_familyUniversal]
     simp only [SMνSpecies_numberCharges, Fin.zero_eta, Fin.isValue, toSpecies_apply]

HepLean/AnomalyCancellation/SMNu/Ordinary/DimSevenPlane.lean

@@ -279,7 +279,7 @@ lemma B_sum_is_sol (f : Fin 7 → ℚ) : (SM 3).IsSolution (∑ i, f i • B i)
     have h : accGrav (B i) = 0 := by
       fin_cases i <;> rfl
     rw [h]
-    simp)
+    exact DistribMulAction.smul_zero (f i))
     (by
       rw [map_sum]
       apply Fintype.sum_eq_zero
@@ -288,7 +288,7 @@ lemma B_sum_is_sol (f : Fin 7 → ℚ) : (SM 3).IsSolution (∑ i, f i • B i)
       have h : accSU2 (B i) = 0 := by
         fin_cases i <;> rfl
       rw [h]
-      simp)
+      exact DistribMulAction.smul_zero (f i))
     (by
       rw [map_sum]
       apply Fintype.sum_eq_zero
@@ -297,7 +297,7 @@ lemma B_sum_is_sol (f : Fin 7 → ℚ) : (SM 3).IsSolution (∑ i, f i • B i)
       have h : accSU3 (B i) = 0 := by
         fin_cases i <;> rfl
       rw [h]
-      simp)
+      exact DistribMulAction.smul_zero (f i))
     (B_in_accCube f)
   use X
   rfl

HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean

@@ -80,7 +80,7 @@ lemma add_AFL_quad (S : (PlusU1 n).LinSols) (a b : ℚ) :
 lemma add_quad (S : (PlusU1 n).QuadSols) (a b : ℚ) :
     accQuad (a • S.val + b • (BL n).val) = 0 := by
   rw [add_AFL_quad, quadSol S]
-  simp
+  exact Rat.mul_zero (a ^ 2)
 
 /-- The `QuadSol` obtained by adding $B-L$ to a `QuadSol`. -/
 def addQuad (S : (PlusU1 n).QuadSols) (a b : ℚ) : (PlusU1 n).QuadSols :=

HepLean/AnomalyCancellation/SMNu/PlusU1/PlaneNonSols.lean

@@ -85,7 +85,7 @@ lemma Bi_sum_quad (i : Fin 11) (f : Fin 11 → ℚ) :
   · rw [quadBiLin.map_smul₂]
   · intro k hij
     rw [quadBiLin.map_smul₂, Bi_Bj_quad hij.symm]
-    simp
+    exact Rat.mul_zero (f k)
 
 /-- The coefficents of the quadratic equation in our basis. -/
 @[simp]

HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSolToSol.lean

@@ -106,7 +106,7 @@ lemma quadSolToSolInv_1 (S : (PlusU1 n).Sols) :
 lemma quadSolToSolInv_α₁_α₂_zero (S : (PlusU1 n).Sols) (h : α₁ S.1 = 0) :
     α₁ (quadSolToSolInv S).1 = 0 ∧ α₂ (quadSolToSolInv S).1 = 0 := by
   rw [quadSolToSolInv_1, α₂_AF S, h]
-  simp
+  exact Prod.mk_eq_zero.mp rfl
 
 lemma quadSolToSolInv_α₁_α₂_neq_zero (S : (PlusU1 n).Sols) (h : α₁ S.1 ≠ 0) :
     ¬ (α₁ (quadSolToSolInv S).1 = 0 ∧ α₂ (quadSolToSolInv S).1 = 0) := by

HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean

@@ -489,7 +489,7 @@ lemma eq_standParam_of_fstRowThdColRealCond {V : CKMMatrix} (hb : [V]ud ≠ 0
     (hV : FstRowThdColRealCond V) : V = standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) (- arg [V]ub) := by
   have hb' : VubAbs ⟦V⟧ ≠ 1 := by
     rw [ud_us_neq_zero_iff_ub_neq_one] at hb
-    simp [VAbs, hb]
+    exact hb
   have h1 : ofReal (√(VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2) *
     ↑√(VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2)) = ofReal (VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2) := by
     rw [Real.mul_self_sqrt]
@@ -552,16 +552,16 @@ lemma eq_standParam_of_ubOnePhaseCond {V : CKMMatrix} (hV : ubOnePhaseCond V) :
   have h1 : VubAbs ⟦V⟧ = 1 := by
     simp [VAbs]
     rw [hV.2.2.2.1]
-    simp
+    exact AbsoluteValue.map_one Complex.abs
   refine eq_rows V ?_ ?_ hV.2.2.2.2.1
   · funext i
     fin_cases i
     · simp [uRow, standParam, standParamAsMatrix]
       rw [C₁₃_eq_ℂcos_θ₁₃ ⟦V⟧, C₁₃_of_Vub_eq_one h1, hV.1]
-      simp only [ofReal_zero, mul_zero]
+      exact Eq.symm (mul_eq_zero_of_right (cos ↑(θ₁₂ ⟦V⟧)) rfl)
     · simp [uRow, standParam, standParamAsMatrix]
       rw [C₁₃_eq_ℂcos_θ₁₃ ⟦V⟧, C₁₃_of_Vub_eq_one h1, hV.2.1]
-      simp only [ofReal_zero, mul_zero]
+      exact Eq.symm (mul_eq_zero_of_right (sin ↑(θ₁₂ ⟦V⟧)) rfl)
     · simp [uRow, standParam, standParamAsMatrix]
       rw [S₁₃_eq_ℂsin_θ₁₃ ⟦V⟧, S₁₃]
       simp [VAbs]
@@ -589,7 +589,7 @@ lemma eq_standParam_of_ubOnePhaseCond {V : CKMMatrix} (hV : ubOnePhaseCond V) :
       rw [h3, S₂₃_of_Vub_eq_one h1, hV.2.2.2.2.2.2]
     · simp [cRow, standParam, standParamAsMatrix]
       rw [C₁₃_eq_ℂcos_θ₁₃ ⟦V⟧, C₁₃_of_Vub_eq_one h1, hV.2.2.1]
-      simp
+      exact Eq.symm (mul_eq_zero_of_right (sin ↑(θ₂₃ ⟦V⟧)) rfl)
 
 theorem exists_δ₁₃ (V : CKMMatrix) :
     ∃ (δ₃ : ℝ), V ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₃ := by
@@ -639,7 +639,7 @@ theorem eq_standardParameterization_δ₃ (V : CKMMatrix) :
   · simp at h
     have h1 : δ₁₃ ⟦V⟧ = 0 := by
       rw [hSV, δ₁₃, h]
-      simp
+      exact arg_zero
     rw [h1]
     rw [mulExpδ₁₃_on_param_eq_zero_iff, Vs_zero_iff_cos_sin_zero] at h
     refine phaseShiftRelation_equiv.trans hδ₃ ?_

HepLean/Mathematics/LinearMaps.lean

@@ -193,20 +193,15 @@ def mk₃ (f : V × V × V→ ℚ) (map_smul : ∀ a S T L, f (a • S, T, L) =
       rw [swap₁, map_add, swap₁, swap₁ S2 S T])
     (by
       intro L T
-      simp only
-      rw [swap₂])).toLinearMap
+      exact swap₂ S L T)).toLinearMap
   map_add' S1 S2 := by
     apply LinearMap.ext
     intro T
     apply LinearMap.ext
     intro S
-    simp [BiLinearSymm.mk₂, map_add]
-  map_smul' a S := by
-    apply LinearMap.ext
-    intro T
-    apply LinearMap.ext
-    intro L
-    simp [BiLinearSymm.mk₂, map_smul]
+    exact map_add S1 S2 T S
+  map_smul' a S :=
+    LinearMap.ext fun T => LinearMap.ext fun L => map_smul a S T L
   swap₁' := swap₁
   swap₂' := swap₂
 
@@ -248,8 +243,7 @@ lemma map_add₃ (f : TriLinearSymm V) (S T L1 L2 : V) :
 /-- Fixing the second and third input vectors, the resulting linear map. -/
 def toLinear₁ (f : TriLinearSymm V) (T L : V) : V →ₗ[ℚ] ℚ where
   toFun S := f S T L
-  map_add' S1 S2 := by
-    simp only [f.map_add₁]
+  map_add' S1 S2 := map_add₁ f S1 S2 T L
   map_smul' a S := by
     simp only [f.map_smul₁]
     rfl

HepLean/Mathematics/SO3/Basic.lean

@@ -47,13 +47,8 @@ lemma coe_inv (A : SO3) : (A⁻¹).1 = A.1⁻¹:=
 /-- The inclusion of `SO(3)` into `GL (Fin 3) ℝ`. -/
 def toGL : SO(3) →* GL (Fin 3) ℝ where
   toFun A := ⟨A.1, (A⁻¹).1, A.2.2, mul_eq_one_comm.mpr A.2.2⟩
-  map_one' := by
-    simp
-    rfl
-  map_mul' x y := by
-    simp only [_root_.mul_inv_rev, coe_inv]
-    ext
-    rfl
+  map_one' := (GeneralLinearGroup.ext_iff _ 1).mpr fun _=> congrFun rfl
+  map_mul' _ _ := (GeneralLinearGroup.ext_iff _ _).mpr fun _ => congrFun rfl
 
 lemma subtype_val_eq_toGL : (Subtype.val : SO3 → Matrix (Fin 3) (Fin 3) ℝ) =
     Units.val ∘ toGL.toFun :=
@@ -70,14 +65,7 @@ lemma toGL_injective : Function.Injective toGL := by
 def toProd : SO(3) →* (Matrix (Fin 3) (Fin 3) ℝ) × (Matrix (Fin 3) (Fin 3) ℝ)ᵐᵒᵖ :=
   MonoidHom.comp (Units.embedProduct _) toGL
 
-lemma toProd_eq_transpose : toProd A = (A.1, ⟨A.1ᵀ⟩) := by
-  simp only [toProd, Units.embedProduct, coe_units_inv, MulOpposite.op_inv, toGL, coe_inv,
-    MonoidHom.coe_comp, MonoidHom.coe_mk, OneHom.coe_mk, Function.comp_apply, Prod.mk.injEq,
-    true_and]
-  refine MulOpposite.unop_inj.mp ?_
-  simp only [MulOpposite.unop_inv, MulOpposite.unop_op]
-  rw [← coe_inv]
-  rfl
+lemma toProd_eq_transpose : toProd A = (A.1, ⟨A.1ᵀ⟩) := rfl
 
 lemma toProd_injective : Function.Injective toProd := by
   intro A B h
@@ -131,7 +119,7 @@ lemma det_minus_id (A : SO(3)) : det (A.1 - 1) = 0 := by
       _ = det A.1 * det (1 - A.1ᵀ) := by rw [← det_mul, mul_sub, mul_one]
       _ = det (1 - A.1ᵀ) := by simp [A.2.1]
       _ = det (1 - A.1ᵀ)ᵀ := by rw [det_transpose]
-      _ = det (1 - A.1) := by simp
+      _ = det (1 - A.1) := rfl
       _ = det (- (A.1 - 1)) := by simp
       _ = (- 1) ^ 3 * det (A.1 - 1) := by simp only [det_neg, Fintype.card_fin, neg_mul, one_mul]
       _ = - det (A.1 - 1) := by simp [pow_three]
@@ -145,7 +133,7 @@ lemma det_id_minus (A : SO(3)) : det (1 - A.1) = 0 := by
       _ = (- 1) ^ 3 * det (A.1 - 1) := by simp only [det_neg, Fintype.card_fin, neg_mul, one_mul]
       _ = - det (A.1 - 1) := by simp [pow_three]
   rw [h1, det_minus_id]
-  simp only [neg_zero]
+  exact neg_zero
 
 @[simp]
 lemma one_in_spectrum (A : SO(3)) : 1 ∈ spectrum ℝ (A.1) := by

scripts/check_file_imports.lean

@@ -83,7 +83,7 @@ def checkMissingImports (modData : ModuleData) (reqImports : Array Name) :
 
 def main (_ : List String) : IO UInt32 := do
   initSearchPath (← findSysroot)
-  let mods : Name :=  `HepLean
+  let mods : Name := `HepLean
   let imp : Import := {module := mods}
   let mFile ← findOLean imp.module
   unless (← mFile.pathExists) do