refactor: More countId

HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean

@@ -437,7 +437,7 @@ lemma countId_index_neq_zero (i : Fin l.length) : l.countId (l.val.get i) ≠ 0
   simp at hm
 
 lemma countId_append_symm (I : Index X) : (l ++ l2).countId I = (l2 ++ l).countId I := by
-  simp
+  simp only [countId_append]
   omega
 
 lemma countId_eq_one_append_mem_right_self_eq_one {I : Index X} (hI : I ∈ l2.val)

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

@@ -97,17 +97,16 @@ lemma contr_areDualInSelf (i j : Fin l.contr.length) :
     l.contr.AreDualInSelf i j ↔ False := by
   simp [contr]
 
-lemma contr_countP_eq_zero_of_countP (I : Index 𝓒.Color)
-    (h : l.val.countP (fun J => I.id = J.id) = 0) :
-    l.contr.val.countP (fun J => I.id = J.id) = 0 := by
+lemma contr_countId_eq_zero_of_countId_zero (I : Index 𝓒.Color)
+    (h : l.countId I = 0) : l.contr.countId I = 0 := by
   simp [contr]
-  exact countP_contrIndexList_zero_of_countP l.toIndexList I h
+  exact countId_contrIndexList_zero_of_countId l.toIndexList I h
 
-lemma contr_countP (I : Index 𝓒.Color) :
-    l.contr.val.countP (fun J => I.id = J.id) =
+lemma contr_countId_eq_filter (I : Index 𝓒.Color) :
+    l.contr.countId I =
     (l.val.filter (fun J => I.id = J.id)).countP
     (fun i => l.val.countP (fun j => i.id = j.id) = 1) := by
-  simp [contr, contrIndexList]
+  simp [contr, contrIndexList, countId]
   rw [List.countP_filter, List.countP_filter]
   congr
   funext J
@@ -115,18 +114,17 @@ lemma contr_countP (I : Index 𝓒.Color) :
   exact Bool.and_comm (decide (I.id = J.id))
     (decide (List.countP (fun j => decide (J.id = j.id)) l.val = 1))
 
-lemma contr_cons_dual (I : Index 𝓒.Color) (hI1 : l.val.countP (fun J => I.id = J.id) ≤ 1) :
-    l.contr.val.countP (fun J => I.id = J.id) ≤ 1 := by
-  rw [contr_countP]
-  by_cases hI1 : l.val.countP (fun J => I.id = J.id) = 0
-  · rw [filter_of_countP_zero]
-    · simp
-    · exact hI1
-  · have hI1 : l.val.countP (fun J => I.id = J.id) = 1 := by
+lemma countId_contr_le_one_of_countId (I : Index 𝓒.Color) (hI1 : l.countId I ≤ 1) :
+    l.contr.countId I ≤ 1 := by
+  rw [contr_countId_eq_filter]
+  by_cases hI1 : l.countId I = 0
+  · rw [l.filter_id_of_countId_eq_zero' hI1]
+    simp
+  · have hI1 : l.countId I = 1 := by
       omega
-    rw [consDual_filter]
-    · simp_all
-    · exact hI1
+    rw [l.consDual_filter hI1]
+    apply (List.countP_le_length _).trans
+    rfl
 
 /-!
 

HepLean/SpaceTime/LorentzTensor/IndexNotation/OnlyUniqueDuals.lean

@@ -173,6 +173,11 @@ lemma filter_id_of_countId_eq_zero {i : Fin l.length} (h1 : l.countId (l.val.get
   rw [countId_eq_length_filter, List.length_eq_zero] at h1
   exact h1
 
+lemma filter_id_of_countId_eq_zero' {I : Index X} (h1 : l.countId I = 0) :
+    l.val.filter (fun J => I.id = J.id) = [] := by
+  rw [countId_eq_length_filter, List.length_eq_zero] at h1
+  exact h1
+
 lemma filter_id_of_countId_eq_one {i : Fin l.length} (h1 : l.countId (l.val.get i) = 1) :
     l.val.filter (fun J => (l.val.get i).id = J.id) = [l.val.get i] := by
   rw [countId_eq_length_filter, List.length_eq_one] at h1