refactor: Lint

HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean

@@ -405,46 +405,45 @@ lemma countP_id_neq_zero (i : Fin l.length) :
   rw [List.countP_eq_length_filter]
   by_contra hn
   rw [List.length_eq_zero] at hn
-  have hm : l.val.get i ∈ List.filter (fun J => decide ((l.val.get i).id = J.id)) l.val  := by
+  have hm : l.val.get i ∈ List.filter (fun J => decide ((l.val.get i).id = J.id)) l.val := by
     simpa using List.getElem_mem l.val i.1 i.isLt
   rw [hn] at hm
   simp at hm
 
-
 /-! TODO: Replace with Mathlib lemma. -/
-lemma filter_sort_comm  {n : ℕ} (s : Finset (Fin n)) (p : Fin n → Prop) [DecidablePred p] :
-      List.filter p (Finset.sort (fun i j => i ≤ j) s) =
-      Finset.sort (fun i j => i ≤ j) (Finset.filter p s) := by
-    simp [Finset.filter, Finset.sort]
-    have : ∀ (m : Multiset (Fin n)), List.filter p (Multiset.sort (fun i j => i ≤ j) m) =
-        Multiset.sort (fun i j => i ≤ j) (Multiset.filter p m) := by
-      apply Quot.ind
-      intro m
-      simp [List.mergeSort]
-      have h1 : List.Sorted (fun i j => i ≤ j) (List.filter (fun b => decide (p b))
-          (List.mergeSort (fun i j => i ≤ j) m)) := by
-        simp [List.Sorted]
-        rw [List.pairwise_filter]
-        rw [@List.pairwise_iff_get]
-        intro i j h1 _ _
-        have hs : List.Sorted (fun i j => i ≤ j) (List.mergeSort (fun i j => i ≤ j) m) := by
-          exact List.sorted_mergeSort (fun i j => i ≤ j) m
-        simp [List.Sorted] at hs
-        rw [List.pairwise_iff_get] at hs
-        exact hs i j h1
-      have hp1 : (List.mergeSort (fun i j => i ≤ j) m).Perm m := by
-        exact List.perm_mergeSort (fun i j => i ≤ j) m
-      have hp2 : (List.filter (fun b => decide (p b)) ((List.mergeSort (fun i j => i ≤ j) m))).Perm
-          (List.filter (fun b => decide (p b)) m) := by
-        exact List.Perm.filter (fun b => decide (p b)) hp1
-      have hp3 : (List.filter (fun b => decide (p b)) m).Perm
-        (List.mergeSort (fun i j => i ≤ j) (List.filter (fun b => decide (p b)) m)) := by
-        exact List.Perm.symm (List.perm_mergeSort (fun i j => i ≤ j)
-        (List.filter (fun b => decide (p b)) m))
-      have hp4 := hp2.trans hp3
-      refine List.eq_of_perm_of_sorted hp4 h1 ?_
-      exact List.sorted_mergeSort (fun i j => i ≤ j) (List.filter (fun b => decide (p b)) m)
-    exact this s.val
+lemma filter_sort_comm {n : ℕ} (s : Finset (Fin n)) (p : Fin n → Prop) [DecidablePred p] :
+    List.filter p (Finset.sort (fun i j => i ≤ j) s) =
+    Finset.sort (fun i j => i ≤ j) (Finset.filter p s) := by
+  simp [Finset.filter, Finset.sort]
+  have : ∀ (m : Multiset (Fin n)), List.filter p (Multiset.sort (fun i j => i ≤ j) m) =
+      Multiset.sort (fun i j => i ≤ j) (Multiset.filter p m) := by
+    apply Quot.ind
+    intro m
+    simp [List.mergeSort]
+    have h1 : List.Sorted (fun i j => i ≤ j) (List.filter (fun b => decide (p b))
+        (List.mergeSort (fun i j => i ≤ j) m)) := by
+      simp [List.Sorted]
+      rw [List.pairwise_filter]
+      rw [@List.pairwise_iff_get]
+      intro i j h1 _ _
+      have hs : List.Sorted (fun i j => i ≤ j) (List.mergeSort (fun i j => i ≤ j) m) := by
+        exact List.sorted_mergeSort (fun i j => i ≤ j) m
+      simp [List.Sorted] at hs
+      rw [List.pairwise_iff_get] at hs
+      exact hs i j h1
+    have hp1 : (List.mergeSort (fun i j => i ≤ j) m).Perm m := by
+      exact List.perm_mergeSort (fun i j => i ≤ j) m
+    have hp2 : (List.filter (fun b => decide (p b)) ((List.mergeSort (fun i j => i ≤ j) m))).Perm
+        (List.filter (fun b => decide (p b)) m) := by
+      exact List.Perm.filter (fun b => decide (p b)) hp1
+    have hp3 : (List.filter (fun b => decide (p b)) m).Perm
+      (List.mergeSort (fun i j => i ≤ j) (List.filter (fun b => decide (p b)) m)) := by
+      exact List.Perm.symm (List.perm_mergeSort (fun i j => i ≤ j)
+      (List.filter (fun b => decide (p b)) m))
+    have hp4 := hp2.trans hp3
+    refine List.eq_of_perm_of_sorted hp4 h1 ?_
+    exact List.sorted_mergeSort (fun i j => i ≤ j) (List.filter (fun b => decide (p b)) m)
+  exact this s.val
 
 lemma filter_id_eq_sort (i : Fin l.length) : l.val.filter (fun J => (l.val.get i).id = J.id) =
     List.map l.val.get (Finset.sort (fun i j => i ≤ j)

HepLean/SpaceTime/LorentzTensor/IndexNotation/Color.lean

@@ -332,7 +332,7 @@ lemma orderEmbOfFin_univ (n m : ℕ) (h : n = m) :
 
 -/
 
-/-! TODO: Define `cons` for  `ColorIndexList`. Will need conditions unlike for `IndexList`. -/
+/-! TODO: Define `cons` for `ColorIndexList`. Will need conditions unlike for `IndexList`. -/
 
 /-!
 

HepLean/SpaceTime/LorentzTensor/IndexNotation/OnlyUniqueDuals.lean

@@ -124,7 +124,6 @@ lemma withUnqiueDual_eq_withDual_of_empty (h : l.withDual = ∅) :
   have hx' := x'.2
   simp [h] at hx'
 
-
 lemma withUniqueDual_eq_withDual_iff_sort_eq :
     l.withUniqueDual = l.withDual ↔
     l.withUniqueDual.sort (fun i j => i ≤ j) = l.withDual.sort (fun i j => i ≤ j) := by
@@ -184,7 +183,8 @@ lemma withUniqueDual_eq_withDual_cons_iff (I : Index X) (hl : l.withUniqueDual =
     (l.cons I).withUniqueDual = (l.cons I).withDual
     ↔ l.val.countP (fun J => I.id = J.id) ≤ 1 := by
   rw [withUniqueDual_eq_withDual_iff_all_countP_le_two]
-  simp
+  simp only [cons_val, List.all_cons, decide_True, List.countP_cons_of_pos, Nat.reduceLeDiff,
+    Bool.and_eq_true, decide_eq_true_eq, List.all_eq_true, and_iff_left_iff_imp]
   intro h I' hI'
   by_cases hII' : I'.id = I.id
   · rw [List.countP_cons_of_pos]

HepLean/SpaceTime/LorentzTensor/IndexNotation/WithUniqueDual.lean

@@ -921,7 +921,7 @@ lemma finset_filter_id_mem_withUniqueDual (i : Fin l.length) (h : i ∈ l.withUn
     Finset.filter (fun j => l.idMap i = l.idMap j) Finset.univ =
     {i, (l.getDual? i).get (l.mem_withUniqueDual_isSome i h)} := by
   refine Finset.ext (fun j => ?_)
-  simp
+  simp only [Finset.mem_filter, Finset.mem_univ, true_and, Finset.mem_insert, Finset.mem_singleton]
   rw [← propext (eq_getDual?_get_of_withUniqueDual_iff l i j h)]
   simp only [AreDualInSelf, ne_eq]
   refine Iff.intro (fun h => ?_) (fun h=> ?_)
@@ -959,10 +959,11 @@ lemma mem__withUniqueDual_iff_finset_filter (i : Fin l.length) (h : i ∈ l.with
 
 /-! TODO: Move -/
 lemma card_finset_self_dual (i : Fin l.length) (h : i ∈ l.withDual) :
-   ({i, (l.getDual? i).get ((mem_withDual_iff_isSome l i).mp h)} : Finset (Fin l.length)).card = 2 := by
+    ({i, (l.getDual? i).get ((mem_withDual_iff_isSome l i).mp h)} :
+    Finset (Fin l.length)).card = 2 := by
   rw [Finset.card_eq_two]
   use i, (l.getDual? i).get ((mem_withDual_iff_isSome l i).mp h)
-  simp
+  simp only [ne_eq, and_true]
   have h1 : l.AreDualInSelf i ((l.getDual? i).get ((mem_withDual_iff_isSome l i).mp h)) := by
     simp
   exact h1.1