refactor: change simp to simp?

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

@@ -238,14 +238,17 @@ lemma append_val {l l2 : IndexList X} : (l ++ l2).val = l.val ++ l2.val := by
 @[simp]
 lemma idMap_append_inl {l l2 : IndexList X} (i : Fin l.length) :
     (l ++ l2).idMap (appendEquiv (Sum.inl i)) = l.idMap i := by
-  simp [appendEquiv, idMap]
+  simp only [idMap, append_val, appendEquiv, Equiv.trans_apply, finSumFinEquiv_apply_left,
+    List.get_eq_getElem]
   rw [List.getElem_append_left]
   rfl
 
 @[simp]
 lemma idMap_append_inr {l l2 : IndexList X} (i : Fin l2.length) :
     (l ++ l2).idMap (appendEquiv (Sum.inr i)) = l2.idMap i := by
-  simp [appendEquiv, idMap, IndexList.length]
+  simp only [idMap, append_val, length, appendEquiv, Equiv.trans_apply, finSumFinEquiv_apply_right,
+    RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply, List.get_eq_getElem, Fin.coe_cast,
+    Fin.coe_natAdd]
   rw [List.getElem_append_right]
   · simp only [Nat.add_sub_cancel_left]
   · omega

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

@@ -28,7 +28,7 @@ def dual : Index 𝓒.Color := ⟨𝓒.τ I.toColor, I.id⟩
 
 @[simp]
 lemma dual_dual : I.dual.dual = I := by
-  simp [dual, toColor, id]
+  simp only [dual, toColor, id]
   rw [𝓒.τ_involutive]
   rfl
 
@@ -53,11 +53,12 @@ lemma countColorQuot_eq_filter_id_countP (I : Index 𝓒.Color) :
     l.countColorQuot I =
     (l.val.filter (fun J => I.id = J.id)).countP
     (fun J => I.toColor = J.toColor ∨ I.toColor = 𝓒.τ (J.toColor)) := by
-  simp [countColorQuot]
+  simp only [countColorQuot, Bool.decide_or]
   rw [List.countP_filter]
   apply List.countP_congr
   intro I' _
-  simp [Index.eq_iff_color_eq_and_id_eq]
+  simp only [Index.eq_iff_color_eq_and_id_eq, Bool.decide_and, Index.dual_color, Index.dual_id,
+    Bool.or_eq_true, Bool.and_eq_true, decide_eq_true_eq, Bool.decide_or]
   apply Iff.intro
   · intro a_1
     cases a_1 with
@@ -158,7 +159,7 @@ def countSelf (I : Index 𝓒.Color) : ℕ := l.val.countP (fun J => I = J)
 
 lemma countSelf_eq_filter_id_countP : l.countSelf I =
     (l.val.filter (fun J => I.id = J.id)).countP (fun J => I.toColor = J.toColor) := by
-  simp [countSelf]
+  rw [countSelf]
   rw [List.countP_filter]
   apply List.countP_congr
   intro I' _
@@ -167,7 +168,7 @@ lemma countSelf_eq_filter_id_countP : l.countSelf I =
 lemma countSelf_eq_filter_color_countP :
     l.countSelf I =
     (l.val.filter (fun J => I.toColor = J.toColor)).countP (fun J => I.id = J.id) := by
-  simp [countSelf]
+  simp only [countSelf]
   rw [List.countP_filter]
   apply List.countP_congr
   intro I' _
@@ -253,11 +254,12 @@ lemma countDual_eq_countSelf_Dual (I : Index 𝓒.Color) : l.countDual I = l.cou
 
 lemma countDual_eq_filter_id_countP : l.countDual I =
     (l.val.filter (fun J => I.id = J.id)).countP (fun J => I.toColor = 𝓒.τ (J.toColor)) := by
-  simp [countDual]
+  simp only [countDual]
   rw [List.countP_filter]
   apply List.countP_congr
   intro I' _
-  simp [Index.eq_iff_color_eq_and_id_eq, Index.dual, Index.toColor, Index.id]
+  simp only [Index.dual, Index.toColor, Index.id, Index.eq_iff_color_eq_and_id_eq, Bool.decide_and,
+    Bool.and_eq_true, decide_eq_true_eq, and_congr_left_iff]
   intro _
   refine Iff.intro (fun h => ?_) (fun h => ?_)
   · rw [← h]
