refactor: Lint

HepLean/SpaceTime/LorentzTensor/IndexNotation/Contraction.lean

@@ -390,8 +390,8 @@ lemma mem_contrIndexList_filter {I : Index X} (h : I ∈ l.contrIndexList.val) :
     rw [← List.countP_eq_length_filter]
     exact l.mem_contrIndexList_count h
   have h2 : I ∈ l.val.filter (fun J => I.id = J.id) := by
-    simp
-    simp [contrIndexList] at h
+    simp only [List.mem_filter, decide_True, and_true]
+    simp only [contrIndexList, List.mem_filter, decide_eq_true_eq] at h
     exact h.1
   rw [List.length_eq_one] at h1
   obtain ⟨J, hJ⟩ := h1
@@ -433,7 +433,7 @@ lemma cons_contrIndexList_of_countP_neq_zero {I : Index X}
       simp only [h, not_false_eq_true]
     · simp only [hI, decide_False, Bool.not_false, Bool.true_and, decide_eq_decide]
       rw [List.countP_cons_of_neg]
-      simp
+      simp only [decide_eq_true_eq]
       exact fun a => hI (id (Eq.symm a))
   · simp only [decide_True, List.countP_cons_of_pos, add_left_eq_self, decide_eq_true_eq]
     exact h
@@ -460,7 +460,7 @@ lemma countP_contrIndexList_zero_of_countP (I : Index X)
   trans (l.val.filter (fun J => I.id = J.id)).countP
     (fun i => l.val.countP (fun j => i.id = j.id) = 1)
   · rw [contrIndexList]
-    simp
+    simp only
     rw [List.countP_filter, List.countP_filter]
     simp only [decide_eq_true_eq, Bool.decide_and]
     congr

HepLean/SpaceTime/LorentzTensor/IndexNotation/Relations.lean

@@ -39,7 +39,7 @@ open IndexList TensorColor
 -/
 def Reindexing : Prop := l.length = l'.length ∧
   ∀ (h : l.length = l'.length), l.colorMap = l'.colorMap ∘ Fin.cast h ∧
-    l.getDual? = Option.map (Fin.cast h.symm) ∘  l'.getDual? ∘ Fin.cast h
+    l.getDual? = Option.map (Fin.cast h.symm) ∘ l'.getDual? ∘ Fin.cast h
 
 namespace Reindexing
 
@@ -58,7 +58,7 @@ lemma symm (h : Reindexing l l') : Reindexing l' l := by
   · rw [h2.2]
     funext a
     simp only [Function.comp_apply, Fin.cast_trans, Fin.cast_eq_self, Option.map_map]
-    have h1 (h : l.length = l'.length) : Fin.cast h ∘  Fin.cast h.symm = id := by
+    have h1 (h : l.length = l'.length) : Fin.cast h ∘ Fin.cast h.symm = id := by
       funext a
       simp only [Function.comp_apply, Fin.cast_trans, Fin.cast_eq_self, id_eq]
     rw [h1]

HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean

@@ -286,7 +286,6 @@ lemma rel_contr (T : 𝓣.TensorIndex) : T ≈ T.contr := by
   apply congrArg
   rfl
 
-
 /-!
 
 ## Scalar multiplication of
@@ -344,7 +343,7 @@ lemma symm {T₁ T₂ : 𝓣.TensorIndex} (h : AddCond T₁ T₂) : AddCond T₂
   rw [AddCond] at h
   exact h.symm
 
-lemma refl (T : 𝓣.TensorIndex) : AddCond T T := ContrPerm.refl
+lemma refl (T : 𝓣.TensorIndex) : AddCond T T := ContrPerm.refl T.toColorIndexList
 
 lemma trans {T₁ T₂ T₃ : 𝓣.TensorIndex} (h1 : AddCond T₁ T₂) (h2 : AddCond T₂ T₃) :
     AddCond T₁ T₃ := by
@@ -479,7 +478,7 @@ lemma add_comm {T₁ T₂ : 𝓣.TensorIndex} (h : AddCond T₁ T₂) : T₁ +[h
 open AddCond in
 lemma add_rel_left {T₁ T₁' T₂ : 𝓣.TensorIndex} (h : AddCond T₁ T₂) (h' : T₁ ≈ T₁') :
     T₁ +[h] T₂ ≈ T₁' +[h.rel_left h'] T₂ := by
-  apply And.intro ContrPerm.refl
+  apply And.intro (ContrPerm.refl _)
   intro h
   simp only [contr_add_tensor, add_tensor, map_add]
   apply Mathlib.Tactic.LinearCombination.add_pf