refactor: Speed and lint

HepLean/SpaceTime/LorentzTensor/IndexNotation/AreDual.lean

@@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.SpaceTime.LorentzTensor.IndexNotation.Basic
-import Mathlib.Algebra.Order.Ring.Nat
-import Mathlib.Data.Finset.Sort
 /-!
 
 # Indices which are dual in an index list

HepLean/SpaceTime/LorentzTensor/IndexNotation/Color.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.SpaceTime.LorentzTensor.IndexNotation.Contraction
+import HepLean.SpaceTime.LorentzTensor.IndexNotation.OnlyUniqueDuals
 import HepLean.SpaceTime.LorentzTensor.Basic
 import Init.Data.List.Lemmas
 import HepLean.SpaceTime.LorentzTensor.Contraction
@@ -69,7 +70,7 @@ lemma iff_withDual :
 lemma iff_on_isSome : l.ColorCond ↔ ∀ (i : Fin l.length) (h : (l.getDual? i).isSome), 𝓒.τ
     (l.colorMap ((l.getDual? i).get h)) = l.colorMap i := by
   rw [iff_withDual]
-  simp
+  simp only [Subtype.forall, mem_withDual_iff_isSome]
 
 lemma assoc (h : ColorCond (l ++ l2 ++ l3)) :
     ColorCond (l ++ (l2 ++ l3)) := by
@@ -79,7 +80,9 @@ lemma assoc (h : ColorCond (l ++ l2 ++ l3)) :
 lemma inl (h : ColorCond (l ++ l2)) : ColorCond l := by
   rw [iff_withDual] at h ⊢
   intro i
-  simpa using h ⟨appendEquiv (Sum.inl i), by simp_all⟩
+  simpa only [withDual_isSome, getDual?_append_inl_of_getDual?_isSome, Option.get_some,
+    colorMap_append_inl] using h ⟨appendEquiv (Sum.inl i), by simp only [mem_withDual_iff_isSome,
+      withDual_isSome, getDual?_append_inl_of_getDual?_isSome, Option.isSome_some]⟩
 
 lemma symm (hu : (l ++ l2).withUniqueDual = (l ++ l2).withDual) (h : ColorCond (l ++ l2)) :
     ColorCond (l2 ++ l) := by