@@ -292,9 +294,10 @@ lemma countSelf_eq_countDual_iff_of_isSome (hl : l.OnlyUniqueDuals)
   rcases l.filter_id_of_countId_eq_two hi1 with hf | hf
   all_goals
     erw [hf]
-    simp [List.countP, List.countP.go]
+    simp only [List.countP, List.countP.go, List.get_eq_getElem, decide_True, zero_add,
+      Nat.reduceAdd, cond_true]
     by_cases hn : l.colorMap i = 𝓒.τ (l.colorMap ((l.getDual? i).get hi))
-    · simp [hn]
+    · simp only [hn, true_or, iff_true]
       have hn' : decide (l.val[↑i].toColor = 𝓒.τ l.val[↑((l.getDual? i).get hi)].toColor)
         = true := by simpa [colorMap] using hn
       erw [hn']
@@ -302,34 +305,34 @@ lemma countSelf_eq_countDual_iff_of_isSome (hl : l.OnlyUniqueDuals)
       have hτ : l.colorMap ((l.getDual? i).get hi) = 𝓒.τ (l.colorMap i) := by
         rw [hn]
         exact (𝓒.τ_involutive _).symm
-      simp [colorMap] at hτ
+      simp only [colorMap, List.get_eq_getElem] at hτ
       erw [hτ]
     · have hn' : decide (l.val[↑i].toColor = 𝓒.τ l.val[↑((l.getDual? i).get hi)].toColor) =
           false := by simpa [colorMap] using hn
       erw [hn']
-      simp [hn]
+      simp only [cond_false, hn, false_or]
       by_cases hm : l.colorMap i = 𝓒.τ (l.colorMap i)
       · trans True
-        · simp
+        · simp only [iff_true]
           have hm' : decide (l.val[↑i].toColor = 𝓒.τ l.val[↑i].toColor) = true := by simpa using hm
           erw [hm']
           simp only [cond_true]
           have hm'' : decide (l.val[↑i].toColor = l.val[↑((l.getDual? i).get hi)].toColor)
               = false := by
             simp only [Fin.getElem_fin, decide_eq_false_iff_not]
-            simp [colorMap] at hm
+            simp only [colorMap, List.get_eq_getElem] at hm
             erw [hm]
             by_contra hn'
             have hn'' : l.colorMap i = 𝓒.τ (l.colorMap ((l.getDual? i).get hi)) := by
-              simp [colorMap]
+              simp only [colorMap, List.get_eq_getElem]
               rw [← hn']
               exact (𝓒.τ_involutive _).symm
             exact hn hn''
           erw [hm'']
           rfl
         · exact true_iff_iff.mpr hm
-      · simp [hm]
-        simp [colorMap] at hm
+      · simp only [hm, iff_false, ne_eq]
+        simp only [colorMap, List.get_eq_getElem] at hm
         have hm' : decide (l.val[↑i].toColor = 𝓒.τ l.val[↑i].toColor) = false := by simpa using hm
         erw [hm']
         simp only [cond_false, ne_eq]
@@ -357,13 +360,13 @@ lemma iff_withDual :
     (l.colorMap ((l.getDual? i).get (l.withDual_isSome i))) = l.colorMap i := by
   refine Iff.intro (fun h i => ?_) (fun h => ?_)
   · have h' := congrFun h i
-    simp at h'
+    simp only [Function.comp_apply] at h'
     rw [show l.getDual? i = some ((l.getDual? i).get (l.withDual_isSome i)) by simp] at h'
     have h'' : (Option.guard (fun i => (l.getDual? i).isSome = true) ↑i) = i := by
       apply Option.guard_eq_some.mpr
       simp [l.withDual_isSome i]
     rw [h'', Option.map_some', Option.map_some'] at h'
-    simp at h'
+    simp only [Function.comp_apply, Option.some.injEq] at h'
     rw [h']
     exact 𝓒.τ_involutive (l.colorMap i)
   · funext i
@@ -376,10 +379,11 @@ lemma iff_withDual :
       rw [Option.eq_some_of_isSome hi, Option.map_some']
       simp only [Option.some.injEq]
       have hii := h ⟨i, (mem_withDual_iff_isSome l i).mpr hi⟩
-      simp at hii
+      simp only at hii
       rw [← hii]
       exact (𝓒.τ_involutive _).symm
-    · simp [Option.guard, hi]
+    · simp only [Function.comp_apply, Option.guard, hi, Bool.false_eq_true, ↓reduceIte,
+      Option.map_none', Option.map_eq_none']
       exact Option.not_isSome_iff_eq_none.mp hi
 
 omit [DecidableEq 𝓒.Color] in
@@ -462,7 +466,7 @@ lemma mem_iff_dual_mem (hl : l.OnlyUniqueDuals) (hc : l.ColorCond) (I : Index
     have hc' := (hc I.dual h hIdd).2
     rw [← countSelf_neq_zero] at h ⊢
     rw [countDual_eq_countSelf_Dual] at hc'
-    simp at hc'
+    simp only [Index.dual_dual] at hc'
     exact Ne.symm (ne_of_ne_of_eq (id (Ne.symm h)) hc')
 
 lemma iff_countColorCond (hl : l.OnlyUniqueDuals) :
@@ -498,12 +502,13 @@ lemma inl (hl : (l ++ l2).OnlyUniqueDuals) (h : ColorCond (l ++ l2)) : ColorCond
   have hI2' : l2.countId I = 0 := by
     rw [OnlyUniqueDuals.iff_countId_leq_two'] at hl
     have hlI := hl I
-    simp at hlI
+    simp only [countId_append] at hlI
     omega
   have hI' := h I (by
     simp only [countSelf_append, ne_eq, add_eq_zero, not_and, hI1, false_implies])
     (by simp_all)
-  simp at hI'
+  simp only [countColorCond, countColorQuot_append, countId_append, countSelf_append,
+    countDual_append] at hI'
   rw [l2.countColorQuot_of_countId_zero hI2', l2.countSelf_of_countId_zero hI2',
     l2.countDual_of_countId_zero hI2', hI2'] at hI'
   exact hI'
@@ -542,7 +547,7 @@ lemma contrIndexList_left (hl : (l ++ l2).OnlyUniqueDuals) (h1 : (l ++ l2).Color
   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
+    simp only [countId_append] at h2 hI2
     omega
   simp only [countColorCond, countColorQuot_append, countId_append, countSelf_append,
     countDual_append]

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

@@ -89,20 +89,22 @@ lemma contrIndexList_length : l.contrIndexList.length = l.withoutDual.card := by
 @[simp]
 lemma contrIndexList_idMap (i : Fin l.contrIndexList.length) : l.contrIndexList.idMap i
     = l.idMap (l.withoutDualEquiv (Fin.cast l.contrIndexList_length i)).1 := by
-  simp [contrIndexList_eq_contrIndexList', idMap]
+  simp only [idMap, List.get_eq_getElem, contrIndexList_eq_contrIndexList', contrIndexList',
+    List.getElem_ofFn, Function.comp_apply]
   rfl
 
 @[simp]
 lemma contrIndexList_colorMap (i : Fin l.contrIndexList.length) : l.contrIndexList.colorMap i
     = l.colorMap (l.withoutDualEquiv (Fin.cast l.contrIndexList_length i)).1 := by
-  simp [contrIndexList_eq_contrIndexList', colorMap]
+  simp only [colorMap, List.get_eq_getElem, contrIndexList_eq_contrIndexList', contrIndexList',
+    List.getElem_ofFn, Function.comp_apply]
   rfl
 
 lemma contrIndexList_areDualInSelf (i j : Fin l.contrIndexList.length) :
     l.contrIndexList.AreDualInSelf i j ↔
     l.AreDualInSelf (l.withoutDualEquiv (Fin.cast l.contrIndexList_length i)).1
       (l.withoutDualEquiv (Fin.cast l.contrIndexList_length j)).1 := by
-  simp [AreDualInSelf]
+  simp only [AreDualInSelf, ne_eq, contrIndexList_idMap, and_congr_left_iff]
   intro _
   trans ¬ (l.withoutDualEquiv (Fin.cast l.contrIndexList_length i)) =
     (l.withoutDualEquiv (Fin.cast l.contrIndexList_length j))
@@ -151,10 +153,11 @@ lemma contrIndexList_of_withDual_empty (h : l.withDual = ∅) : l.contrIndexList
   rw [contrIndexList_length, h1]
   simp only [Finset.card_univ, Fintype.card_fin, List.get_eq_getElem, true_and]
   intro n h1' h2
-  simp [contrIndexList_eq_contrIndexList']
+  simp only [contrIndexList_eq_contrIndexList', contrIndexList', List.getElem_ofFn,
+    Function.comp_apply, List.get_eq_getElem]
   congr
-  simp [withoutDualEquiv]
-  simp [h1]
+  simp only [withoutDualEquiv, RelIso.coe_fn_toEquiv, Finset.coe_orderIsoOfFin_apply]
+  simp only [h1]
   rw [(Finset.orderEmbOfFin_unique' _
     (fun x => Finset.mem_univ ((Fin.castOrderIso _).toOrderEmbedding x))).symm]
   · exact Eq.symm (Nat.add_zero n)
@@ -167,15 +170,15 @@ lemma contrIndexList_contrIndexList : l.contrIndexList.contrIndexList = l.contrI
 @[simp]
 lemma contrIndexList_getDualInOther?_self (i : Fin l.contrIndexList.length) :
     l.contrIndexList.getDualInOther? l.contrIndexList i = some i := by
-  simp [getDualInOther?]
+  simp only [getDualInOther?]
   rw [@Fin.find_eq_some_iff]
-  simp [AreDualInOther]
+  simp only [AreDualInOther, contrIndexList_idMap, true_and]
   intro j hj
   have h1 : i = j := by
     by_contra hn
     have h : l.contrIndexList.AreDualInSelf i j := by
       simp only [AreDualInSelf]
-      simp [hj]
+      simp only [ne_eq, contrIndexList_idMap, hj, and_true]
       exact hn
     exact (contrIndexList_areDualInSelf_false l i j).mp h
   exact Fin.ge_of_eq (id (Eq.symm h1))
@@ -184,7 +187,7 @@ lemma cons_contrIndexList_of_countId_eq_zero {I : Index X}
     (h : l.countId I = 0) :
     (l.cons I).contrIndexList = l.contrIndexList.cons I := by
   apply ext
-  simp [contrIndexList, countId]
+  simp only [contrIndexList, countId, cons_val]
   rw [List.filter_cons_of_pos]
   · apply congrArg
     apply List.filter_congr
@@ -233,7 +236,7 @@ lemma mem_contrIndexList_filter {I : Index X} (h : I ∈ l.contrIndexList.val) :
   rw [List.length_eq_one] at h1
   obtain ⟨J, hJ⟩ := h1
   rw [hJ] at h2
-  simp at h2
+  simp only [List.mem_singleton] at h2
   subst h2
   exact hJ
 
@@ -279,14 +282,14 @@ lemma countId_contrIndexList_eq_one_iff_countId_eq_one (I : Index X) :
     l.contrIndexList.countId I = 1 ↔ l.countId I = 1 := by
   refine Iff.intro (fun h => ?_) (fun h => ?_)
   · obtain ⟨I', hI1, hI2⟩ := countId_neq_zero_mem l.contrIndexList I (ne_zero_of_eq_one h)
-    simp [contrIndexList] at hI1
+    simp only [contrIndexList, List.mem_filter, decide_eq_true_eq] at hI1
     rw [countId_congr l hI2]
     exact hI1.2
   · obtain ⟨I', hI1, hI2⟩ := countId_neq_zero_mem l I (ne_zero_of_eq_one h)
     rw [countId_congr l hI2] at h
     rw [countId_congr _ hI2]
     refine mem_contrIndexList_countId_contrIndexList l ?_
-    simp [contrIndexList]
+    simp only [contrIndexList, List.mem_filter, decide_eq_true_eq]
     exact ⟨hI1, h⟩
 
 lemma countId_contrIndexList_le_countId (I : Index X) :
@@ -318,7 +321,8 @@ lemma filter_id_contrIndexList_eq_of_countId_contrIndexList (I : Index X)
 lemma contrIndexList_append_eq_filter : (l ++ l2).contrIndexList.val =
     l.contrIndexList.val.filter (fun I => l2.countId I = 0) ++
     l2.contrIndexList.val.filter (fun I => l.countId I = 0) := by
-  simp [contrIndexList]
+  simp only [contrIndexList, countId_append, append_val, List.filter_append, List.filter_filter,
+    decide_eq_true_eq, Bool.decide_and]
   congr 1
   · apply List.filter_congr
     intro I hI

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

@@ -132,7 +132,7 @@ lemma filter_finRange (i : Fin l.length) :
   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]
+    · rw [List.count]
       apply List.countP_congr (fun j _ => ?_)
       simp only [decide_eq_true_eq, beq_iff_eq]
       exact eq_comm
@@ -317,7 +317,7 @@ lemma mem_withUniqueDual_of_countId_eq_two (i : Fin l.length)
   have hj : j ∈ List.filter (fun j => decide (l.AreDualInSelf i j)) (List.finRange l.length) := by
     simpa using hj
   rw [ha] at hj
-  simp at hj
+  simp only [List.mem_singleton] at hj
   subst hj
   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

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

@@ -157,12 +157,12 @@ lemma not_mem_withDual_iff_isNone (i : Fin l.length) :
     Option.isNone_iff_eq_none]
 
 lemma mem_withDual_iff_exists : i ∈ l.withDual ↔ ∃ j, l.AreDualInSelf i j := by
-  simp [withDual, Finset.mem_filter, Finset.mem_univ, getDual?]
+  simp only [withDual, getDual?, Finset.mem_filter, Finset.mem_univ, true_and]
   exact Fin.isSome_find_iff
 
 lemma mem_withInDualOther_iff_exists :
     i ∈ l.withDualInOther l2 ↔ ∃ (j : Fin l2.length), l.AreDualInOther l2 i j := by
-  simp [withDualInOther, Finset.mem_filter, Finset.mem_univ, getDualInOther?]
+  simp only [withDualInOther, getDualInOther?, Finset.mem_filter, Finset.mem_univ, true_and]
   exact Fin.isSome_find_iff
 
 lemma withDual_disjoint_withoutDual : Disjoint l.withDual l.withoutDual := by
@@ -183,7 +183,7 @@ lemma withDual_union_withoutDual : l.withDual ∪ l.withoutDual = Finset.univ :=
   intro i
   by_cases h : (l.getDual? i).isSome
   · simp [withDual, Finset.mem_filter, Finset.mem_univ, h]
-  · simp at h
+  · simp only [Bool.not_eq_true, Option.not_isSome, Option.isNone_iff_eq_none] at h
     simp [withoutDual, Finset.mem_filter, Finset.mem_univ, h]
 
 lemma mem_withUniqueDual_of_mem_withUniqueDualLt (i : Fin l.length) (h : i ∈ l.withUniqueDualLT) :
@@ -308,7 +308,7 @@ lemma getDual?_of_areDualInSelf (h : l.AreDualInSelf i j) :
     by_cases hik' : i = k'
     · exact Fin.ge_of_eq (id (Eq.symm hik'))
     · have hik'' : l.AreDualInSelf i k' := by
-        simp [AreDualInSelf, hik']
+        simp only [AreDualInSelf, ne_eq, hik', not_false_eq_true, true_and]
         simp_all [AreDualInSelf]
       have hk'' := hk.2 k' hik''
       exact (lt_of_lt_of_le hik hk'').le
@@ -329,14 +329,14 @@ lemma getDual?_of_areDualInSelf (h : l.AreDualInSelf i j) :
       · subst hik'
         exact Lean.Omega.Fin.le_of_not_lt hik
       · have hik'' : l.AreDualInSelf i k' := by
-          simp [AreDualInSelf, hik']
-          simp_all [AreDualInSelf]
+          simp only [AreDualInSelf, ne_eq, hik', not_false_eq_true, true_and]
+          simp_all only [AreDualInSelf, ne_eq, and_imp, not_lt, not_le]
         exact hk.2 k' hik''
 
 @[simp]
 lemma getDual?_neq_self (i : Fin l.length) : ¬ l.getDual? i = some i := by
   intro h
-  simp [getDual?] at h
+  simp only [getDual?] at h
   rw [Fin.find_eq_some_iff] at h
   simp [AreDualInSelf] at h
 
@@ -356,7 +356,7 @@ lemma getDual?_get_id (i : Fin l.length) (h : (l.getDual? i).isSome) :
   have h1 : l.getDual? i = some ((l.getDual? i).get h) := Option.eq_some_of_isSome h
   nth_rewrite 1 [getDual?] at h1
   rw [Fin.find_eq_some_iff] at h1
-  simp [AreDualInSelf] at h1
+  simp only [AreDualInSelf, ne_eq, and_imp] at h1
   exact h1.1.2.symm
 
 @[simp]
@@ -392,7 +392,7 @@ lemma getDualInOther?_id (i : Fin l.length) (h : (l.getDualInOther? l2 i).isSome
     Option.eq_some_of_isSome h
   nth_rewrite 1 [getDualInOther?] at h1
   rw [Fin.find_eq_some_iff] at h1
-  simp [AreDualInOther] at h1
+  simp only [AreDualInOther] at h1
   exact h1.1.symm
 
 @[simp]
@@ -415,7 +415,7 @@ lemma getDualInOther?_getDualInOther?_get_isSome (i : Fin l.length)
 @[simp]
 lemma getDualInOther?_self_isSome (i : Fin l.length) :
     (l.getDualInOther? l i).isSome := by
-  simp [getDualInOther?]
+  simp only [getDualInOther?]
   rw [@Fin.isSome_find_iff]
   exact ⟨i, rfl⟩
 
@@ -425,7 +425,7 @@ lemma getDualInOther?_getDualInOther?_get_self (i : Fin l.length) :
     some ((l.getDualInOther? l i).get (getDualInOther?_self_isSome l i)) := by
   nth_rewrite 1 [getDualInOther?]
   rw [Fin.find_eq_some_iff]
-  simp [AreDualInOther]
+  simp only [AreDualInOther, getDualInOther?_id, true_and]
   intro j hj
   have h1 := Option.eq_some_of_isSome (getDualInOther?_self_isSome l i)
   nth_rewrite 1 [getDualInOther?] at h1

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

@@ -94,7 +94,7 @@ lemma getDual?_getDualEquiv (i : l.withUniqueDual) : l.getDual? (l.getDualEquiv
   have h1 := (Equiv.apply_symm_apply l.getDualEquiv i).symm
   nth_rewrite 2 [h1]
   nth_rewrite 2 [getDualEquiv]
-  simp
+  simp only [Equiv.coe_fn_mk, Option.some_get]
   rfl
 
 /-- An equivalence from `l.withUniqueDualInOther l2 ` to
@@ -140,7 +140,7 @@ omit [IndexNotation X] [Fintype X] in
 lemma getDualInOtherEquiv_self_refl : l.getDualInOtherEquiv l = Equiv.refl _ := by
   apply Equiv.ext
   intro x
-  simp [getDualInOtherEquiv]
+  simp only [getDualInOtherEquiv, Equiv.coe_fn_mk, Equiv.refl_apply]
   apply Subtype.eq
   simp only
   have hx2 := x.2

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

@@ -184,7 +184,7 @@ lemma findIdx?_on_finRange_eq_findIdx {n : ℕ} (p : Fin n → Prop) [DecidableP
           rw [@Fin.find_eq_some_iff] at hi ⊢
           simp_all only [Function.comp_apply, Fin.succ_pred, true_and]
           exact fun j hj => (Fin.pred_le_iff hn).mpr (hi.2 j.succ hj)
-        · simp at hs
+        · simp only [Bool.not_eq_true, Option.not_isSome, Option.isNone_iff_eq_none] at hs
           rw [hs]
           simp only [Nat.succ_eq_add_one, Option.map_eq_none']
           rw [@Fin.find_eq_none_iff] at hs ⊢
@@ -229,7 +229,8 @@ lemma idList_getDualInOther? : l.idList =
   rw [idList, idListFin_getDualInOther?]
 
 lemma mem_idList_of_mem {I : Index X} (hI : I ∈ l.val) : I.id ∈ l.idList := by
-  simp [idList_getDualInOther?]
+  simp only [idList_getDualInOther?, List.mem_map, List.mem_filter, List.mem_finRange,
+    decide_eq_true_eq, true_and]
   have hI : l.val.indexOf I < l.val.length := List.indexOf_lt_length.mpr hI
   have hI' : I = l.val.get ⟨l.val.indexOf I, hI⟩ := Eq.symm (List.indexOf_get hI)
   rw [hI']
@@ -257,7 +258,7 @@ lemma idList_indexOf_get (i : Fin l.length) :
     l.idList.indexOf (l.idMap i) = l.idListFin.indexOf ((l.getDualInOther? l i).get
       (getDualInOther?_self_isSome l i)) := by
   rw [idList]
-  simp [idListFin_getDualInOther?]
+  simp only [idListFin_getDualInOther?]
   rw [← indexOf_map' l.idMap (fun i => (l.getDualInOther? l i).get
       (getDualInOther?_self_isSome l i))]
   · intro i _ j
@@ -271,7 +272,7 @@ lemma idList_indexOf_get (i : Fin l.length) :
         · exact congrArg l.idMap h
         · exact getDualInOther?_id l l j (getDualInOther?_self_isSome l j)
   · intro i hi
-    simp at hi
+    simp only [List.mem_filter, List.mem_finRange, decide_eq_true_eq, true_and] at hi
     exact Option.get_of_mem (getDualInOther?_self_isSome l i) hi
   · exact fun i => Eq.symm (getDualInOther?_id l l i (getDualInOther?_self_isSome l i))
 
@@ -343,9 +344,9 @@ lemma areDualInSelf_of (h : GetDualCast l l2) (i j : Fin l.length) (hA : l.AreDu
     have h1 : ((l2.getDual? (Fin.cast h.1 j)).get ((getDual?_isSome_iff h j).mp hn))
         = ((l2.getDual? (Fin.cast h.1 i)).get ((getDual?_isSome_iff h i).mp hni)) := by
       simpa [Fin.ext_iff] using h1'
-    simp [AreDualInSelf]
+    simp only [AreDualInSelf, ne_eq]
     apply And.intro
-    · simp [AreDualInSelf] at hA
+    · simp only [AreDualInSelf, ne_eq] at hA
       simpa [Fin.ext_iff] using hA.1
     trans l2.idMap ((l2.getDual? (Fin.cast h.1 j)).get ((getDual?_isSome_iff h j).mp hn))
     · trans l2.idMap ((l2.getDual? (Fin.cast h.1 i)).get ((getDual?_isSome_iff h i).mp hni))
@@ -367,7 +368,7 @@ lemma idMap_eq_of (h : GetDualCast l l2) (i j : Fin l.length) (hm : l.idMap i =
   by_cases h1 : i = j
   · exact congrArg l2.idMap (congrArg (Fin.cast h.left) h1)
   have h1' : l.AreDualInSelf i j := by
-    simp [AreDualInSelf]
+    simp only [AreDualInSelf, ne_eq]
     exact ⟨h1, hm⟩
   rw [h.areDualInSelf_iff] at h1'
   simpa using h1'.2
@@ -390,10 +391,10 @@ lemma iff_idMap_eq : GetDualCast l l2 ↔
   simp only [Function.comp_apply]
   by_cases h1 : (l.getDual? i).isSome
   · have h1' : (l2.getDual? (Fin.cast h.1 i)).isSome := by
-      simp [getDual?, Fin.isSome_find_iff] at h1 ⊢
+      simp only [getDual?, Fin.isSome_find_iff] at h1 ⊢
       obtain ⟨j, hj⟩ := h1
       use (Fin.cast h.1 j)
-      simp [AreDualInSelf] at hj ⊢
+      simp only [AreDualInSelf, ne_eq] at hj ⊢
       rw [← h.2]
       simpa [Fin.ext_iff] using hj
     have h2 := Option.eq_some_of_isSome h1'
@@ -402,26 +403,26 @@ lemma iff_idMap_eq : GetDualCast l l2 ↔
     rw [Fin.find_eq_some_iff] at h2 ⊢
     apply And.intro
     · apply And.intro
-      · simp [AreDualInSelf] at h2
+      · simp only [AreDualInSelf, ne_eq, getDual?_get_id, and_true, and_imp] at h2
         simpa [Fin.ext_iff] using h2.1
       · rw [h.2 h.1]
         simp
     · intro j hj
       apply h2.2 (Fin.cast h.1 j)
-      simp [AreDualInSelf] at hj ⊢
+      simp only [AreDualInSelf, ne_eq] at hj ⊢
       apply And.intro
       · simpa [Fin.ext_iff] using hj.1
       · rw [← h.2]
         simpa using hj.2
-  · simp at h1
+  · simp only [Bool.not_eq_true, Option.not_isSome, Option.isNone_iff_eq_none] at h1
     rw [h1]
     symm
     refine Option.map_eq_none'.mpr ?_
     rw [getDual?, Fin.find_eq_none_iff] at h1 ⊢
-    simp [AreDualInSelf]
+    simp only [AreDualInSelf, ne_eq, not_and]
     intro j hij
     have h1j := h1 (Fin.cast h.1.symm j)
-    simp [AreDualInSelf] at h1j
+    simp only [AreDualInSelf, ne_eq, not_and] at h1j
     rw [h.2 h.1] at h1j
     apply h1j
     exact ne_of_apply_ne (Fin.cast h') hij
@@ -447,12 +448,12 @@ lemma getDualInOther?_get (h : GetDualCast l l2) (i : Fin l.length) :
   have h1 := Option.eq_some_of_isSome (getDualInOther?_self_isSome l2 (Fin.cast h.left i))
   erw [Fin.find_eq_some_iff] at h1
   apply And.intro
-  · simp [AreDualInOther]
+  · simp only [AreDualInOther]
     rw [idMap_eq_iff h]
     simp
   · intro j hj
     apply h1.2 (Fin.cast h.1 j)
-    simp [AreDualInOther]
+    simp only [AreDualInOther]
     exact (idMap_eq_iff h i j).mp hj
 
 lemma countId_cast (h : GetDualCast l l2) (i : Fin l.length) :
@@ -478,11 +479,12 @@ lemma idListFin_cast (h : GetDualCast l l2) :
   rw [h1]
   rw [List.filter_map]
   have h1 : Fin.cast h.1 ∘ Fin.cast h.1.symm = id := rfl
-  simp [h1]
+  simp only [List.map_map, h1, List.map_id]
   rw [idListFin_getDualInOther?]
   apply List.filter_congr
   intro i _
-  simp [getDualInOther?, Fin.find_eq_some_iff, AreDualInOther]
+  simp only [getDualInOther?, AreDualInOther, Fin.find_eq_some_iff, true_and, Function.comp_apply,
+    decide_eq_decide]
   refine Iff.intro (fun h' j hj => ?_) (fun h' j hj => ?_)
   · simpa using h' (Fin.cast h.1.symm j) (by rw [h.idMap_eq_iff]; exact hj)
   · simpa using h' (Fin.cast h.1 j) (by rw [h.symm.idMap_eq_iff]; exact hj)
@@ -518,7 +520,7 @@ lemma normalize_eq_map :
   have hl : l.val = List.map l.val.get (List.finRange l.length) := by
     simp [length]
   rw [hl]
-  simp [normalize]
+  simp only [normalize, List.map_map]
   exact List.ofFn_eq_map
 
 omit [DecidableEq X] in
@@ -548,13 +550,13 @@ lemma normalize_countId (i : Fin l.normalize.length) :
     l.normalize.countId l.normalize.val[Fin.val i] =
     l.countId (l.val.get ⟨i, by simpa using i.2⟩) := by
   rw [countId, countId]
-  simp [l.normalize_eq_map, Index.id]
+  simp only [Index.id, l.normalize_eq_map, List.getElem_map, List.countP_map, List.get_eq_getElem]
   apply List.countP_congr
   intro J hJ
   simp only [Function.comp_apply, decide_eq_true_eq]
   trans List.indexOf (l.val.get ⟨i, by simpa using i.2⟩).id l.idList = List.indexOf J.id l.idList
   · rfl
-  · simp
+  · simp only [List.get_eq_getElem]
     rw [idList_indexOf_mem]
     · rfl
     · exact List.getElem_mem l.val _ _
@@ -564,13 +566,13 @@ lemma normalize_countId (i : Fin l.normalize.length) :
 lemma normalize_countId' (i : Fin l.length) (hi : i.1 < l.normalize.length) :
     l.normalize.countId (l.normalize.val[Fin.val i]) = l.countId (l.val.get i) := by
   rw [countId, countId]
-  simp [l.normalize_eq_map, Index.id]
+  simp only [Index.id, l.normalize_eq_map, List.getElem_map, List.countP_map, List.get_eq_getElem]
   apply List.countP_congr
   intro J hJ
   simp only [Function.comp_apply, decide_eq_true_eq]
   trans List.indexOf (l.val.get i).id l.idList = List.indexOf J.id l.idList
   · rfl
-  · simp
+  · simp only [List.get_eq_getElem]
     rw [idList_indexOf_mem]
     · rfl
     · exact List.getElem_mem l.val _ _
@@ -689,7 +691,7 @@ lemma normalize_colorMap_eq_of_eq_colorMap (h : l.length = l2.length)
     (hc : l.colorMap = l2.colorMap ∘ Fin.cast h) :
     l.normalize.colorMap = l2.normalize.colorMap ∘
     Fin.cast (normalize_length_eq_of_eq_length l l2 h) := by
-  simp [hc]
+  simp only [normalize_colorMap, hc]
   rfl
 
 /-!