refactor: golf

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

@@ -52,15 +52,13 @@ lemma getDualInOtherEquiv_eq (h : l.ContrPerm l2) (i : Fin l.contr.length) :
   · trans (l2.contr.colorMap' ∘ Subtype.val ∘ (l.contr.getDualInOtherEquiv l2.contr)) ⟨i, by
       rw [h.2.1]
       exact Finset.mem_univ i⟩
-    · simp
-      rfl
+    · rfl
     · simp only [h.2.2]
       rfl
   · trans l2.contr.idMap (l.contr.getDualInOtherEquiv l2.contr ⟨i, by
       rw [h.2.1]
       exact Finset.mem_univ i⟩).1
-    · simp
-      rfl
+    · rfl
     · simp [getDualInOtherEquiv]
       rfl
 
@@ -83,7 +81,7 @@ lemma countSelf_eq_one_snd_of_countSelf_eq_one_fst (h : l.ContrPerm l2) {I : Ind
     have h2' := countSelf_le_countId l.contr.toIndexList I
     omega
   · rw [← countSelf_neq_zero, h1]
-    simp
+    exact Nat.one_ne_zero
 
 lemma getDualInOtherEquiv_eq_of_countSelf
     (hn : IndexList.Subperm l.contr l2.contr.toIndexList) (i : Fin l.contr.length)
@@ -94,7 +92,7 @@ lemma getDualInOtherEquiv_eq_of_countSelf
       exact Finset.mem_univ i⟩).1 = l.contr.val.get i := by
   have h1' : (l.contr.val.get i) ∈ l2.contr.val := by
     rw [← countSelf_neq_zero, h2]
-    simp
+    exact Nat.one_ne_zero
   rw [← List.mem_singleton, ← filter_id_of_countId_eq_one_mem l2.contr.toIndexList h1' h1]
   simp only [List.get_eq_getElem, List.mem_filter, decide_eq_true_eq]
   apply And.intro (List.getElem_mem _ _ _)
@@ -144,13 +142,12 @@ lemma iff_count' : l.ContrPerm l2 ↔
   · intro ha I hI1
     have hI : I ∈ l.contr.val := by
       rw [← countSelf_neq_zero, hI1]
-      simp
+      exact Nat.one_ne_zero
     have hId : l.contr.val.indexOf I < l.contr.val.length := List.indexOf_lt_length.mpr hI
     have hI' : I = l.contr.val.get ⟨l.contr.val.indexOf I, hId⟩ := (List.indexOf_get hId).symm
     rw [hI'] at hI1 ⊢
     exact ha ⟨l.contr.val.indexOf I, hId⟩ hI1
-  · intro a_2 i a_3
-    simp_all only
+  · exact fun a i a_1 => a l.contr.val[↑i] a_1
 
 lemma iff_count : l.ContrPerm l2 ↔ l.contr.length = l2.contr.length ∧
     ∀ I, l.contr.countSelf I = 1 → l2.contr.countSelf I = 1 := by
@@ -160,7 +157,7 @@ lemma iff_count : l.ContrPerm l2 ↔ l.contr.length = l2.contr.length ∧
   intro I
   apply And.intro (countId_contr_le_one l I)
   intro h'
-  obtain ⟨I', hI1, hI2⟩ := countId_neq_zero_mem l.contr I (by omega)
+  obtain ⟨I', hI1, hI2⟩ := countId_neq_zero_mem l.contr I (ne_zero_of_eq_one h')
   rw [countId_congr _ hI2] at h' ⊢
   have hi := h.2 I' (countSelf_eq_one_of_countId_eq_one l.contr.toIndexList I' h' hI1)
   have h1 := countSelf_le_countId l2.contr.toIndexList I'
@@ -196,7 +193,7 @@ lemma iff_countSelf : l.ContrPerm l2 ↔ ∀ I, l.contr.countSelf I = l2.contr.c
       exact List.Perm.length_eq h1
     · intro I
       rw [h I]
-      simp
+      exact fun a => a
 
 lemma contr_perm (h : l.ContrPerm l2) : l.contr.val.Perm l2.contr.val := by
   rw [List.perm_iff_count]
@@ -206,9 +203,8 @@ lemma contr_perm (h : l.ContrPerm l2) : l.contr.val.Perm l2.contr.val := by
 
 /-- The relation `ContrPerm` is reflexive. -/
 @[simp]
-lemma refl (l : ColorIndexList 𝓒) : ContrPerm l l := by
-  rw [iff_countSelf]
-  exact fun I => rfl
+lemma refl (l : ColorIndexList 𝓒) : ContrPerm l l :=
+  iff_countSelf.mpr (congrFun rfl)
 
 /-- The relation `ContrPerm` is transitive. -/
 @[trans]
@@ -223,8 +219,7 @@ lemma equivalence : Equivalence (@ContrPerm 𝓒 _ _) where
   trans := trans
 
 lemma symm_trans (h1 : ContrPerm l l2) (h2 : ContrPerm l2 l3) :
-    (h1.trans h2).symm = h2.symm.trans h1.symm := by
-  simp only
+    (h1.trans h2).symm = h2.symm.trans h1.symm := rfl
 
 @[simp]
 lemma contr_self : ContrPerm l l.contr := by
@@ -233,9 +228,7 @@ lemma contr_self : ContrPerm l l.contr := by
   simp
 
 @[simp]
-lemma self_contr : ContrPerm l.contr l := by
-  symm
-  simp
+lemma self_contr : ContrPerm l.contr l := symm contr_self
 
 lemma length_of_no_contr (h : l.ContrPerm l') (h1 : l.withDual = ∅) (h2 : l'.withDual = ∅) :
     l.length = l'.length := by
@@ -248,8 +241,7 @@ lemma mem_withUniqueDualInOther_of_no_contr (h : l.ContrPerm l') (h1 : l.withDua
   simp only [ContrPerm] at h
   rw [contr_of_withDual_empty l h1, contr_of_withDual_empty l' h2] at h
   rw [h.2.1]
-  intro x
-  exact Finset.mem_univ x
+  exact fun x => Finset.mem_univ x
 
 end ContrPerm
 
@@ -279,10 +271,7 @@ lemma contrPermEquiv_colorMap_iso {l l' : ColorIndexList 𝓒} (h : ContrPerm l
   have hi : i ∈ (l'.contr.withUniqueDualInOther l.contr.toIndexList) := by
     rw [h.symm.2.1]
     exact Finset.mem_univ i
-  have hn := congrFun h' ⟨i, hi⟩
-  simp at hn
-  rw [← hn]
-  rfl
+  exact (congrFun h' ⟨i, hi⟩).symm
 
 lemma contrPermEquiv_colorMap_iso' {l l' : ColorIndexList 𝓒} (h : ContrPerm l l') :
     ColorMap.MapIso (contrPermEquiv h) l.contr.colorMap' l'.contr.colorMap' := by
@@ -296,7 +285,6 @@ lemma contrPermEquiv_refl : contrPermEquiv (ContrPerm.refl l) = Equiv.refl _ :=
 @[simp]
 lemma contrPermEquiv_symm {l l' : ColorIndexList 𝓒} (h : ContrPerm l l') :
     (contrPermEquiv h).symm = contrPermEquiv h.symm := by
-  simp only [contrPermEquiv]
   rfl
 
 @[simp]
@@ -354,7 +342,7 @@ lemma contrPermEquiv_contr_self {l : ColorIndexList 𝓒} :
     contrPermEquiv (by simp : ContrPerm l.contr l) =
     (Fin.castOrderIso (by simp)).toEquiv := by
   rw [← contrPermEquiv_symm, contrPermEquiv_self_contr]
-  simp
+  rfl
 
 /-- Given two `ColorIndexList` related by permutations and without duals, the equivalence between
   the indices of the corresponding index lists. This equivalence is the
@@ -368,19 +356,12 @@ def permEquiv {l l' : ColorIndexList 𝓒} (h : ContrPerm l l')
 lemma permEquiv_colorMap_iso {l l' : ColorIndexList 𝓒} (h : ContrPerm l l')
     (h1 : l.withDual = ∅) (h2 : l'.withDual = ∅) :
     ColorMap.MapIso (permEquiv h h1 h2).symm l'.colorMap' l.colorMap' := by
-  simp [ColorMap.MapIso]
   funext i
-  simp [contrPermEquiv, getDualInOtherEquiv]
+  rw [Function.comp_apply]
   have h' := h.symm
   simp only [ContrPerm] at h'
   rw [contr_of_withDual_empty l h1, contr_of_withDual_empty l' h2] at h'
-  have hi : i ∈ (l'.withUniqueDualInOther l.toIndexList) := by
-    rw [h'.2.1]
-    exact Finset.mem_univ i
-  have hn := congrFun h'.2.2 ⟨i, hi⟩
-  simp at hn
-  rw [← hn]
-  rfl
+  exact (congrFun h'.2.2 ⟨i, _⟩).symm
 
 end ColorIndexList
 

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

@@ -37,9 +37,7 @@ def contr : ColorIndexList 𝓒 where
   toIndexList := l.toIndexList.contrIndexList
   unique_duals := by
     simp [OnlyUniqueDuals]
-  dual_color := by
-    funext i
-    simp [Option.guard]
+  dual_color := ColorCond.contrIndexList
 
 @[simp]
 lemma contr_contr : l.contr.contr = l.contr := by
@@ -61,7 +59,7 @@ lemma contr_contr_idMap (i : Fin l.contr.contr.length) :
   rw [orderEmbOfFin_univ]
   · rfl
   · rw [h1]
-    simp
+    exact (Finset.card_fin l.contrIndexList.length).symm
 
 @[simp]
 lemma contr_contr_colorMap (i : Fin l.contr.contr.length) :
@@ -78,7 +76,7 @@ lemma contr_contr_colorMap (i : Fin l.contr.contr.length) :
   rw [orderEmbOfFin_univ]
   · rfl
   · rw [h1]
-    simp
+    exact (Finset.card_fin l.contrIndexList.length).symm
 
 @[simp]
 lemma contr_of_withDual_empty (h : l.withDual = ∅) :
@@ -148,18 +146,14 @@ def contrEquiv : (l.withUniqueDualLT ⊕ l.withUniqueDualLT) ⊕ Fin l.contr.len
   (Equiv.sumCongr (l.withUniqueLTGTEquiv) (Equiv.refl _)).trans <|
   (Equiv.sumCongr (Equiv.subtypeEquivRight (by
   rw [l.unique_duals]
-  simp only [mem_withDual_iff_isSome, implies_true]))
+  exact fun x => Eq.to_iff rfl))
     (Fin.castOrderIso l.contrIndexList_length).toEquiv).trans <|
   l.dualEquiv
 
 lemma contrEquiv_inl_inl_isSome (i : l.withUniqueDualLT) :
-    (l.getDual? (l.contrEquiv (Sum.inl (Sum.inl i)))).isSome := by
-  change (l.getDual? i).isSome
-  have h1 : i.1 ∈ l.withUniqueDual := by
-    have hi2 := i.2
-    simp only [withUniqueDualLT, Finset.mem_filter] at hi2
-    exact hi2.1
-  exact mem_withUniqueDual_isSome l.toIndexList (↑i) h1
+    (l.getDual? (l.contrEquiv (Sum.inl (Sum.inl i)))).isSome :=
+  mem_withUniqueDual_isSome l.toIndexList (↑i)
+    (mem_withUniqueDual_of_mem_withUniqueDualLt l.toIndexList (↑i) i.2)
 
 @[simp]
 lemma contrEquiv_inl_inr_eq (i : l.withUniqueDualLT) :
@@ -175,9 +169,9 @@ lemma contrEquiv_inl_inl_eq (i : l.withUniqueDualLT) :
 lemma contrEquiv_colorMapIso :
     ColorMap.MapIso (Equiv.refl (Fin l.contr.length))
     (ColorMap.contr l.contrEquiv l.colorMap) l.contr.colorMap := by
-  simp [ColorMap.MapIso, ColorMap.contr]
+  simp only [ColorMap.MapIso, ColorMap.contr, Equiv.coe_refl, CompTriple.comp_eq]
   funext i
-  simp [contr]
+  simp only [contr, Function.comp_apply, contrIndexList_colorMap]
   rfl
 
 lemma contrEquiv_contrCond : ColorMap.ContrCond l.contrEquiv l.colorMap := by
@@ -201,7 +195,7 @@ lemma contrEquiv_on_withDual_empty (i : Fin l.contr.length) (h : l.withDual =
   rw [orderEmbOfFin_univ]
   · rfl
   · rw [h]
-    simp
+    exact (Finset.card_fin l.length).symm
 
 end ColorIndexList
 end IndexNotation

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

@@ -240,7 +240,7 @@ def withUniqueDualLTEquivGT : l.withUniqueDualLT ≃ l.withUniqueDualGT where
     apply option_not_lt
     · rw [getDual?_getDualEquiv]
       simpa only [getDualEquiv, Equiv.coe_fn_mk, Option.some_get] using hi.2
-    · simp only [ne_eq, getDual?_neq_self, not_false_eq_true]⟩
+    · exact getDual?_neq_self l _⟩
   invFun i := ⟨l.getDualEquiv.symm ⟨i, l.mem_withUniqueDual_of_mem_withUniqueDualGt i i.2⟩, by
     have hi := i.2
     simp only [withUniqueDualLT, Finset.mem_filter, Finset.coe_mem, true_and, gt_iff_lt]
@@ -249,7 +249,7 @@ def withUniqueDualLTEquivGT : l.withUniqueDualLT ≃ l.withUniqueDualGT where
     · erw [getDual?_getDualEquiv]
       simpa [getDualEquiv] using hi.2
     · symm
-      simp⟩
+      exact getDual?_neq_self l _⟩
   left_inv x := SetCoe.ext <| by
     simp
   right_inv x := SetCoe.ext <| by