@@ -97,7 +100,7 @@ lemma symm (hu : (l ++ l2).withUniqueDual = (l ++ l2).withDual) (h : ColorCond (
       Option.isSome_some, mem_withInDualOther_iff_isSome, Bool.not_eq_true, Option.not_isSome,
       Option.isNone_iff_eq_none, true_iff, Option.get_some, colorMap_append_inl]
       have hk'' := h (appendEquiv (Sum.inr k))
-      simp at hk''
+      simp only [getDual?_isSome_append_inr_iff, colorMap_append_inr] at hk''
       simp_all only [getDual?_append_inl_of_getDual?_isSome, Option.isSome_some, Option.isSome_none,
         Bool.false_eq_true, or_false, Option.isNone_none,
         getDual?_inr_getDualInOther?_isNone_getDual?_isSome, Option.get_some, colorMap_append_inr,
@@ -117,16 +120,25 @@ lemma symm (hu : (l ++ l2).withUniqueDual = (l ++ l2).withDual) (h : ColorCond (
   | Sum.inr k =>
     have hn := l2.append_inr_not_mem_withDual_of_withDualInOther l k hj
     by_cases hk' : (l.getDual? k).isSome
-    · simp_all
+    · simp_all only [mem_withDual_iff_isSome, mem_withInDualOther_iff_isSome, Bool.not_eq_true,
+        Option.not_isSome, Option.isNone_iff_eq_none, true_iff, Option.isNone_none,
+        getDual?_inr_getDualInOther?_isNone_getDual?_isSome, Option.get_some, colorMap_append_inr]
       have hk'' := h (appendEquiv (Sum.inl k))
-      simp at hk''
-      simp_all
-    · simp_all
+      simp only [getDual?_isSome_append_inl_iff, colorMap_append_inl] at hk''
+      simp_all only [Option.isNone_none, getDual?_inr_getDualInOther?_isNone_getDual?_isSome,
+        Option.isSome_some, Option.isSome_none, Bool.false_eq_true, or_false,
+        getDual?_append_inl_of_getDual?_isSome, Option.get_some, colorMap_append_inl, true_implies]
+    · simp_all only [mem_withDual_iff_isSome, Bool.false_eq_true, mem_withInDualOther_iff_isSome,
+      Bool.not_eq_true, Option.not_isSome, Option.isNone_iff_eq_none, false_iff,
+      colorMap_append_inr]
       have hn' : (l.getDualInOther? l2 k).isSome := by
-        simp_all
+        exact Option.ne_none_iff_isSome.mp hn
       have hk'' := h (appendEquiv (Sum.inl k))
-      simp at hk''
-      simp_all
+      simp only [getDual?_isSome_append_inl_iff, colorMap_append_inl] at hk''
+      simp_all only [Option.isSome_none, Bool.false_eq_true, or_true, Option.isNone_none,
+        getDual?_inl_of_getDual?_isNone_getDualInOther?_isSome, Option.get_some,
+        colorMap_append_inr, true_implies, getDual?_append_inr_getDualInOther?_isSome,
+        colorMap_append_inl]
 
 lemma inr  (hu : (l ++ l2).withUniqueDual = (l ++ l2).withDual) (h : ColorCond (l ++ l2)) :
     ColorCond l2 := inl (symm hu h)
@@ -185,7 +197,8 @@ lemma swap  (hu : (l ++ l2 ++ l3).withUniqueDual = (l ++ l2 ++ l3).withDual)
         simp only [getDualInOther?_append_of_inl, colorMap_append_inl]
         have hL := triple_right hu' hC
         rw [iff_on_isSome] at hL
-        have hL' := hL (appendEquiv (Sum.inl k')) (by simp [hn])
+        have hL' := hL (appendEquiv (Sum.inl k')) (by simp only [getDual?_isSome_append_inl_iff, hn,
+          or_true])
         simp_all only [Option.isNone_none, getDualInOther?_append_of_inl,
           getDual?_inl_of_getDual?_isNone_getDualInOther?_isSome, Option.isSome_some,
           getDual?_eq_none_append_inl_iff, Option.get_some, colorMap_append_inr,
@@ -195,7 +208,8 @@ lemma swap  (hu : (l ++ l2 ++ l3).withUniqueDual = (l ++ l2 ++ l3).withDual)
         simp only [getDualInOther?_append_of_inr, colorMap_append_inr]
         have hR := triple_drop_mid hu' hC
         rw [iff_on_isSome] at hR
-        have hR' := hR (appendEquiv (Sum.inl k')) (by simp [hn])
+        have hR' := hR (appendEquiv (Sum.inl k')) (by simp only [getDual?_isSome_append_inl_iff, hn,
+          or_true])
         simp_all only [Option.isNone_none, getDualInOther?_append_of_inr,
           getDual?_inl_of_getDual?_isNone_getDualInOther?_isSome, Option.isSome_some,
           getDual?_eq_none_append_inr_iff, Option.get_some, colorMap_append_inr,
@@ -226,9 +240,12 @@ lemma swap  (hu : (l ++ l2 ++ l3).withUniqueDual = (l ++ l2 ++ l3).withDual)
         simp_all only [getDualInOther?_of_append_of_isSome, Option.isSome_some,
           getDual?_append_inr_getDualInOther?_isSome, Option.get_some, colorMap_append_inl,
           colorMap_append_inr]
-      · simp_all
+      · simp_all only [Bool.not_eq_true, Option.not_isSome, Option.isNone_iff_eq_none,
+          true_implies]
         rw [← @Option.not_isSome_iff_eq_none, not_not] at hn
-        simp_all
+        simp_all only [getDualInOther?_of_append_of_isNone_isSome, Option.isSome_some,
+          getDual?_append_inr_getDualInOther?_isSome, Option.get_some, colorMap_append_inl,
+          colorMap_append_inr]
         have hR := triple_drop_mid hu' hC
         rw [iff_on_isSome] at hR
         have hR' := hR (appendEquiv (Sum.inr k)) (by simp [hn])
@@ -246,7 +263,8 @@ def bool (l : IndexList 𝓒.Color) : Bool :=
 
 lemma iff_bool : l.ColorCond ↔ bool l := by
   rw [iff_withDual, bool]
-  simp
+  simp only [Subtype.forall, mem_withDual_iff_isSome, Bool.if_false_right, Bool.and_true,
+    decide_eq_true_eq]
 
 end ColorCond
 
@@ -385,7 +403,8 @@ lemma contr_areDualInSelf (i j : Fin l.contr.length) :
 def contrEquiv : (l.withUniqueDualLT ⊕ l.withUniqueDualLT) ⊕ Fin l.contr.length ≃ Fin l.length :=
   (Equiv.sumCongr (l.withUniqueLTGTEquiv) (Equiv.refl _)).trans <|
   (Equiv.sumCongr (Equiv.subtypeEquivRight (by
-  simp [l.unique_duals])) (Fin.castOrderIso l.contrIndexList_length).toEquiv).trans <|
+  simp only [l.unique_duals, implies_true]))
+    (Fin.castOrderIso l.contrIndexList_length).toEquiv).trans <|
   l.dualEquiv
 
 lemma contrEquiv_inl_inl_isSome (i : l.withUniqueDualLT) :
