refactor: Lint

HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean

@@ -3,9 +3,6 @@ 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 Mathlib.Data.Set.Finite
-import Mathlib.Logic.Equiv.Fin
-import Mathlib.Data.Finset.Sort
 import Mathlib.Tactic.FinCases
 /-!
 
@@ -105,6 +102,8 @@ instance : Decidable (listCharIndex X l) :=
 
 -/
 
+/-- An index for `X` is an pair of an element of `X` (the color of the index) and a natural
+  number (the id of the index). -/
 def Index : Type := X × ℕ
 
 instance : DecidableEq (Index X) := instDecidableEqProd
@@ -116,6 +115,7 @@ variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X]
 /-- The color associated to an index. -/
 def toColor (I : Index X) : X := I.1
 
+/-- The natural number representating the id of an index. -/
 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
@@ -136,7 +136,7 @@ end Index
 
 -/
 
-/-- An index is a non-empty string satisfying the condtion `listCharIndex`,
+/-- An index rep is a non-empty string satisfying the condtion `listCharIndex`,
   e.g. `ᵘ¹²` or `ᵤ₄₃` etc. -/
 def IndexRep : Type := {s : String // listCharIndex X s.toList ∧ s.toList ≠ []}
 
@@ -198,6 +198,8 @@ def tailNat (s : IndexRep X) : List ℕ := s.tail.map charToNat
 /-- The id of an index, as a natural number. -/
 def id (s : IndexRep X) : ℕ := s.tailNat.foldl (fun a b => 10 * a + b) 0
 
+/-- The index associated with a `IndexRep`. -/
 def toIndex (s : IndexRep X) : Index X := (s.toColor, s.id)
+
 end IndexRep
 end IndexNotation

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

@@ -184,7 +184,7 @@ lemma getDualInOtherEquiv_eq_of_countSelf
     rw [← countSelf_neq_zero, h2]
     simp
   rw [← List.mem_singleton, ← filter_id_of_countId_eq_one_mem l2.contr.toIndexList h1' h1 ]
-  simp
+  simp only [List.get_eq_getElem, List.mem_filter, decide_eq_true_eq]
   apply And.intro (List.getElem_mem _ _ _)
   simp [getDualInOtherEquiv]
   change _ = l2.contr.idMap (l.contr.getDualInOtherEquiv l2.contr ⟨i, by
@@ -194,7 +194,8 @@ lemma getDualInOtherEquiv_eq_of_countSelf
   rfl
 
 lemma colorMap_eq_of_countSelf (hn : IndexList.Subperm l.contr l2.contr.toIndexList)
-    (h2 : ∀ i, l.contr.countSelf (l.contr.val.get i) = 1 → l2.contr.countSelf (l.contr.val.get i) = 1) :
+    (h2 : ∀ i, l.contr.countSelf (l.contr.val.get i) = 1
+    → l2.contr.countSelf (l.contr.val.get i) = 1) :
     l2.contr.colorMap' ∘ Subtype.val ∘ (l.contr.getDualInOtherEquiv l2.contr)
     = l.contr.colorMap' ∘ Subtype.val := by
   funext a

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

@@ -3,6 +3,9 @@ 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 Mathlib.Data.Set.Finite
+import Mathlib.Logic.Equiv.Fin
+import Mathlib.Data.Finset.Sort
 import HepLean.SpaceTime.LorentzTensor.IndexNotation.Basic
 /-!
 

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

@@ -49,6 +49,7 @@ variable {𝓒 : TensorColor}
 variable [IndexNotation 𝓒.Color] [Fintype 𝓒.Color] [DecidableEq 𝓒.Color]
 variable (l l2 l3 : IndexList 𝓒.Color)
 
+/-- The number of times `I` or its dual appears in an `IndexList`. -/
 def countColorQuot (I : Index 𝓒.Color) : ℕ := l.val.countP (fun J => I = J ∨ I.dual = J)
 
 lemma countColorQuot_eq_filter_id_countP (I : Index 𝓒.Color) :
@@ -81,7 +82,8 @@ lemma countColorQuot_eq_filter_id_countP (I : Index 𝓒.Color) :
       simp
 
 lemma countColorQuot_eq_filter_color_countP (I : Index 𝓒.Color) :
-    l.countColorQuot I = (l.val.filter (fun J =>  I.toColor = J.toColor ∨ I.toColor = 𝓒.τ (J.toColor))).countP
+    l.countColorQuot I =
+    (l.val.filter (fun J =>  I.toColor = J.toColor ∨ I.toColor = 𝓒.τ (J.toColor))).countP
     (fun J =>  I.id = J.id) := by
   rw [countColorQuot_eq_filter_id_countP]
   rw [List.countP_filter, List.countP_filter]
@@ -154,6 +156,7 @@ lemma countColorQuot_contrIndexList_eq_of_countId_eq
     l.filter_id_contrIndexList_eq_of_countId_contrIndexList I h1,
     countColorQuot_eq_filter_id_countP]
 
+/-- The number of times an index `I` appears in an index list. -/
 def countSelf (I : Index 𝓒.Color) : ℕ := l.val.countP (fun J => I = J)
 
 lemma countSelf_eq_filter_id_countP : l.countSelf I =
@@ -165,7 +168,7 @@ lemma countSelf_eq_filter_id_countP : l.countSelf I =
   simp [Index.eq_iff_color_eq_and_id_eq]
 
 lemma countSelf_eq_filter_color_countP :
-  l.countSelf I =
+    l.countSelf I =
     (l.val.filter (fun J => I.toColor = J.toColor)).countP (fun J => I.id = J.id) := by
   simp [countSelf]
   rw [List.countP_filter]
@@ -182,7 +185,7 @@ lemma countSelf_count (I : Index 𝓒.Color) : l.countSelf I = l.val.count I :=
   rw [countSelf, List.count]
   apply List.countP_congr
   intro I' _
-  simp
+  simp only [decide_eq_true_eq, beq_iff_eq]
   exact eq_comm
 
 lemma countSelf_eq_zero (I : Index 𝓒.Color) : l.countSelf I = 0 ↔ I ∉ l.val := by
@@ -246,6 +249,7 @@ lemma countSelf_contrIndexList_get (i : Fin l.contrIndexList.length) :
     exact List.getElem_mem l.contrIndexList.val (↑i) _
   · exact List.getElem_mem l.contrIndexList.val (↑i) _
 
+/-- The number of times the dual of an index `I` appears in an index list. -/
 def countDual (I : Index 𝓒.Color) : ℕ := l.val.countP (fun J => I.dual = J)
 
 lemma countDual_eq_countSelf_Dual (I : Index 𝓒.Color) : l.countDual I = l.countSelf I.dual := by
@@ -398,10 +402,10 @@ abbrev countColorCond (l : IndexList 𝓒.Color) (I : Index 𝓒.Color) : Prop :
 lemma countColorCond_of_filter_eq (l l2 : IndexList 𝓒.Color) {I : Index 𝓒.Color}
     (hf : l.val.filter (fun J => I.id = J.id) = l2.val.filter (fun J => I.id = J.id))
     (h1 : countColorCond l I) : countColorCond l2 I := by
-  rw [countColorCond, countColorQuot_eq_filter_id_countP, countId_eq_length_filter, countSelf_eq_filter_id_countP,
-    countDual_eq_filter_id_countP, ← hf]
-  rw [countColorCond, countColorQuot_eq_filter_id_countP, countId_eq_length_filter, countSelf_eq_filter_id_countP,
-    countDual_eq_filter_id_countP] at h1
+  rw [countColorCond, countColorQuot_eq_filter_id_countP, countId_eq_length_filter,
+    countSelf_eq_filter_id_countP, countDual_eq_filter_id_countP, ← hf]
+  rw [countColorCond, countColorQuot_eq_filter_id_countP, countId_eq_length_filter,
+    countSelf_eq_filter_id_countP, countDual_eq_filter_id_countP] at h1
   exact h1
 
 lemma iff_countColorCond_isSome (hl : l.OnlyUniqueDuals) : l.ColorCond ↔
@@ -548,7 +552,8 @@ lemma contrIndexList_left (hl : (l ++ l2).OnlyUniqueDuals) (h1 : (l ++ l2).Color
   have hIdEq : l.contrIndexList.countId I = l.countId I := by
     simp at h2 hI2
     omega
-  simp
+  simp only [countColorCond, countColorQuot_append, countId_append, countSelf_append,
+    countDual_append]
   rw [l.countColorQuot_contrIndexList_eq_of_countId_eq hIdEq,
     l.countSelf_contrIndexList_eq_of_countId_eq hIdEq,
     l.countDual_contrIndexList_eq_of_countId_eq hIdEq, hIdEq]

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

@@ -124,13 +124,14 @@ lemma countId_get_other (i : Fin l.length) : l2.countId (l.val.get i) =
   simp [AreDualInOther, idMap]
 
 /-! TODO: Replace with mathlib lemma. -/
-lemma filter_finRange (i : Fin l.length) : List.filter (fun j => i = j) (List.finRange l.length) = [i] := by
+lemma filter_finRange (i : Fin l.length) :
+    List.filter (fun j => i = j) (List.finRange l.length) = [i] := by
   have h3 : (List.filter (fun j => i = j) (List.finRange l.length)).length = 1 := by
     rw [← List.countP_eq_length_filter]
     trans List.count i (List.finRange l.length)
     · simp [List.count]
       apply List.countP_congr (fun j _ => ?_)
-      simp
+      simp only [decide_eq_true_eq, beq_iff_eq]
       exact eq_comm
     · exact List.nodup_iff_count_eq_one.mp (List.nodup_finRange l.length) _ (List.mem_finRange i)
   have h4 : i ∈ List.filter (fun j => i = j) (List.finRange l.length) := by
@@ -153,7 +154,8 @@ lemma countId_get (i : Fin l.length) : l.countId (l.val.get i) =
     intro j _
     simp [AreDualInSelf, AreDualInOther]
   rw [h1]
-  have h1 := List.length_eq_countP_add_countP (fun j => i = j) ((List.finRange l.length).filter (fun j => l.AreDualInOther l i j))
+  have h1 := List.length_eq_countP_add_countP (fun j => i = j)
+    ((List.finRange l.length).filter (fun j => l.AreDualInOther l i j))
   have h2 : List.countP (fun j => i = j)
       (List.filter (fun j => l.AreDualInOther l i j) (List.finRange l.length)) =
      List.countP (fun j => l.AreDualInOther l i j)
@@ -165,7 +167,7 @@ lemma countId_get (i : Fin l.length) : l.countId (l.val.get i) =
   rw [ha] at h2
   rw [h2] at h1
   rw [List.countP_eq_length_filter, h1, add_comm]
-  simp
+  simp only [decide_eq_true_eq, decide_not, add_right_inj]
   simp [List.countP, List.countP.go, AreDualInOther]
 
 /-!
@@ -214,7 +216,7 @@ lemma countId_neq_zero_of_mem_withDualInOther (i : Fin l.length) (h : i ∈ l.wi
   rw [List.length_eq_zero] at hn
   obtain ⟨j, hj⟩ := h
   have hjmem : l2.val.get j ∈  List.filter (fun J => decide ((l.val.get i).id = J.id)) l2.val := by
-    simp
+    simp only [List.get_eq_getElem, List.mem_filter, decide_eq_true_eq]
     apply And.intro
     · exact List.getElem_mem l2.val (↑j) j.isLt
     · simpa [AreDualInOther] using hj
@@ -231,7 +233,6 @@ lemma countId_of_not_mem_withDualInOther (i : Fin l.length) (h : i ∉ l.withDua
   obtain ⟨j, hj⟩ := hx
   have hjmem : j ∈ l2.val :=  List.mem_of_mem_filter hj
   have hj' : l2.val.indexOf j < l2.length := List.indexOf_lt_length.mpr hjmem
-  have hjid : l2.val.get ⟨l2.val.indexOf j, hj'⟩ = j := List.indexOf_get hj'
   rw [mem_withInDualOther_iff_exists] at h
   simp at h
   have hj' := h ⟨l2.val.indexOf j, hj'⟩
@@ -261,7 +262,7 @@ lemma mem_withoutDual_iff_countId_eq_one (i : Fin l.length) :
 lemma countId_eq_two_of_mem_withUniqueDual (i : Fin l.length) (h : i ∈ l.withUniqueDual) :
     l.countId (l.val.get i) = 2 := by
   rw [countId_get]
-  simp
+  simp only [Nat.reduceEqDiff]
   let i' :=  (l.getDual? i).get (mem_withUniqueDual_isSome l i h)
   have h1 :  [i'] = (List.finRange l.length).filter (fun j => (l.AreDualInSelf i j)) := by
     trans List.filter (fun j => (l.AreDualInSelf i j)) [i']
@@ -279,7 +280,7 @@ lemma countId_eq_two_of_mem_withUniqueDual (i : Fin l.length) (h : i ∈ l.withU
       exact Bool.and_comm (decide (l.AreDualInSelf i j)) (decide (j = i'))
     · simp
       refine List.filter_congr (fun j _ => ?_)
-      simp
+      simp only [Bool.and_iff_right_iff_imp, decide_eq_true_eq]
       simp [withUniqueDual] at h
       intro hj
       have hj' := h.2 j hj
@@ -340,7 +341,7 @@ lemma countId_eq_one_of_mem_withUniqueDualInOther (i : Fin l.length)
     · simp
       refine List.filter_congr (fun j _ => ?_)
       simp [withUniqueDualInOther] at h
-      simp
+      simp only [Bool.and_iff_right_iff_imp, decide_eq_true_eq]
       intro hj
       have hj' := h.2.2 j hj
       apply Option.some_injective

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

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.SpaceTime.LorentzTensor.IndexNotation.IndexList.CountId
-import Mathlib.Algebra.Order.Ring.Nat
 import Mathlib.Data.Finset.Sort
 import Mathlib.Tactic.FinCases
 /-!
@@ -97,6 +96,8 @@ lemma getDual?_getDualEquiv (i : l.withUniqueDual) : l.getDual? (l.getDualEquiv
   simp
   rfl
 
+/-- An equivalence from `l.withUniqueDualInOther l2 ` to
+  `l2.withUniqueDualInOther l` obtained by taking the dual index. -/
 def getDualInOtherEquiv : l.withUniqueDualInOther l2 ≃ l2.withUniqueDualInOther l where
   toFun x := ⟨(l.getDualInOther? l2 x).get (l.mem_withUniqueDualInOther_isSome l2 x.1 x.2), by
     rw [mem_withUniqueDualInOther_iff_countId_eq_one]
@@ -139,7 +140,7 @@ lemma getDualInOtherEquiv_self_refl : l.getDualInOtherEquiv l = Equiv.refl _ :=
   intro x
   simp [getDualInOtherEquiv]
   apply Subtype.eq
-  simp
+  simp only
   have hx2 := x.2
   simp [withUniqueDualInOther] at hx2
   apply Option.some_injective

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

@@ -25,6 +25,8 @@ namespace IndexList
 variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X]
 variable (l l2 l3 : IndexList X)
 
+/-- The conditon on an index list which is true if and only if for every index with a dual,
+  that dual is unique. -/
 def OnlyUniqueDuals : Prop := l.withUniqueDual = l.withDual
 
 namespace OnlyUniqueDuals
@@ -100,7 +102,7 @@ lemma symm' (h : (l ++ l2).OnlyUniqueDuals) : (l2 ++ l).OnlyUniqueDuals := by
   intro I
   have hI := h I
   simp at hI
-  simp
+  simp only [countId_append, ge_iff_le]
   omega
 
 lemma symm : (l ++ l2).OnlyUniqueDuals ↔ (l2 ++ l).OnlyUniqueDuals := by
@@ -111,7 +113,7 @@ lemma swap (h : (l ++ l2 ++ l3).OnlyUniqueDuals) : (l2 ++ l ++ l3).OnlyUniqueDua
   intro I
   have hI := h I
   simp at hI
-  simp
+  simp only [countId_append, ge_iff_le]
   omega
 
 /-!
@@ -161,13 +163,12 @@ lemma countId_of_OnlyUniqueDuals (h : l.OnlyUniqueDuals) (I : Index X) :
   exact h I
 
 lemma countId_eq_two_ofcontrIndexList_left_of_OnlyUniqueDuals
-     (h : (l ++ l2).OnlyUniqueDuals) (I : Index X) (h' : (l.contrIndexList ++ l2).countId I = 2 ) :
+    (h : (l ++ l2).OnlyUniqueDuals) (I : Index X) (h' : (l.contrIndexList ++ l2).countId I = 2 ) :
     (l ++ l2).countId I = 2 := by
-  simp
+  simp only [countId_append]
   have h1 := countId_contrIndexList_le_countId l I
   have h3 :=  countId_of_OnlyUniqueDuals _ h I
-  have h4 := countId_of_OnlyUniqueDuals _ h.contrIndexList_left I
-  simp at h3 h4 h'
+  simp at h3 h'
   omega
 
 

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

@@ -5,7 +5,6 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.SpaceTime.LorentzTensor.IndexNotation.IndexList.CountId
 import HepLean.SpaceTime.LorentzTensor.IndexNotation.IndexList.Contraction
-import HepLean.SpaceTime.LorentzTensor.IndexNotation.IndexList.Color
 import Mathlib.Algebra.Order.Ring.Nat
 import Mathlib.Data.Finset.Sort
 import Mathlib.Tactic.FinCases
@@ -22,6 +21,8 @@ namespace IndexList
 variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X]
 variable (l l2 l3 : IndexList X)
 
+/-- We say a IndexList `l` is a subpermutation of `l2` there are no duals in `l`, and
+  every element of `l` has a unique dual in `l2`. -/
 def Subperm : Prop := l.withUniqueDualInOther l2 = Finset.univ
 
 namespace Subperm
@@ -88,7 +89,7 @@ lemma symm (h : l.Subperm l2) (hl : l.length = l2.length) : l2.Subperm l := by
 lemma contr_refl : l.contrIndexList.Subperm l.contrIndexList := by
   rw [iff_countId]
   intro I
-  simp
+  simp only [imp_self, and_true]
   exact countId_contrIndexList_le_one l I
 
 end Subperm