refactor: replace simps

HepLean/AnomalyCancellation/PureU1/ConstAbs.lean

@@ -121,7 +121,7 @@ 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]; exact le.intro rfl)
@@ -144,7 +144,7 @@ lemma not_hasBoundary_zero_le (hnot : ¬ (HasBoundary S)) (h0 : S (0 : Fin n.suc
   · rfl
   · rename_i i hii
     have hnott := hnot ⟨i, succ_lt_succ_iff.mp hi⟩
-    have hii := hii (by omega)
+    have hii := hii (lt_of_succ_lt hi)
     erw [← hii] at hnott
     exact (val_le_zero hS (hnott h0)).symm
 
@@ -212,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) :
@@ -233,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) :

HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean

@@ -71,9 +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]
-    exact fun _ _=> rfl
+    · 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
@@ -82,9 +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]
-    exact fun _ _ => rfl
+    · 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
@@ -93,9 +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]
-    exact fun _ _ => rfl
+    · 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]
@@ -108,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
@@ -511,10 +511,10 @@ 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
@@ -648,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 :

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

HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean

@@ -82,7 +82,7 @@ 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]
@@ -91,7 +91,7 @@ lemma δa₂_δ!₁ (j : Fin n) : δa₂ j = δ!₁ j.castSucc := by
 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,7 +99,7 @@ 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]
@@ -108,15 +108,15 @@ lemma δa₄_δ!₂ (j : Fin n.succ) : δa₄ j = δ!₂ j := by
 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]
-    exact fun _ _ => rfl
+    · 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]
@@ -129,14 +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]
-    exact fun _ _ => rfl
-  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
@@ -503,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
@@ -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/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/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δ₃ ?_