refactor: Replace simp proofs

HepLean/SpaceTime/LorentzGroup/Basic.lean

@@ -141,17 +141,17 @@ lemma coe_inv : (Λ⁻¹).1 = Λ.1⁻¹:= (inv_eq_left_inv (mem_iff_dual_mul_sel
 lemma subtype_inv_mul : (Subtype.val Λ)⁻¹ * (Subtype.val Λ) = 1 := by
   trans Subtype.val (Λ⁻¹ * Λ)
   · rw [← coe_inv]
-    simp only [lorentzGroupIsGroup_inv, lorentzGroupIsGroup_mul_coe]
+    rfl
   · rw [inv_mul_self Λ]
-    simp only [lorentzGroupIsGroup_one_coe]
+    rfl
 
 @[simp]
 lemma subtype_mul_inv : (Subtype.val Λ) * (Subtype.val Λ)⁻¹ = 1 := by
   trans Subtype.val (Λ * Λ⁻¹)
   · rw [← coe_inv]
-    simp only [lorentzGroupIsGroup_inv, lorentzGroupIsGroup_mul_coe]
+    rfl
   · rw [mul_inv_self Λ]
-    simp only [lorentzGroupIsGroup_one_coe]
+    rfl
 
 @[simp]
 lemma mul_minkowskiMatrix_mul_transpose :
@@ -198,13 +198,11 @@ embedding.
 def toGL : LorentzGroup d →* GL (Fin 1 ⊕ Fin d) ℝ where
   toFun A := ⟨A.1, (A⁻¹).1, mul_eq_one_comm.mpr $ mem_iff_dual_mul_self.mp A.2,
     mem_iff_dual_mul_self.mp A.2⟩
-  map_one' := by
-    simp
-    rfl
-  map_mul' x y := by
-    simp only [lorentzGroupIsGroup, _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 toGL_injective : Function.Injective (@toGL d) := by
   refine fun A B h => Subtype.eq ?_

HepLean/SpaceTime/LorentzGroup/Boosts.lean

@@ -98,7 +98,7 @@ lemma toMatrix_apply (u v : FuturePointing d) (μ ν : Fin 1 ⊕ Fin d) :
     LinearMap.id_apply, LinearMap.coe_mk, AddHom.coe_mk, basis_left, map_smul, smul_eq_mul, map_neg,
     mul_eq_mul_left_iff]
   ring_nf
-  simp
+  exact (true_or_iff (η μ μ = 0)).mpr trivial
 
 open minkowskiMatrix LorentzVector in
 lemma toMatrix_continuous (u : FuturePointing d) : Continuous (toMatrix u) := by

HepLean/SpaceTime/LorentzGroup/Rotations.lean

@@ -43,13 +43,12 @@ lemma SO3ToMatrix_injective : Function.Injective SO3ToMatrix := by
 space-time rotation. -/
 def SO3ToLorentz : SO(3) →* LorentzGroup 3 where
   toFun A := ⟨SO3ToMatrix A, SO3ToMatrix_in_LorentzGroup A⟩
-  map_one' := by
-    apply Subtype.eq
-    simp only [SO3ToMatrix, Nat.reduceAdd, Matrix.reindex_apply, lorentzGroupIsGroup_one_coe]
-    erw [Matrix.fromBlocks_one]
-  map_mul' A B := by
-    apply Subtype.eq
-    simp [Matrix.fromBlocks_multiply]
+  map_one' := Subtype.eq <|
+    (minkowskiMetric.matrix_eq_iff_eq_forall _ ↑1).mpr fun w => congrFun rfl
+  map_mul' A B := Subtype.eq <| by
+    simp only [SO3ToMatrix, SO3Group_mul_coe, lorentzGroupIsGroup_mul_coe,
+      Matrix.fromBlocks_multiply, mul_one, Matrix.mul_zero, add_zero, Matrix.zero_mul,
+      Matrix.mul_one, zero_add]
 
 end LorentzGroup
 

HepLean/SpaceTime/LorentzTensor/Basic.lean

@@ -133,7 +133,7 @@ lemma trans (h : cX.MapIso e cY) (h' : cY.MapIso e' cZ) :
     cX.MapIso (e.trans e') cZ:= by
   funext a
   subst h h'
-  simp
+  rfl
 
 lemma sum {eX : X ≃ X'} {eY : Y ≃ Y'} (hX : cX.MapIso eX cX') (hY : cY.MapIso eY cY') :
     (cX.sum cY).MapIso (eX.sumCongr eY) (cX'.sum cY') := by
@@ -201,7 +201,7 @@ lemma contrRightAux_comp {V1 V2 V3 V4 V5 : Type} [AddCommMonoid V1] [AddCommMono
   intro x3 x4
   simp [contrRightAux, contrMidAux, contrLeftAux]
   erw [TensorProduct.map_tmul]
-  simp only [LinearMapClass.map_smul, LinearMap.id_coe, id_eq, mk_apply, rid_tmul]
+  rfl
 
 end TensorStructure
 
@@ -646,7 +646,7 @@ lemma contrDual_symm' (μ : 𝓣.Color) (x : 𝓣.ColorModule (𝓣.τ μ))
     (𝓣.contrDual μ) ((𝓣.colorModuleCast (𝓣.τ_involutive μ) y) ⊗ₜ[R] x) := by
   rw [𝓣.contrDual_symm, 𝓣.contrDual_cast (𝓣.τ_involutive μ)]
   congr
-  simp [colorModuleCast]
+  exact (LinearEquiv.eq_symm_apply (𝓣.colorModuleCast (congrArg 𝓣.τ (𝓣.τ_involutive μ)))).mp rfl
 
 lemma contrDual_symm_contrRightAux (h : ν = η) :
     (𝓣.colorModuleCast h) ∘ₗ contrRightAux (𝓣.contrDual μ) =
@@ -660,8 +660,8 @@ lemma contrDual_symm_contrRightAux (h : ν = η) :
   · intro x z
     simp [contrRightAux]
     congr
-    · simp [colorModuleCast]
-    · simp [colorModuleCast]
+    · exact (LinearEquiv.symm_apply_eq (𝓣.colorModuleCast (𝓣.τ_involutive μ))).mp rfl
+    · exact (LinearEquiv.symm_apply_eq (𝓣.colorModuleCast (𝓣.τ_involutive (𝓣.τ μ)))).mp rfl
   · intro x z h1 h2
     simp [add_tmul, LinearMap.map_add, h1, h2]
 

HepLean/SpaceTime/LorentzTensor/Contraction.lean

@@ -81,8 +81,7 @@ lemma trans_mapIso {e : X ≃ Y} {e' : Z ≃ Y}
 lemma mapIso_trans {e : X ≃ Y} {e' : Z ≃ X}
     (h : cX.ContrAll e cY) (h' : cZ.MapIso e' cX) : cZ.ContrAll (e'.trans e) cY := by
   subst h h'
-  funext x
-  simp only [Function.comp_apply, Equiv.coe_trans, Equiv.apply_symm_apply]
+  rfl
 
 end ContrAll
 
@@ -257,7 +256,8 @@ lemma contrAll'_mapIso (e : X ≃ Y) (h : cX.MapIso e cY) :
   rw [𝓣.contrDual_cast (congrFun h.symm y)]
   apply congrArg
   congr 1
-  · simp [colorModuleCast]
+  · exact (LinearEquiv.eq_symm_apply
+      (𝓣.colorModuleCast (congrFun (TensorColor.ColorMap.MapIso.symm h) y))).mp rfl
   · symm
     apply cast_eq_iff_heq.mpr
     simp [colorModuleCast, Equiv.apply_symm_apply]
@@ -281,7 +281,6 @@ def contrAll (e : X ≃ Y) (h : cX.ContrAll e cY) : 𝓣.Tensor cX ⊗[R] 𝓣.T
 lemma contrAll_tmul (e : X ≃ Y) (h : cX.ContrAll e cY) (x : 𝓣.Tensor cX) (y : 𝓣.Tensor cY) :
     𝓣.contrAll e h (x ⊗ₜ[R] y) = 𝓣.contrAll' (x ⊗ₜ[R] ((𝓣.mapIso e.symm h.symm.toMapIso) y)) := by
   rw [contrAll]
-  simp only [LinearMap.coe_comp, Function.comp_apply]
   rfl
 
 @[simp]
@@ -442,7 +441,7 @@ lemma contr_tprod_isEmpty [IsEmpty C] (e : (C ⊕ C) ⊕ P ≃ X) (h : cX.ContrC
   rw [contrAll_tmul, contrAll'_isEmpty_tmul]
   simp only [isEmptyEquiv_tprod, Equiv.refl_symm, mapIso_tprod, Equiv.refl_apply, one_mul]
   erw [isEmptyEquiv_tprod]
-  simp
+  exact MulAction.one_smul ((tprod R) fun p => f (e (Sum.inr p)))
 
 /-- The contraction of indices via `contr` is equivariant. -/
 @[simp]

HepLean/SpaceTime/LorentzTensor/EinsteinNotation/Basic.lean

@@ -73,7 +73,7 @@ noncomputable def einsteinTensor (R : Type) [CommSemiring R] (n : ℕ) : TensorS
         Fintype.total_apply, LinearMap.stdBasis_apply', smul_eq_mul, mul_ite, mul_one, mul_zero,
         Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte, lid_tmul, ite_smul, one_smul, zero_smul]
       rw [if_neg (id (Ne.symm hi))]
-      simp only [tmul_zero]
+      exact tmul_zero (Fin n → R) ((LinearMap.stdBasis R (fun _ => R) x) 1)
 
 namespace einsteinTensor
 

HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean

@@ -119,11 +119,8 @@ def toColor (I : Index X) : X := I.1
 def id (I : Index X) : ℕ := I.2
 
 lemma eq_iff_color_eq_and_id_eq (I J : Index X) : I = J ↔ I.toColor = J.toColor ∧ I.id = J.id := by
-  refine Iff.intro ?_ ?_
-  · intro h
-    simp [h]
-  · intro h
-    cases I
+  refine Iff.intro (fun h => Prod.mk.inj_iff.mp h)  (fun h => ?_)
+  · cases I
     cases J
     simp [toColor, id] at h
     simp [h]

HepLean/SpaceTime/LorentzTensor/IndexNotation/ColorIndexList/ContrPerm.lean

@@ -339,7 +339,7 @@ lemma contrPermEquiv_self_contr {l : ColorIndexList 𝓒} :
 
 @[simp]
 lemma contrPermEquiv_contr_self {l : ColorIndexList 𝓒} :
-    contrPermEquiv (by simp : ContrPerm l.contr l) =
+    contrPermEquiv (self_contr : ContrPerm l.contr l) =
     (Fin.castOrderIso (by simp)).toEquiv := by
   rw [← contrPermEquiv_symm, contrPermEquiv_self_contr]
   rfl

HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexList/Basic.lean

@@ -106,7 +106,7 @@ lemma ext_colorMap_idMap {l l2 : IndexList X} (hl : l.length = l2.length)
   · trans l.idMap ⟨n, h1⟩
     · rfl
     · rw [hi]
-      simp [idMap]
+      rfl
 
 /-- Given a list of indices a subset of `Fin l.numIndices × Index X`
   of pairs of positions in `l` and the corresponding item in `l`. -/
@@ -330,7 +330,7 @@ lemma filter_id_eq_sort (i : Fin l.length) : l.val.filter (fun J => (l.val.get i
   rw [← filter_sort_comm]
   apply List.filter_congr
   intro x _
-  simp [idMap]
+  rfl
 
 end IndexList
 

HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexList/Color.lean

@@ -34,12 +34,10 @@ lemma dual_dual : I.dual.dual = I := by
   rfl
 
 @[simp]
-lemma dual_id : I.dual.id = I.id := by
-  simp [dual, id]
+lemma dual_id : I.dual.id = I.id := rfl
 
 @[simp]
-lemma dual_color : I.dual.toColor = 𝓒.τ I.toColor := by
-  simp [dual, toColor]
+lemma dual_color : I.dual.toColor = 𝓒.τ I.toColor := rfl
 
 end Index
 
@@ -70,7 +68,7 @@ lemma countColorQuot_eq_filter_id_countP (I : Index 𝓒.Color) :
       obtain ⟨left, _⟩ := h_1
       rw [← left]
       rw [𝓒.τ_involutive]
-      simp
+      exact Or.inr rfl
   · intro a_1
     simp_all only [and_true]
     obtain ⟨left, _⟩ := a_1
@@ -79,7 +77,7 @@ lemma countColorQuot_eq_filter_id_countP (I : Index 𝓒.Color) :
     | inr h_1 =>
       simp_all only
       rw [𝓒.τ_involutive]
-      simp
+      exact Or.inr rfl
 
 lemma countColorQuot_eq_filter_color_countP (I : Index 𝓒.Color) :
     l.countColorQuot I =
@@ -119,7 +117,7 @@ lemma countColorQuot_eq_countId_iff_of_isSome (hl : l.OnlyUniqueDuals) (i : Fin
         decide (l.val[↑i].toColor = 𝓒.τ l.val[↑((l.getDual? i).get hi)].toColor)) = true := by
         simpa using h
       erw [hn']
-      simp
+      rfl
 
 lemma countColorQuot_of_countId_zero {I : Index 𝓒.Color} (h : l.countId I = 0) :
     l.countColorQuot I = 0 := by
@@ -141,7 +139,7 @@ lemma countColorQuot_contrIndexList_le_one (I : Index 𝓒.Color) :
 lemma countColorQuot_contrIndexList_eq_zero_or_one (I : Index 𝓒.Color) :
     l.contrIndexList.countColorQuot I = 0 ∨ l.contrIndexList.countColorQuot I = 1 := by
   have h1 := countColorQuot_contrIndexList_le_one l I
-  omega
+  exact Nat.le_one_iff_eq_zero_or_eq_one.mp h1
 
 lemma countColorQuot_contrIndexList_le_countColorQuot (I : Index 𝓒.Color) :
     l.contrIndexList.countColorQuot I ≤ l.countColorQuot I := by
@@ -220,8 +218,7 @@ lemma countSelf_contrIndexList_le_one (I : Index 𝓒.Color) :
 
 lemma countSelf_contrIndexList_eq_zero_or_one (I : Index 𝓒.Color) :
     l.contrIndexList.countSelf I = 0 ∨ l.contrIndexList.countSelf I = 1 := by
-  have h1 := countSelf_contrIndexList_le_one l I
-  omega
+  exact Nat.le_one_iff_eq_zero_or_eq_one.mp (countSelf_contrIndexList_le_one l I)
 
 lemma countSelf_contrIndexList_eq_zero_of_zero (I : Index 𝓒.Color) (h : l.countSelf I = 0) :
     l.contrIndexList.countSelf I = 0 := by
@@ -330,7 +327,7 @@ lemma countSelf_eq_countDual_iff_of_isSome (hl : l.OnlyUniqueDuals)
               exact (𝓒.τ_involutive _).symm
             exact hn hn''
           erw [hm'']
-          simp
+          rfl
         · exact true_iff_iff.mpr hm
       · simp [hm]
         simp [colorMap] at hm
@@ -339,12 +336,12 @@ lemma countSelf_eq_countDual_iff_of_isSome (hl : l.OnlyUniqueDuals)
         simp only [cond_false, ne_eq]
         by_cases hm'' : decide (l.val[↑i].toColor = l.val[↑((l.getDual? i).get hi)].toColor) = true
         · erw [hm'']
-          simp
+          exact Nat.add_one_ne_zero 1
         · have hm''' : decide (l.val[↑i].toColor = l.val[↑((l.getDual? i).get hi)].toColor)
               = false := by
             simpa using hm''
           erw [hm''']
-          simp
+          exact Nat.add_one_ne_zero 0
 
 /-- The condition an index and its' dual, when it exists, have dual colors. -/
 def ColorCond : Prop := Option.map l.colorMap ∘
@@ -376,10 +373,9 @@ lemma iff_withDual :
         simp only [true_and]
         exact hi
       simp only [Function.comp_apply, h'', Option.map_some']
-      rw [show l.getDual? ↑i = some ((l.getDual? i).get hi) by simp]
-      rw [Option.map_some']
+      rw [Option.eq_some_of_isSome hi, Option.map_some']
       simp only [Option.some.injEq]
-      have hii := h ⟨i, by simp [withDual, hi]⟩
+      have hii := h ⟨i, (mem_withDual_iff_isSome l i).mpr hi⟩
       simp at hii
       rw [← hii]
       exact (𝓒.τ_involutive _).symm
@@ -462,14 +458,14 @@ lemma mem_iff_dual_mem (hl : l.OnlyUniqueDuals) (hc : l.ColorCond) (I : Index
   · have hIdd : l.countId I.dual = 2 := by
       rw [← hId]
       apply countId_congr
-      simp
+      rfl
     have hc' := (hc I.dual h hIdd).2
     simp at hc'
     rw [← countSelf_neq_zero]
     rw [← countSelf_neq_zero] at h
     rw [countDual_eq_countSelf_Dual] at hc'
     simp at hc'
-    omega
+    exact Ne.symm (ne_of_ne_of_eq (id (Ne.symm h)) hc')
 
 lemma iff_countColorCond (hl : l.OnlyUniqueDuals) :
     l.ColorCond ↔ ∀ I, l.countSelf I ≠ 0 → l.countId I = 2 → countColorCond l I := by
@@ -511,13 +507,10 @@ lemma inl (hl : (l ++ l2).OnlyUniqueDuals) (h : ColorCond (l ++ l2)) : ColorCond
   simp at hI'
   rw [l2.countColorQuot_of_countId_zero hI2', l2.countSelf_of_countId_zero hI2',
     l2.countDual_of_countId_zero hI2', hI2'] at hI'
-  simp at hI'
-  omega
+  exact hI'
 
-lemma inr (hl : (l ++ l2).OnlyUniqueDuals) (h : ColorCond (l ++ l2)) : ColorCond l2 := by
-  have hs := symm hl h
-  rw [OnlyUniqueDuals.symm] at hl
-  exact inl hl hs
+lemma inr (hl : (l ++ l2).OnlyUniqueDuals) (h : ColorCond (l ++ l2)) : ColorCond l2 :=
+  inl (OnlyUniqueDuals.symm.mp hl) (symm hl h)
 
 lemma swap (hl : (l ++ l2 ++ l3).OnlyUniqueDuals) (h : ColorCond (l ++ l2 ++ l3)) :
     ColorCond (l2 ++ l ++ l3) := by

HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexList/Contraction.lean

@@ -46,7 +46,7 @@ def contrIndexList : IndexList X where
 @[simp]
 lemma contrIndexList_empty : (⟨[]⟩ : IndexList X).contrIndexList = { val := [] } := by
   apply ext
-  simp [contrIndexList]
+  rfl
 
 lemma contrIndexList_val : l.contrIndexList.val =
     l.val.filter (fun I => l.countId I = 1) := by
@@ -81,7 +81,7 @@ lemma contrIndexList_eq_contrIndexList' : l.contrIndexList = l.contrIndexList' :
     rw [hf, ← List.filter_map]
     apply congrArg
     simp [length]
-  · simp only [List.map_ofFn]
+  · exact List.map_ofFn (Subtype.val ∘ ⇑l.withoutDualEquiv) l.val.get
 
 @[simp]
 lemma contrIndexList_length : l.contrIndexList.length = l.withoutDual.card := by
@@ -210,7 +210,7 @@ lemma cons_contrIndexList_of_countId_neq_zero {I : Index X} (h : l.countId I ≠
     · simp only [hI, decide_True, List.countP_cons_of_pos, add_left_eq_self, Bool.not_true,
       Bool.false_and, decide_eq_false_iff_not, countId]
       rw [countId, hI] at h
-      simp only [h, not_false_eq_true]
+      exact h
     · simp only [hI, decide_False, Bool.not_false, Bool.true_and, decide_eq_decide]
       rw [List.countP_cons_of_neg]
       simp only [decide_eq_true_eq]
@@ -230,8 +230,7 @@ lemma mem_contrIndexList_filter {I : Index X} (h : I ∈ l.contrIndexList.val) :
     exact l.mem_contrIndexList_countId h
   have h2 : I ∈ l.val.filter (fun J => I.id = J.id) := by
     simp only [List.mem_filter, decide_True, and_true]
-    simp only [contrIndexList, List.mem_filter, decide_eq_true_eq] at h
-    exact h.1
+    exact List.mem_of_mem_filter h
   rw [List.length_eq_one] at h1
   obtain ⟨J, hJ⟩ := h1
   rw [hJ] at h2
@@ -268,23 +267,23 @@ lemma countId_contrIndexList_zero_of_countId (I : Index X)
     rw [Bool.and_comm]
   · rw [countId_eq_length_filter, List.length_eq_zero] at h
     rw [h]
-    simp only [List.countP_nil]
+    rfl
 
 lemma countId_contrIndexList_le_one (I : Index X) :
     l.contrIndexList.countId I ≤ 1 := by
   by_cases h : l.contrIndexList.countId I = 0
-  · simp [h]
+  · exact StrictMono.minimal_preimage_bot (fun ⦃a b⦄ a => a) h 1
   · obtain ⟨I', hI1, hI2⟩ := countId_neq_zero_mem l.contrIndexList I h
     rw [countId_congr l.contrIndexList hI2, mem_contrIndexList_countId_contrIndexList l hI1]
 
 lemma countId_contrIndexList_eq_one_iff_countId_eq_one (I : Index X) :
     l.contrIndexList.countId I = 1 ↔ l.countId I = 1 := by
   refine Iff.intro (fun h => ?_) (fun h => ?_)
-  · obtain ⟨I', hI1, hI2⟩ := countId_neq_zero_mem l.contrIndexList I (by omega)
+  · obtain ⟨I', hI1, hI2⟩ := countId_neq_zero_mem l.contrIndexList I (ne_zero_of_eq_one h)
     simp [contrIndexList] at hI1
     rw [countId_congr l hI2]
     exact hI1.2
-  · obtain ⟨I', hI1, hI2⟩ := countId_neq_zero_mem l I (by omega)
+  · obtain ⟨I', hI1, hI2⟩ := countId_neq_zero_mem l I (ne_zero_of_eq_one h)
     rw [countId_congr l hI2] at h
     rw [countId_congr _ hI2]
     refine mem_contrIndexList_countId_contrIndexList l ?_

HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexList/CountId.lean

@@ -42,17 +42,14 @@ lemma countId_eq_length_filter (I : Index X) :
   rw [List.countP_eq_length_filter]
 
 lemma countId_index_neq_zero (i : Fin l.length) : l.countId (l.val.get i) ≠ 0 := by
-  rw [countId_eq_length_filter]
   by_contra hn
-  rw [List.length_eq_zero] at hn
-  have hm : l.val.get i ∈ List.filter (fun J => decide ((l.val.get i).id = J.id)) l.val := by
-    simpa using List.getElem_mem l.val i.1 i.isLt
-  rw [hn] at hm
-  simp at hm
+  rw [countId_eq_length_filter, List.length_eq_zero] at hn
+  refine (List.mem_nil_iff (l.val.get i)).mp ?_
+  simpa [← hn] using List.getElem_mem l.val i.1 i.isLt
 
 lemma countId_append_symm (I : Index X) : (l ++ l2).countId I = (l2 ++ l).countId I := by
   simp only [countId_append]
-  omega
+  exact Nat.add_comm (l.countId I) (l2.countId I)
 
 lemma countId_eq_one_append_mem_right_self_eq_one {I : Index X} (hI : I ∈ l2.val)
     (h : (l ++ l2).countId I = 1) : l2.countId I = 1 := by
@@ -64,7 +61,7 @@ lemma countId_eq_one_append_mem_right_self_eq_one {I : Index X} (hI : I ∈ l2.v
     by_contra hn
     rw [@List.length_eq_zero] at hn
     rw [hn] at hmem
-    simp at hmem
+    exact (List.mem_nil_iff I).mp hmem
   omega
 
 lemma countId_eq_one_append_mem_right_other_eq_zero {I : Index X} (hI : I ∈ l2.val)
@@ -77,7 +74,7 @@ lemma countId_eq_one_append_mem_right_other_eq_zero {I : Index X} (hI : I ∈ l2
     by_contra hn
     rw [@List.length_eq_zero] at hn
     rw [hn] at hmem
-    simp at hmem
+    exact (List.mem_nil_iff I).mp hmem
   omega
 
 @[simp]
@@ -106,7 +103,7 @@ lemma countId_mem (I : Index X) (hI : I ∈ l.val) : l.countId I ≠ 0 := by
   have hIme : I ∈ List.filter (fun J => decide (I.id = J.id)) l.val := by
     simp [hI]
   rw [hn] at hIme
-  simp at hIme
+  exact (List.mem_nil_iff I).mp hIme
 
 lemma countId_get_other (i : Fin l.length) : l2.countId (l.val.get i) =
     (List.finRange l2.length).countP (fun j => l.AreDualInOther l2 i j) := by
@@ -117,8 +114,7 @@ lemma countId_get_other (i : Fin l.length) : l2.countId (l.val.get i) =
   nth_rewrite 1 [hl2]
   rw [List.filter_map, List.length_map]
   apply congrArg
-  refine List.filter_congr (fun j _ => ?_)
-  simp [AreDualInOther, idMap]
+  refine List.filter_congr (fun j _ => rfl)
 
 /-! TODO: Replace with mathlib lemma. -/
 lemma filter_finRange (i : Fin l.length) :
@@ -184,7 +180,7 @@ lemma countId_gt_zero_of_mem_withDual (i : Fin l.length) (h : i ∈ l.withDual)
   have hjmem : j ∈ (List.finRange l.length).filter (fun j => decide (l.AreDualInSelf i j)) := by
     simpa using hj
   rw [hn] at hjmem
-  simp at hjmem
+  exact (List.mem_nil_iff j).mp hjmem
 
 lemma countId_of_not_mem_withDual (i : Fin l.length)(h : i ∉ l.withDual) :
     l.countId (l.val.get i) = 1 := by
@@ -217,7 +213,7 @@ lemma countId_neq_zero_of_mem_withDualInOther (i : Fin l.length) (h : i ∈ l.wi
     · exact List.getElem_mem l2.val (↑j) j.isLt
     · simpa [AreDualInOther] using hj
   rw [hn] at hjmem
-  simp at hjmem
+  exact (List.mem_nil_iff (l2.val.get j)).mp hjmem
 
 lemma countId_of_not_mem_withDualInOther (i : Fin l.length) (h : i ∉ l.withDualInOther l2) :
     l2.countId (l.val.get i) = 0 := by
@@ -242,7 +238,7 @@ lemma mem_withDualInOther_iff_countId_neq_zero (i : Fin l.length) :
     (fun h => ?_)
   by_contra hn
   have hn' := countId_of_not_mem_withDualInOther l l2 i hn
-  omega
+  exact h hn'
 
 lemma mem_withoutDual_iff_countId_eq_one (i : Fin l.length) :
     i ∈ l.withoutDual ↔ l.countId (l.val.get i) = 1 := by
@@ -270,10 +266,9 @@ lemma countId_eq_two_of_mem_withUniqueDual (i : Fin l.length) (h : i ∈ l.withU
       apply List.filter_congr (fun j _ => ?_)
       simpa using eq_comm
     trans List.filter (fun j => j = i')
-      ((List.finRange l.length).filter (fun j => (l.AreDualInSelf i j)))
-    · simp
-      apply List.filter_congr (fun j _ => ?_)
-      exact Bool.and_comm (decide (l.AreDualInSelf i j)) (decide (j = i'))
+      ((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
       refine List.filter_congr (fun j _ => ?_)
       simp only [Bool.and_iff_right_iff_imp, decide_eq_true_eq]
@@ -349,7 +344,7 @@ lemma countId_eq_one_of_mem_withUniqueDualInOther (i : Fin l.length)
     have h2 := countId_index_neq_zero l i
     omega
   · rw [countId_get_other, List.countP_eq_length_filter, ← h1]
-    simp
+    rfl
 
 lemma mem_withUniqueDualInOther_of_countId_eq_one (i : Fin l.length)
     (h : l.countId (l.val.get i) = 1 ∧ l2.countId (l.val.get i) = 1) :
@@ -363,7 +358,7 @@ lemma mem_withUniqueDualInOther_of_countId_eq_one (i : Fin l.length)
     omega
   · apply And.intro
     · rw [mem_withDualInOther_iff_countId_neq_zero]
-      omega
+      exact countId_neq_zero_of_mem_withDualInOther l l2 i hw
     · intro j hj
       have h2 := h.2
       rw [countId_get_other l l2, List.countP_eq_length_filter, List.length_eq_one] at h2
@@ -380,7 +375,7 @@ lemma mem_withUniqueDualInOther_of_countId_eq_one (i : Fin l.length)
       rw [ha] at ht
       simp at ht
       subst ht
-      simp
+      exact Option.some_get ((mem_withInDualOther_iff_isSome l l2 i).mp hw)
 
 lemma mem_withUniqueDualInOther_iff_countId_eq_one (i : Fin l.length) :
     i ∈ l.withUniqueDualInOther l2 ↔ l.countId (l.val.get i) = 1 ∧ l2.countId (l.val.get i) = 1 :=
@@ -448,8 +443,7 @@ lemma filter_id_of_countId_eq_one {i : Fin l.length} (h1 : l.countId (l.val.get
   rw [hJ] at hme
   simp only [List.get_eq_getElem, List.mem_singleton] at hme
   erw [hJ]
-  simp only [List.get_eq_getElem, List.cons.injEq, and_true]
-  exact id (Eq.symm hme)
+  exact congrFun (congrArg List.cons (id (Eq.symm hme))) []
 
 lemma filter_id_of_countId_eq_one_mem {I : Index X} (hI : I ∈ l.val) (h : l.countId I = 1) :
     l.val.filter (fun J => I.id = J.id) = [I] := by
@@ -461,8 +455,7 @@ lemma filter_id_of_countId_eq_one_mem {I : Index X} (hI : I ∈ l.val) (h : l.co
   rw [hJ] at hme
   simp only [List.mem_singleton] at hme
   erw [hJ]
-  simp only [List.cons.injEq, and_true]
-  exact id (Eq.symm hme)
+  exact congrFun (congrArg List.cons (id (Eq.symm hme))) []
 
 lemma filter_id_of_countId_eq_two {i : Fin l.length}
     (h : l.countId (l.val.get i) = 2) :
@@ -481,7 +474,7 @@ lemma filter_id_of_countId_eq_two {i : Fin l.length}
         simp only [List.get_eq_getElem, decide_True, List.filter_cons_of_pos, List.cons.injEq,
           List.filter_eq_self, List.mem_singleton, decide_eq_true_eq, forall_eq, true_and]
         change l.idMap i = l.idMap ((l.getDual? i).get (l.getDual?_isSome_of_countId_eq_two h))
-        simp
+        exact Eq.symm (getDual?_get_id l i (getDual?_isSome_of_countId_eq_two l h))
       rw [← h1]
       refine List.Sublist.filter (fun (J : Index X) => ((l.val.get i).id = J.id)) ?_
       rw [List.sublist_iff_exists_fin_orderEmbedding_get_eq]
@@ -495,7 +488,7 @@ lemma filter_id_of_countId_eq_two {i : Fin l.length}
       · intro a
         fin_cases a <;> rfl
     · rw [hc]
-      simp
+      rfl
   · have hi' : ((l.getDual? i).get (l.getDual?_isSome_of_countId_eq_two h)) < i := by
       have h1 := l.getDual?_get_areDualInSelf i (getDual?_isSome_of_countId_eq_two l h)
       simp only [AreDualInSelf] at h1
@@ -509,8 +502,8 @@ lemma filter_id_of_countId_eq_two {i : Fin l.length}
           decide_eq_true_eq, forall_eq_or_imp, forall_eq, and_true]
         apply And.intro
         · change l.idMap i = l.idMap ((l.getDual? i).get (l.getDual?_isSome_of_countId_eq_two h))
-          simp
-        · simp only [List.not_mem_nil, false_implies, implies_true, and_self]
+          exact Eq.symm (getDual?_get_id l i (getDual?_isSome_of_countId_eq_two l h))
+        · exact And.symm (if_false_right.mp trivial)
       rw [← h1]
       refine List.Sublist.filter (fun (J : Index X) => ((l.val.get i).id = J.id)) ?_
       rw [List.sublist_iff_exists_fin_orderEmbedding_get_eq]
@@ -528,7 +521,7 @@ lemma filter_id_of_countId_eq_two {i : Fin l.length}
       · intro a
         fin_cases a <;> rfl
     · rw [hc]
-      simp
+      rfl
 
 end IndexList
 

HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexList/OnlyUniqueDuals.lean

@@ -52,12 +52,10 @@ lemma iff_countId_leq_two :
     l.OnlyUniqueDuals ↔ ∀ i, l.countId (l.val.get i) ≤ 2 := by
   refine Iff.intro (fun h i => ?_) (fun h => ?_)
   · by_cases hi : i ∈ l.withDual
-    · rw [← h] at hi
-      rw [mem_withUniqueDual_iff_countId_eq_two] at hi
+    · rw [← h, mem_withUniqueDual_iff_countId_eq_two] at hi
       rw [hi]
     · rw [mem_withDual_iff_countId_gt_one] at hi
-      simp at hi
-      exact Nat.le_succ_of_le hi
+      exact Nat.le_of_not_ge hi
   · refine Finset.ext (fun i => ?_)
     rw [mem_withUniqueDual_iff_countId_eq_two, mem_withDual_iff_countId_gt_one]
     have hi := h i
@@ -87,14 +85,14 @@ lemma inl (h : (l ++ l2).OnlyUniqueDuals) : l.OnlyUniqueDuals := by
   intro I
   have hI := h I
   simp at hI
-  omega
+  exact Nat.le_of_add_right_le hI
 
 lemma inr (h : (l ++ l2).OnlyUniqueDuals) : l2.OnlyUniqueDuals := by
   rw [iff_countId_leq_two'] at h ⊢
   intro I
   have hI := h I
   simp at hI
-  omega
+  exact le_of_add_le_right hI
 
 lemma symm' (h : (l ++ l2).OnlyUniqueDuals) : (l2 ++ l).OnlyUniqueDuals := by
   rw [iff_countId_leq_two'] at h ⊢
@@ -123,10 +121,7 @@ lemma swap (h : (l ++ l2 ++ l3).OnlyUniqueDuals) : (l2 ++ l ++ l3).OnlyUniqueDua
 
 lemma contrIndexList (h : l.OnlyUniqueDuals) : l.contrIndexList.OnlyUniqueDuals := by
   rw [iff_countId_leq_two'] at h ⊢
-  intro I
-  have hI := h I
-  have h1 := countId_contrIndexList_le_countId l I
-  omega
+  exact fun I => Nat.le_trans (countId_contrIndexList_le_countId l I) (h I)
 
 lemma contrIndexList_left (h1 : (l ++ l2).OnlyUniqueDuals) :
     (l.contrIndexList ++ l2).OnlyUniqueDuals := by
@@ -136,7 +131,7 @@ lemma contrIndexList_left (h1 : (l ++ l2).OnlyUniqueDuals) :
   simp only [countId_append] at hI
   simp only [countId_append, ge_iff_le]
   have h1 := countId_contrIndexList_le_countId l I
-  omega
+  exact add_le_of_add_le_right hI h1
 
 lemma contrIndexList_right (h1 : (l ++ l2).OnlyUniqueDuals) :
     (l ++ l2.contrIndexList).OnlyUniqueDuals := by

HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexList/Subperm.lean

@@ -52,7 +52,7 @@ lemma iff_countId : l.Subperm l2 ↔
       have hi' := h ⟨l.val.indexOf I', hi'⟩
       rw [← hIi'] at hi'
       rw [hi'.1, hi'.2]
-      simp
+      exact if_false_right.mp (congrFun rfl)
   · have hi := h (l.val.get i)
     have h1 : l.countId (l.val.get i) ≠ 0 := countId_index_neq_zero l i
     omega

HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean

@@ -49,7 +49,7 @@ instance : Coe 𝓣.TensorIndex (ColorIndexList 𝓣.toTensorColor) where
   coe T := T.toColorIndexList
 
 lemma colormap_mapIso {T₁ T₂ : 𝓣.TensorIndex} (hi : T₁.toColorIndexList = T₂.toColorIndexList) :
-    ColorMap.MapIso (Fin.castOrderIso (by simp [IndexList.length, hi])).toEquiv
+    ColorMap.MapIso (Fin.castOrderIso (congrArg IndexList.length (congrArg toIndexList hi))).toEquiv
     T₁.colorMap' T₂.colorMap' := by
   cases T₁; cases T₂
   simp [ColorMap.MapIso]

HepLean/SpaceTime/LorentzTensor/MulActionTensor.lean

@@ -60,9 +60,7 @@ def compHom (f : H →* G) : MulActionTensor H 𝓣 where
 /-- The trivial `MulActionTensor` defined via trivial representations. -/
 def trivial : MulActionTensor G 𝓣 where
   repColorModule μ := Representation.trivial R
-  contrDual_inv μ g := by
-    simp only [Representation.trivial, MonoidHom.one_apply, TensorProduct.map_one]
-    rfl
+  contrDual_inv μ g := ext rfl
   metric_inv μ g := by
     simp only [Representation.trivial, MonoidHom.one_apply, TensorProduct.map_one]
     rfl
@@ -101,7 +99,7 @@ lemma colorModuleCast_equivariant_apply (h : μ = ν) (g : G) (x : 𝓣.ColorMod
     (𝓣.colorModuleCast h) (repColorModule μ g x) =
     (repColorModule ν g) (𝓣.colorModuleCast h x) := by
   subst h
-  simp [colorModuleCast]
+  rfl
 
 @[simp]
 lemma contrRightAux_contrDual_equivariant_tmul (g : G) (m : 𝓣.ColorModule ν ⊗[R] 𝓣.ColorModule μ)

HepLean/SpaceTime/LorentzTensor/Real/Basic.lean

@@ -54,8 +54,9 @@ instance : Fintype ColorType where
   complete := by
     intro x
     cases x
-    · simp only [Finset.mem_insert, Finset.mem_singleton, or_false]
-    · simp only [Finset.mem_insert, Finset.mem_singleton, or_true]
+    · exact Finset.mem_insert_self ColorType.up {ColorType.down}
+    · apply Finset.insert_eq_self.mp
+      rfl
 
 end realTensorColor
 

HepLean/SpaceTime/LorentzTensor/RisingLowering.lean

@@ -79,8 +79,7 @@ lemma boolFin'_DualMap {c₁ c₂ : 𝓒.ColorMap (Fin n)} (h : boolFin' c₁ c
   funext x
   exact h x
 
-lemma refl : DualMap c₁ c₁ := by
-  simp [DualMap]
+lemma refl : DualMap c₁ c₁ := rfl
 
 lemma symm (h : DualMap c₁ c₂) : DualMap c₂ c₁ := by
   rw [DualMap] at h ⊢
@@ -155,7 +154,7 @@ lemma unit_lhs_eq (x : 𝓣.ColorModule μ) (y : 𝓣.ColorModule (𝓣.τ μ)
     contrLeftAux (𝓣.contrDual μ) (x ⊗ₜ[R] y) =
     (contrRightAux (𝓣.contrDual (𝓣.τ μ))) ((TensorProduct.comm R _ _) y
     ⊗ₜ[R] (𝓣.colorModuleCast (𝓣.τ_involutive μ).symm) x) := by
-  refine TensorProduct.induction_on y (by simp) ?_ (fun z1 z2 h1 h2 => ?_)
+  refine TensorProduct.induction_on y (by rfl) ?_ (fun z1 z2 h1 h2 => ?_)
   · intro x1 x2
     simp only [contrRightAux, LinearEquiv.refl_toLinearMap, comm_tmul, colorModuleCast,
       Equiv.cast_symm, LinearEquiv.coe_mk, Equiv.cast_apply, LinearMap.coe_comp,
@@ -184,7 +183,7 @@ lemma metric_cast (h : μ = ν) :
     𝓣.metric ν := by
   subst h
   erw [congr_refl_refl]
-  simp only [LinearEquiv.refl_apply]
+  rfl
 
 @[simp]
 lemma metric_contrRight_unit (μ : 𝓣.Color) (x : 𝓣.ColorModule μ) :
@@ -198,7 +197,7 @@ lemma metric_contrRight_unit (μ : 𝓣.Color) (x : 𝓣.ColorModule μ) :
   simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, assoc_symm_tmul,
     map_tmul, LinearMap.id_coe, id_eq]
   rw [𝓣.metric_dual]
-  simp only [unit_lid]
+  exact unit_lid 𝓣
 
 /-!
 
@@ -242,7 +241,8 @@ lemma dualizeModule_equivariant (g : G) :
     LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, colorModuleCast_equivariant_apply,
     lTensorHomToHomLTensor_apply, LinearMap.id_coe, id_eq]
   nth_rewrite 1 [← MulActionTensor.metric_inv (𝓣.τ μ) g]
-  simp
+  exact contrRightAux_contrDual_equivariant_tmul 𝓣 g (𝓣.metric (𝓣.τ μ))
+      ((𝓣.colorModuleCast (dualizeFun.proof_3 𝓣 μ)) x)
 
 @[simp]
 lemma dualizeModule_equivariant_apply (g : G) (x : 𝓣.ColorModule μ) :

HepLean/SpaceTime/LorentzVector/Contraction.lean

@@ -56,8 +56,7 @@ def contrUpDownBi : LorentzVector d →ₗ[ℝ] CovariantLorentzVector d →ₗ[
     rw [Finset.smul_sum]
     refine Finset.sum_congr rfl (fun i _ => ?_)
     simp only [HSMul.hSMul, SMul.smul]
-    simp only [RingHom.id, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk, id_eq]
-    ring
+    exact mul_assoc r (v i) (w i)
 
 /-- The linear map defining the contraction of a contravariant Lorentz vector
   and a covariant Lorentz vector. -/
@@ -185,9 +184,10 @@ lemma asTenProd_diag :
   rw [Finset.sum_eq_single μ]
   · intro ν _ hμν
     rw [minkowskiMatrix.off_diag_zero hμν.symm]
-    simp only [zero_smul]
+    exact TensorProduct.zero_smul (e μ ⊗ₜ[ℝ] e ν)
   · intro a
-    simp_all only
+    rename_i j
+    exact False.elim (a j)
 
 /-- The metric tensor as an element of `CovariantLorentzVector d ⊗[ℝ] CovariantLorentzVector d`. -/
 def asCoTenProd : CovariantLorentzVector d ⊗[ℝ] CovariantLorentzVector d :=

HepLean/SpaceTime/LorentzVector/Covariant.lean

@@ -101,7 +101,7 @@ lemma rep_apply_stdBasis (g : LorentzGroup d) (μ : Fin 1 ⊕ Fin d) :
   simp [LorentzVector.stdBasis, Pi.basisFun_apply]
   erw [Pi.basisFun_apply, Matrix.mulVec_stdBasis]
   rw [← LorentzGroup.coe_inv]
-  simp
+  rfl
 
 end CovariantLorentzVector
 

HepLean/SpaceTime/LorentzVector/LorentzAction.lean

@@ -20,8 +20,7 @@ variable {d : ℕ} (v : LorentzVector d)
 /-- The contravariant action of the Lorentz group on a Lorentz vector. -/
 def rep : Representation ℝ (LorentzGroup d) (LorentzVector d) where
   toFun g := Matrix.toLinAlgEquiv e g
-  map_one' := by
-    simp only [lorentzGroupIsGroup_one_coe, map_one]
+  map_one' := (MulEquivClass.map_eq_one_iff (Matrix.toLinAlgEquiv e)).mpr rfl
   map_mul' x y := by
     simp only [lorentzGroupIsGroup_mul_coe, map_mul]
 

HepLean/SpaceTime/MinkowskiMetric.lean

@@ -45,8 +45,8 @@ lemma sq : @minkowskiMatrix d * minkowskiMatrix = 1 := by
       subst h
       simp_all only [one_apply_eq]
     · simp_all only [ne_eq, Sum.inl.injEq, not_false_eq_true, one_apply_ne]
-  · simp only [ne_eq, not_false_eq_true, diagonal_apply_ne, one_apply_ne]
-  · simp only [ne_eq, not_false_eq_true, diagonal_apply_ne, one_apply_ne]
+  · rfl
+  · rfl
   · simp only [diagonal, of_apply, Sum.inr.injEq, Sum.elim_inr, mul_neg, mul_one, neg_neg]
     split
     · rename_i h
@@ -191,7 +191,7 @@ lemma self_spaceReflection_eq_zero_iff : ⟪v, v.spaceReflection⟫ₘ = 0 ↔ v
       exact h3
     · simpa using congrFun h4 i
   · rw [h]
-    simp only [map_zero, LinearMap.zero_apply]
+    exact LinearMap.map_zero₂ minkowskiMetric (spaceReflection 0)
 /-!
 
 # Non degeneracy of the Minkowski metric
@@ -339,16 +339,7 @@ lemma on_basis (μ ν : Fin 1 ⊕ Fin d) : ⟪e μ, e ν⟫ₘ = η μ ν := by
 lemma matrix_apply_stdBasis (ν μ : Fin 1 ⊕ Fin d) :
     Λ ν μ = η ν ν * ⟪e ν, Λ *ᵥ e μ⟫ₘ := by
   rw [on_basis_mulVec, ← mul_assoc]
-  have h1 : η ν ν * η ν ν = 1 := by
-    simp [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal]
-    rcases μ
-    · rcases ν
-      · simp_all only [Sum.elim_inl, mul_one]
-      · simp_all only [Sum.elim_inr, mul_neg, mul_one, neg_neg]
-    · rcases ν
-      · simp_all only [Sum.elim_inl, mul_one]
-      · simp_all only [Sum.elim_inr, mul_neg, mul_one, neg_neg]
-  simp [h1]
+  simp [η_apply_mul_η_apply_diag ν]
 
 end matrices
 end minkowskiMetric

HepLean/StandardModel/HiggsBoson/GaugeAction.lean

@@ -59,7 +59,7 @@ lemma matrixToLin_unitary (g : unitaryGroup (Fin 2) ℂ) :
     matrixToLin g ∈ unitary (HiggsVec →L[ℂ] HiggsVec) := by
   rw [@unitary.mem_iff, ← matrixToLin_star, ← matrixToLin.map_mul, ← matrixToLin.map_mul,
     mem_unitaryGroup_iff.mp g.prop, mem_unitaryGroup_iff'.mp g.prop, matrixToLin.map_one]
-  simp
+  exact Prod.mk_eq_one.mp rfl
 
 /-- The natural homomorphism from unitary `2×2` complex matrices to unitary transformations
 of `higgsVec`. -/