refactor: Lint

HepLean/SpaceTime/LorentzTensor/EinsteinNotation/IndexNotation.lean

@@ -102,7 +102,7 @@ macro "prodTactic" : tactic =>
     `(tactic| {
     apply (ColorIndexList.AppendCond.iff_bool _ _).mpr
     change @ColorIndexList.AppendCond.bool einsteinTensorColor
-       instDecidableEqColorEinsteinTensorColor _ _
+      instDecidableEqColorEinsteinTensorColor _ _
     simp only [prod_toIndexList, indexNotation_eq_color, fromIndexStringColor, mkDualMap,
       toTensorColor_eq, decidableEq_eq_color]
     decide})

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

@@ -127,7 +127,7 @@ lemma iff_bool (l l2 : ColorIndexList 𝓒) : AppendCond l l2 ↔ bool l.toIndex
 lemma countId_contr_fst_eq_zero_mem_snd (h : AppendCond l l2) {I : Index 𝓒.Color}
     (hI : I ∈ l2.val) : l.contr.countId I = 0 ↔ l.countId I = 0 := by
   rw [countId_contr_eq_zero_iff]
-  have h1  := countId_mem l2.toIndexList I hI
+  have h1 := countId_mem l2.toIndexList I hI
   have h1I := h.1
   rw [OnlyUniqueDuals.iff_countId_leq_two'] at h1I
   have h1I' := h1I I

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

@@ -123,7 +123,7 @@ To prevent choice problems, this has to be done after contraction.
 -/
 def ContrPerm : Prop :=
   l.contr.length = l'.contr.length ∧
-  IndexList.Subperm l.contr l'.contr.toIndexList  ∧
+  IndexList.Subperm l.contr l'.contr.toIndexList ∧
   l'.contr.colorMap' ∘ Subtype.val ∘ (l.contr.getDualInOtherEquiv l'.contr)
   = l.contr.colorMap' ∘ Subtype.val
 
@@ -163,7 +163,7 @@ lemma mem_snd_of_mem_snd (h : l.ContrPerm l2) {I : Index 𝓒.Color} (hI : I ∈
 
 lemma countSelf_eq_one_snd_of_countSelf_eq_one_fst (h : l.ContrPerm l2) {I : Index 𝓒.Color}
     (h1 : l.contr.countSelf I = 1) : l2.contr.countSelf I = 1 := by
-  refine countSelf_eq_one_of_countId_eq_one l2.contr I ?_ (mem_snd_of_mem_snd h ?_ )
+  refine countSelf_eq_one_of_countId_eq_one l2.contr I ?_ (mem_snd_of_mem_snd h ?_)
   · have h2 := h.2.1
     rw [Subperm.iff_countId] at h2
     refine (h2 I).2 ?_
@@ -183,7 +183,7 @@ lemma getDualInOtherEquiv_eq_of_countSelf
   have h1' : (l.contr.val.get i) ∈ l2.contr.val := by
     rw [← countSelf_neq_zero, h2]
     simp
-  rw [← List.mem_singleton, ← filter_id_of_countId_eq_one_mem l2.contr.toIndexList h1' h1 ]
+  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 _ _ _)
   simp [getDualInOtherEquiv]
@@ -213,7 +213,7 @@ lemma colorMap_eq_of_countSelf (hn : IndexList.Subperm l.contr l2.contr.toIndexL
       exact List.getElem_mem l.contr.val (↑↑a) a.1.isLt
 
 lemma iff_count_fin : l.ContrPerm l2 ↔
-    l.contr.length = l2.contr.length  ∧ IndexList.Subperm l.contr l2.contr.toIndexList ∧
+    l.contr.length = l2.contr.length ∧ IndexList.Subperm l.contr l2.contr.toIndexList ∧
     ∀ i, l.contr.countSelf (l.contr.val.get i) = 1 →
     l2.contr.countSelf (l.contr.val.get i) = 1 := by
   refine Iff.intro (fun h => ?_) (fun h => ?_)
@@ -224,7 +224,7 @@ lemma iff_count_fin : l.ContrPerm l2 ↔
 
 lemma iff_count' : l.ContrPerm l2 ↔
     l.contr.length = l2.contr.length ∧ IndexList.Subperm l.contr l2.contr.toIndexList ∧
-    ∀ I, l.contr.countSelf I = 1 → l2.contr.countSelf I = 1  := by
+    ∀ I, l.contr.countSelf I = 1 → l2.contr.countSelf I = 1 := by
   rw [iff_count_fin]
   simp_all only [List.get_eq_getElem, and_congr_right_iff]
   intro _ _
@@ -240,7 +240,7 @@ lemma iff_count' : l.ContrPerm l2 ↔
   · intro a_2 i a_3
     simp_all only
 
-lemma iff_count :  l.ContrPerm l2 ↔ l.contr.length = l2.contr.length ∧
+lemma iff_count : l.ContrPerm l2 ↔ l.contr.length = l2.contr.length ∧
     ∀ I, l.contr.countSelf I = 1 → l2.contr.countSelf I = 1 := by
   rw [iff_count']
   refine Iff.intro (fun h => And.intro h.1 h.2.2) (fun h => And.intro h.1 (And.intro ?_ h.2))
@@ -281,7 +281,7 @@ lemma iff_countSelf : l.ContrPerm l2 ↔ ∀ I, l.contr.countSelf I = l2.contr.c
         intro I
         rw [← countSelf_count, ← countSelf_count]
         exact h I
-      exact List.Perm.length_eq  h1
+      exact List.Perm.length_eq h1
     · intro I
       rw [h I]
       simp
@@ -295,8 +295,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
+  rw [iff_countSelf]
+  exact fun I => rfl
 
 /-- The relation `ContrPerm` is transitive. -/
 @[trans]
@@ -398,7 +398,7 @@ lemma contrPermEquiv_trans {l l2 l3 : ColorIndexList 𝓒}
   apply congrArg
   have h1' : l.contr.countSelf (l.contr.val.get x) = 1 := by simp [contr]
   rw [iff_countSelf.mp h1, iff_countSelf.mp h2] at h1'
-  have h3 : l3.contr.countId  (l.contr.val.get x) = 1 := by
+  have h3 : l3.contr.countId (l.contr.val.get x) = 1 := by
     have h' := countSelf_le_countId l3.contr.toIndexList (l.contr.val.get x)
     have h'' := countId_contr_le_one l3 (l.contr.val.get x)
     omega
@@ -411,7 +411,6 @@ lemma contrPermEquiv_trans {l l2 l3 : ColorIndexList 𝓒}
     rw [← List.mem_singleton, ← ha]
     simp [AreDualInOther]
 
-
 @[simp]
 lemma contrPermEquiv_self_contr {l : ColorIndexList 𝓒} :
     contrPermEquiv (contr_self : ContrPerm l l.contr) =
@@ -424,7 +423,7 @@ lemma contrPermEquiv_self_contr {l : ColorIndexList 𝓒} :
   symm
   have h1' : l.contr.countSelf (l.contr.val.get x) = 1 := by simp [contr]
   rw [iff_countSelf.mp contr_self] at h1'
-  have h3 : l.contr.contr.countId  (l.contr.val.get x) = 1 := by
+  have h3 : l.contr.contr.countId (l.contr.val.get x) = 1 := by
     have h' := countSelf_le_countId l.contr.contr.toIndexList (l.contr.val.get x)
     have h'' := countId_contr_le_one l.contr (l.contr.val.get x)
     omega

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

@@ -83,8 +83,8 @@ lemma countColorQuot_eq_filter_id_countP (I : Index 𝓒.Color) :
 
 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
-    (fun J =>  I.id = J.id) := by
+    (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]
   apply List.countP_congr
@@ -450,7 +450,6 @@ lemma iff_countColorCond_mem (hl : l.OnlyUniqueDuals) :
     exact h ⟨i, hi'⟩ hi
   · exact h (l.val.get i) (List.getElem_mem l.val (↑i) i.isLt) hi
 
-
 lemma mem_iff_dual_mem (hl : l.OnlyUniqueDuals) (hc : l.ColorCond) (I : Index 𝓒.Color)
     (hId : l.countId I = 2) : I ∈ l.val ↔ I.dual ∈ l.val := by
   rw [iff_countColorCond_mem hl] at hc
@@ -547,7 +546,7 @@ lemma contrIndexList_left (hl : (l ++ l2).OnlyUniqueDuals) (h1 : (l ++ l2).Color
   intro I hI1 hI2
   simp only [countSelf_append, ne_eq] at hI1
   have hc := countSelf_contrIndexList_le_countSelf l I
-  have h2 := (countId_eq_two_ofcontrIndexList_left_of_OnlyUniqueDuals l l2 hl I hI2 )
+  have h2 := (countId_eq_two_ofcontrIndexList_left_of_OnlyUniqueDuals l l2 hl I hI2)
   have hI1' := h1 I (by simp_all; omega) h2
   have hIdEq : l.contrIndexList.countId I = l.countId I := by
     simp at h2 hI2

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

@@ -8,10 +8,8 @@ import HepLean.SpaceTime.LorentzTensor.IndexNotation.IndexList.Duals
 
 # Counting ids
 
-
 -/
 
-
 namespace IndexNotation
 
 namespace IndexList
@@ -19,7 +17,6 @@ namespace IndexList
 variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X]
 variable (l l2 l3 : IndexList X)
 
-
 /-!
 
 ## countId
@@ -112,7 +109,7 @@ lemma countId_mem (I : Index X) (hI : I ∈ l.val) : l.countId I ≠ 0 := by
   simp at 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
+    (List.finRange l2.length).countP (fun j => l.AreDualInOther l2 i j) := by
   rw [countId_eq_length_filter]
   rw [List.countP_eq_length_filter]
   have hl2 : l2.val = List.map l2.val.get (List.finRange l2.length) := by
@@ -158,7 +155,7 @@ lemma countId_get (i : Fin l.length) : l.countId (l.val.get i) =
     ((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)
+      List.countP (fun j => l.AreDualInOther l i j)
       (List.filter (fun j => i = j) (List.finRange l.length)) := by
     rw [List.countP_filter, List.countP_filter]
     refine List.countP_congr (fun j _ => ?_)
@@ -189,7 +186,6 @@ lemma countId_gt_zero_of_mem_withDual (i : Fin l.length) (h : i ∈ l.withDual)
   rw [hn] at hjmem
   simp at hjmem
 
-
 lemma countId_of_not_mem_withDual (i : Fin l.length)(h : i ∉ l.withDual) :
     l.countId (l.val.get i) = 1 := by
   rw [countId_get]
@@ -215,7 +211,7 @@ lemma countId_neq_zero_of_mem_withDualInOther (i : Fin l.length) (h : i ∈ l.wi
   by_contra hn
   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
+  have hjmem : l2.val.get j ∈ List.filter (fun J => decide ((l.val.get i).id = J.id)) l2.val := by
     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
@@ -231,7 +227,7 @@ lemma countId_of_not_mem_withDualInOther (i : Fin l.length) (h : i ∉ l.withDua
   have hx := eq_false_of_ne_true hn
   rw [List.isEmpty_false_iff_exists_mem] at hx
   obtain ⟨j, hj⟩ := hx
-  have hjmem : j ∈ l2.val :=  List.mem_of_mem_filter hj
+  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
   rw [mem_withInDualOther_iff_exists] at h
   simp at h
@@ -263,8 +259,8 @@ lemma countId_eq_two_of_mem_withUniqueDual (i : Fin l.length) (h : i ∈ l.withU
     l.countId (l.val.get i) = 2 := by
   rw [countId_get]
   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
+  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']
     · simp [List.filter, i']
     trans List.filter (fun j => (l.AreDualInSelf i j))
@@ -307,7 +303,7 @@ lemma mem_withUniqueDual_of_countId_eq_two (i : Fin l.length)
   rw [ha] at hj
   simp at hj
   subst hj
-  have ht : (l.getDual? i).get ((mem_withDual_iff_isSome l i).mp hw)  ∈
+  have ht : (l.getDual? i).get ((mem_withDual_iff_isSome l i).mp hw) ∈
     (List.finRange l.length).filter (fun j => decide (l.AreDualInSelf i j)) := by
       simp
   rw [ha] at ht
@@ -323,8 +319,8 @@ lemma mem_withUniqueDual_iff_countId_eq_two (i : Fin l.length) :
 lemma countId_eq_one_of_mem_withUniqueDualInOther (i : Fin l.length)
     (h : i ∈ l.withUniqueDualInOther l2) :
     l.countId (l.val.get i) = 1 ∧ l2.countId (l.val.get i) = 1 := by
-  let i' :=  (l.getDualInOther? l2 i).get (mem_withUniqueDualInOther_isSome l l2 i h)
-  have h1 :  [i'] = (List.finRange l2.length).filter (fun j => (l.AreDualInOther l2 i j)) := by
+  let i' := (l.getDualInOther? l2 i).get (mem_withUniqueDualInOther_isSome l l2 i h)
+  have h1 : [i'] = (List.finRange l2.length).filter (fun j => (l.AreDualInOther l2 i j)) := by
     trans List.filter (fun j => (l.AreDualInOther l2 i j)) [i']
     · simp [List.filter, i']
     trans List.filter (fun j => (l.AreDualInOther l2 i j))
@@ -378,7 +374,7 @@ lemma mem_withUniqueDualInOther_of_countId_eq_one (i : Fin l.length)
       rw [ha] at hj
       simp at hj
       subst hj
-      have ht : (l.getDualInOther? l2 i).get ((mem_withInDualOther_iff_isSome l l2 i).mp hw)  ∈
+      have ht : (l.getDualInOther? l2 i).get ((mem_withInDualOther_iff_isSome l l2 i).mp hw) ∈
         (List.finRange l2.length).filter (fun j => decide (l.AreDualInOther l2 i j)) := by
           simp
       rw [ha] at ht
@@ -432,7 +428,6 @@ lemma getDual?_isSome_of_countId_eq_two {i : Fin l.length}
 
 -/
 
-
 lemma filter_id_of_countId_eq_zero {i : Fin l.length} (h1 : l.countId (l.val.get i) = 0) :
     l.val.filter (fun J => (l.val.get i).id = J.id) = [] := by
   rw [countId_eq_length_filter, List.length_eq_zero] at h1

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

@@ -19,7 +19,6 @@ We also define the notion of dual indices in different lists. For example,
 
 -/
 
-
 namespace IndexNotation
 
 namespace IndexList

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

@@ -44,7 +44,6 @@ def dualEquiv : l.withDual ⊕ Fin l.withoutDual.card ≃ Fin l.length :=
   (Equiv.Finset.union _ _ l.withDual_disjoint_withoutDual).trans <|
   Equiv.subtypeUnivEquiv (by simp [withDual_union_withoutDual])
 
-
 /-!
 
 ## getDualEquiv
@@ -59,7 +58,7 @@ def getDualEquiv : l.withUniqueDual ≃ l.withUniqueDual where
   invFun x := ⟨(l.getDual? x).get (l.mem_withUniqueDual_isSome x.1 x.2), by
     rw [mem_withUniqueDual_iff_countId_eq_two]
     simpa using l.countId_eq_two_of_mem_withUniqueDual x.1 x.2⟩
-  left_inv x := SetCoe.ext <|  by
+  left_inv x := SetCoe.ext <| by
     let d := (l.getDual? x).get (l.mem_withUniqueDual_isSome x.1 x.2)
     have h1 : l.countId (l.val.get d) = 2 := by
       simpa [d] using l.countId_eq_two_of_mem_withUniqueDual x.1 x.2
@@ -90,7 +89,7 @@ def getDualEquiv : l.withUniqueDual ≃ l.withUniqueDual where
 
 @[simp]
 lemma getDual?_getDualEquiv (i : l.withUniqueDual) : l.getDual? (l.getDualEquiv i) = i := by
-  have h1  := (Equiv.apply_symm_apply l.getDualEquiv i).symm
+  have h1 := (Equiv.apply_symm_apply l.getDualEquiv i).symm
   nth_rewrite 2 [h1]
   nth_rewrite 2 [getDualEquiv]
   simp
@@ -105,7 +104,7 @@ def getDualInOtherEquiv : l.withUniqueDualInOther l2 ≃ l2.withUniqueDualInOthe
   invFun x := ⟨(l2.getDualInOther? l x).get (l2.mem_withUniqueDualInOther_isSome l x.1 x.2), by
     rw [mem_withUniqueDualInOther_iff_countId_eq_one]
     simpa using And.comm.mpr (l2.countId_eq_one_of_mem_withUniqueDualInOther l x.1 x.2)⟩
-  left_inv x := SetCoe.ext <|  by
+  left_inv x := SetCoe.ext <| by
     let d := (l.getDualInOther? l2 x).get (l.mem_withUniqueDualInOther_isSome l2 x.1 x.2)
     have h1 : l.countId (l2.val.get d) = 1 := by
       simpa [d] using (l.countId_eq_one_of_mem_withUniqueDualInOther l2 x.1 x.2).1
@@ -144,10 +143,9 @@ lemma getDualInOtherEquiv_self_refl : l.getDualInOtherEquiv l = Equiv.refl _ :=
   have hx2 := x.2
   simp [withUniqueDualInOther] at hx2
   apply Option.some_injective
-  rw [hx2.2 x.1 (by simp [ AreDualInOther]) ]
+  rw [hx2.2 x.1 (by simp [AreDualInOther])]
   simp
 
-
 @[simp]
 lemma getDualInOtherEquiv_symm : (l.getDualInOtherEquiv l2).symm = l2.getDualInOtherEquiv l := by
   rfl

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

@@ -63,7 +63,6 @@ lemma iff_countId_leq_two :
     have hi := h i
     omega
 
-
 lemma iff_countId_leq_two' : l.OnlyUniqueDuals ↔ ∀ I, l.countId I ≤ 2 := by
   rw [iff_countId_leq_two]
   refine Iff.intro (fun h I => ?_) (fun h i => h (l.val.get i))
@@ -163,15 +162,14 @@ 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 only [countId_append]
   have h1 := countId_contrIndexList_le_countId l I
-  have h3 :=  countId_of_OnlyUniqueDuals _ h I
+  have h3 := countId_of_OnlyUniqueDuals _ h I
   simp at h3 h'
   omega
 
-
 end IndexList
 
 end IndexNotation

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

@@ -21,7 +21,7 @@ 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
+/-- An IndexList `l` is a subpermutation of `l2` if 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
 
@@ -69,7 +69,7 @@ lemma fst_eq_contrIndexList (h : l.Subperm l2) : l.contrIndexList = l := by
   apply ext
   simp [contrIndexList]
   intro I hI
-  have h' : l.countId I ≠ 0 := by exact countId_mem l I hI
+  have h' := countId_mem l I hI
   have hI' := h I
   omega
 

HepLean/SpaceTime/LorentzTensor/Real/IndexNotation.lean

@@ -103,7 +103,7 @@ macro "prodTactic" : tactic =>
     `(tactic| {
     apply (ColorIndexList.AppendCond.iff_bool _ _).mpr
     change @ColorIndexList.AppendCond.bool realTensorColor
-       instDecidableEqColorRealTensorColor _ _
+      instDecidableEqColorRealTensorColor _ _
     simp only [prod_toIndexList, indexNotation_eq_color, fromIndexStringColor, mkDualMap,
       toTensorColor_eq, decidableEq_eq_color]
     rfl})