@@ -393,7 +412,7 @@ lemma contrEquiv_inl_inl_isSome (i : l.withUniqueDualLT) :
   change (l.getDual? i).isSome
   have h1 : i.1 ∈ l.withUniqueDual := by
     have hi2 := i.2
-    simp [withUniqueDualLT] at hi2
+    simp only [withUniqueDualLT, Finset.mem_filter] at hi2
     exact hi2.1
   exact mem_withUniqueDual_isSome l.toIndexList (↑i) h1
 
@@ -503,7 +522,7 @@ lemma assoc (h : AppendCond l l2) (h' : AppendCond (l ++[h] l2) l3) :
 lemma swap (h : AppendCond l l2) (h' : AppendCond (l ++[h] l2) l3) :
     AppendCond (l2 ++[h.symm] l) l3:= by
   apply And.intro
-  · simp
+  · simp only [append_toIndexList]
     rw [← append_withDual_eq_withUniqueDual_swap]
     simpa using h'.1
   · exact ColorCond.swap h'.1 h'.2

HepLean/SpaceTime/LorentzTensor/IndexNotation/Contraction.lean

@@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.SpaceTime.LorentzTensor.IndexNotation.OnlyUniqueDuals
+import HepLean.SpaceTime.LorentzTensor.IndexNotation.WithUniqueDual
 import Mathlib.Algebra.Order.Ring.Nat
 import Mathlib.Data.Finset.Sort
 /-!
@@ -106,7 +106,7 @@ lemma contrIndexList_areDualInSelf (i j : Fin l.contrIndexList.length) :
 lemma contrIndexList_getDual? (i : Fin l.contrIndexList.length) :
     l.contrIndexList.getDual? i = none := by
   rw [← Option.not_isSome_iff_eq_none, ← mem_withDual_iff_isSome, mem_withDual_iff_exists]
-  simp [contrIndexList_areDualInSelf]
+  simp only [contrIndexList_areDualInSelf, not_exists]
   have h1 := (l.withoutDualEquiv (Fin.cast l.contrIndexList_length i)).2
   have h1' := Finset.disjoint_right.mp l.withDual_disjoint_withoutDual h1
   rw [mem_withDual_iff_exists] at h1'
@@ -254,7 +254,7 @@ def withUniqueDualLTEquivGT : l.withUniqueDualLT ≃ l.withUniqueDualGT where
     simp only [withUniqueDualGT, Finset.mem_filter, Finset.coe_mem, true_and]
     simp only [getDualEquiv, Equiv.coe_fn_mk, Option.some_get, Finset.coe_mem,
       getDual?_getDual?_get_of_withUniqueDual]
-    simp [withUniqueDualLT] at hi
+    simp only [withUniqueDualLT, Finset.mem_filter] at hi
     apply option_not_lt
     simpa [withUniqueDualLTToWithUniqueDual] using hi.2
     exact Ne.symm (getDual?_neq_self l i)⟩
@@ -263,7 +263,7 @@ def withUniqueDualLTEquivGT : l.withUniqueDualLT ≃ l.withUniqueDualGT where
     simp only [withUniqueDualLT, Finset.mem_filter, Finset.coe_mem, true_and, gt_iff_lt]
     simp only [getDualEquiv, Equiv.coe_fn_symm_mk, Option.some_get, Finset.coe_mem,
       getDual?_getDual?_get_of_withUniqueDual]
-    simp [withUniqueDualGT] at hi
+    simp only [withUniqueDualGT, Finset.mem_filter] at hi
     apply lt_option_of_not
     simpa [withUniqueDualLTToWithUniqueDual] using hi.2
     exact (getDual?_neq_self l i)⟩
@@ -278,7 +278,8 @@ def withUniqueDualLTEquivGT : l.withUniqueDualLT ≃ l.withUniqueDualGT where
 def withUniqueLTGTEquiv : l.withUniqueDualLT ⊕ l.withUniqueDualLT ≃ l.withUniqueDual := by
   apply (Equiv.sumCongr (Equiv.refl _ ) l.withUniqueDualLTEquivGT).trans
   apply (Equiv.Finset.union _ _ l.withUniqueDualLT_disjoint_withUniqueDualGT).trans
-  apply (Equiv.subtypeEquivRight (by simp [l.withUniqueDualLT_union_withUniqueDualGT]))
+  apply (Equiv.subtypeEquivRight (by simp only [l.withUniqueDualLT_union_withUniqueDualGT,
+    implies_true]))
 
 
 
@@ -327,7 +328,8 @@ lemma withUniqueDualInOther_eq_univ_symm (hl : l.length = l2.length)
   have hS'Eq : S' =  (l2.withUniqueDualInOther l) := by
     rw [@Finset.ext_iff]
     intro a
-    simp [S']
+    simp only [S']
+    simp
   rw [hS'Eq] at hsCardUn
   exact (Finset.card_eq_iff_eq_univ (l2.withUniqueDualInOther l)).mp hsCardUn
 
@@ -374,11 +376,11 @@ lemma withUniqueDualInOther_eq_univ_trans (h : l.withUniqueDualInOther l2 = Fins
   apply And.intro
   · rw [@getDualInOther?_isSome_iff_exists]
     use (l2.getDualInOther? l3 ((l.getDualInOther? l2 i).get hi.2.1)).get hi2.2.1
-    simp [AreDualInOther]
+    simp only [AreDualInOther, getDualInOther?_id]
   intro j hj
   have hj' : j = (l2.getDualInOther? l3 ((l.getDualInOther? l2 i).get hi.2.1)).get hi2.2.1  := by
     rw [← eq_getDualInOther?_get_of_withUniqueDualInOther_iff]
-    simpa [AreDualInOther] using hj
+    simpa only [AreDualInOther, getDualInOther?_id] using hj
     rw [h']
     exact Finset.mem_univ ((l.getDualInOther? l2 i).get hi.right.left)
   have hs : (l.getDualInOther? l3 i).isSome := by
@@ -387,7 +389,7 @@ lemma withUniqueDualInOther_eq_univ_trans (h : l.withUniqueDualInOther l2 = Fins
   have hs' : (l.getDualInOther? l3 i).get hs = (l2.getDualInOther? l3
       ((l.getDualInOther? l2 i).get hi.2.1)).get hi2.2.1 := by
     rw [← eq_getDualInOther?_get_of_withUniqueDualInOther_iff]
-    simp [AreDualInOther]
+    simp only [AreDualInOther, getDualInOther?_id]
     rw [h']
     exact Finset.mem_univ ((l.getDualInOther? l2 i).get hi.right.left)
   rw [← hj'] at hs'

HepLean/SpaceTime/LorentzTensor/IndexNotation/GetDual.lean

@@ -5,7 +5,6 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.SpaceTime.LorentzTensor.IndexNotation.AreDual
 import Mathlib.Algebra.Order.Ring.Nat
-import Mathlib.Data.Finset.Sort
 /-!
 
 # Get dual index

HepLean/SpaceTime/LorentzTensor/IndexNotation/OnlyUniqueDuals.lean

@@ -5,7 +5,6 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.SpaceTime.LorentzTensor.IndexNotation.WithUniqueDual
 import Mathlib.Algebra.Order.Ring.Nat
-import Mathlib.Data.Finset.Sort
 /-!
 
 # withDuals equal to withUniqueDuals
@@ -32,7 +31,8 @@ lemma withUnqiueDual_eq_withDual_iff_unique_forall :
   apply Iff.intro
   · intro h i j hj
     rw [@Finset.ext_iff] at h
-    simp [withUniqueDual] at h
+    simp only [withUniqueDual, mem_withDual_iff_isSome, Finset.mem_filter, Finset.mem_univ,
+      true_and, and_iff_left_iff_imp] at h
     refine h i ?_ j hj
     exact withDual_isSome l i
   · intro h
@@ -41,7 +41,8 @@ lemma withUnqiueDual_eq_withDual_iff_unique_forall :
     apply Iff.intro
     · exact fun hi => mem_withDual_of_mem_withUniqueDual l i hi
     · intro hi
-      simp [withUniqueDual]
+      simp only [withUniqueDual, mem_withDual_iff_isSome, Finset.mem_filter, Finset.mem_univ,
+        true_and]
       apply And.intro
       exact (mem_withDual_iff_isSome l i).mp hi
       intro j hj
@@ -116,9 +117,10 @@ lemma withUnqiueDual_eq_withDual_iff_list_apply_bool :
   rw [withUnqiueDual_eq_withDual_iff_list_apply]
   apply Iff.intro
   intro h
-  simp [withUnqiueDualEqWithDualBool, h]
+  simp only [withUnqiueDualEqWithDualBool, h, mem_withDual_iff_isSome, ↓reduceIte]
   intro h
-  simpa [withUnqiueDualEqWithDualBool] using h
+  simpa only [mem_withDual_iff_isSome, List.map_inj_left, withUnqiueDualEqWithDualBool,
+    Bool.if_false_right, Bool.and_true, decide_eq_true_eq] using h
 
 @[simp]
 lemma withUnqiueDual_eq_withDual_of_empty (h : l.withDual = ∅) :
@@ -146,10 +148,12 @@ lemma withUniqueDualInOther_eq_withDualInOther_append_of_symm'
   match k with
   | Sum.inl k =>
     rw [mem_append_withUniqueDualInOther_symm]
-    simpa using h (appendEquiv (Sum.inr k))
+    simpa only [mem_withInDualOther_iff_isSome, getDualInOther?_append_of_inl,
+      getDualInOther?_append_of_inr] using h (appendEquiv (Sum.inr k))
   | Sum.inr k =>
     rw [← mem_append_withUniqueDualInOther_symm]
-    simpa using h (appendEquiv (Sum.inl k))
+    simpa only [mem_withInDualOther_iff_isSome, getDualInOther?_append_of_inr,
+      getDualInOther?_append_of_inl] using h (appendEquiv (Sum.inl k))
 
 lemma withUniqueDualInOther_eq_withDualInOther_append_of_symm :
     (l ++ l2).withUniqueDualInOther l3 = (l ++ l2).withDualInOther l3 ↔
@@ -228,10 +232,11 @@ lemma append_withDual_eq_withUniqueDual_withUniqueDualInOther_inl
   rw [Finset.ext_iff]
   intro i
   refine Iff.intro (fun h' => ?_) (fun h' => ?_)
-  · simp [h']
+  · simp only [mem_withInDualOther_iff_isSome, h', mem_withUniqueDualInOther_isSome]
   · have hn : appendEquiv (Sum.inl i) ∈ (l ++ l2).withUniqueDual := by
       rw [h]
-      simp_all
+      simp_all only [mem_withInDualOther_iff_isSome, mem_withDual_iff_isSome,
+        getDual?_isSome_append_inl_iff, or_true, mem_withUniqueDual_isSome]
     refine l.mem_withUniqueDualInOther_of_inl_withDualInOther l2 i hn ?_
     exact (mem_withInDualOther_iff_isSome l l2 i).mp h'
 

HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean

@@ -119,10 +119,10 @@ def contr (T : 𝓣.TensorIndex) : 𝓣.TensorIndex where
 lemma contr_of_withDual_empty (T : 𝓣.TensorIndex) (h : T.withDual = ∅) :
     T.contr = T := by
   refine ext ?_ ?_
-  · simp [contr, ColorIndexList.contr]
+  · simp only [contr, ColorIndexList.contr]
     have hx := T.contrIndexList_of_withDual_empty h
     apply ColorIndexList.ext
-    simp [hx]
+    simp only [hx]
   · simp only [contr]
     cases T
     rename_i i T
@@ -142,7 +142,7 @@ lemma contr_of_withDual_empty (T : 𝓣.TensorIndex) (h : T.withDual = ∅) :
         exact Finset.mem_of_mem_filter x hx
       rw [i.unique_duals] at h
       rw [h] at hx'
-      simp_all
+      simp_all only [Finset.not_mem_empty]
     erw [TensorStructure.contr_tprod_isEmpty]
     erw [mapIso_tprod]
     simp only [Equiv.refl_symm, Equiv.refl_apply, colorMap', mapIso_tprod, id_eq,
@@ -393,13 +393,14 @@ lemma add_toColorIndexList (T₁ T₂ : 𝓣.TensorIndex) (h : AddCond T₁ T₂
 @[simp]
 lemma add_tensor (T₁ T₂ : 𝓣.TensorIndex) (h : AddCond T₁ T₂) :
     (add T₁ T₂ h).tensor =
-    (𝓣.mapIso (addCondEquiv h) (addCondEquiv_colorMap h) T₁.contr.tensor) + T₂.contr.tensor := by rfl
+    (𝓣.mapIso (addCondEquiv h) (addCondEquiv_colorMap h) T₁.contr.tensor) + T₂.contr.tensor := rfl
 
 /-- Scalar multiplication commutes with addition. -/
 lemma smul_add (r : R) (T₁ T₂ : 𝓣.TensorIndex) (h : AddCond T₁ T₂) :
     r • (T₁ +[h] T₂) = r • T₁ +[h] r • T₂ := by
   refine ext rfl ?_
-  simp [add]
+  simp only [add, contr_toColorIndexList, addCondEquiv, smul_index, smul_tensor, _root_.smul_add,
+    Fin.castOrderIso_refl, OrderIso.refl_toEquiv, mapIso_refl, map_add, LinearEquiv.refl_apply]
   rw [tensor_eq_of_eq (smul_contr r T₁), tensor_eq_of_eq (smul_contr r T₂)]
   simp only [smul_index, contr_toColorIndexList, Fin.castOrderIso_refl, OrderIso.refl_toEquiv,
     mapIso_refl, smul_tensor, map_smul, LinearEquiv.refl_apply]

HepLean/SpaceTime/LorentzTensor/IndexNotation/WithDual.lean

@@ -5,7 +5,6 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.SpaceTime.LorentzTensor.IndexNotation.GetDual
 import Mathlib.Algebra.Order.Ring.Nat
-import Mathlib.Data.Finset.Sort
 /-!
 
 # With dual

HepLean/SpaceTime/LorentzTensor/IndexNotation/WithUniqueDual.lean

@@ -5,7 +5,6 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.SpaceTime.LorentzTensor.IndexNotation.WithDual
 import Mathlib.Algebra.Order.Ring.Nat
-import Mathlib.Data.Finset.Sort
 /-!
 
 # With Unique Dual