From 855dc5146d19399deee18da66abccd4214e2c786 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Sat, 19 Oct 2024 09:19:29 +0000
Subject: [PATCH] refactor: Simp to simp only ...

---
 HepLean/Mathematics/Fin.lean                  |  69 +++++-----
 .../SpaceTime/PauliMatrices/SelfAdjoint.lean  |   6 +-
 HepLean/Tensors/ComplexLorentz/Lemmas.lean    |   2 +-
 HepLean/Tensors/OverColor/Basic.lean          |   2 +-
 HepLean/Tensors/OverColor/Discrete.lean       |  18 ++-
 HepLean/Tensors/OverColor/Iso.lean            | 101 ++++++++------
 HepLean/Tensors/OverColor/Lift.lean           |  10 +-
 HepLean/Tensors/Tree/Basic.lean               | 125 +++++++++++-------
 HepLean/Tensors/Tree/Elab.lean                |  10 +-
 .../Tensors/Tree/NodeIdentities/Basic.lean    |   4 +-
 .../Tree/NodeIdentities/ContrContr.lean       |  62 +++++----
 .../Tree/NodeIdentities/PermContr.lean        |  40 +++---
 12 files changed, 257 insertions(+), 192 deletions(-)

diff --git a/HepLean/Mathematics/Fin.lean b/HepLean/Mathematics/Fin.lean
index e71e46d..9ad0e81 100644
--- a/HepLean/Mathematics/Fin.lean
+++ b/HepLean/Mathematics/Fin.lean
@@ -31,44 +31,44 @@ def predAboveI (i x : Fin n.succ.succ) : Fin n.succ :=
       · omega
       · omega⟩
 
-lemma predAboveI_self  (i : Fin n.succ.succ) : predAboveI i i = ⟨i.val - 1, by omega⟩ := by
+lemma predAboveI_self (i : Fin n.succ.succ) : predAboveI i i = ⟨i.val - 1, by omega⟩ := by
   simp [predAboveI]
 
 @[simp]
 lemma predAboveI_succAbove (i : Fin n.succ.succ) (x : Fin n.succ) :
     predAboveI i (Fin.succAbove i x) = x := by
-  simp [predAboveI, Fin.succAbove, Fin.ext_iff]
+  simp only [Nat.succ_eq_add_one, predAboveI, Fin.succAbove, Fin.val_fin_lt, Fin.ext_iff]
   split_ifs
   · rfl
   · rename_i h1 h2
-    simp [Fin.lt_def] at h1 h2
+    simp only [Fin.lt_def, Fin.coe_castSucc, not_lt, Nat.succ_eq_add_one, Fin.val_succ] at h1 h2
     omega
   · rfl
 lemma succsAbove_predAboveI {i x : Fin n.succ.succ} (h : i ≠ x) :
     Fin.succAbove i (predAboveI i x) = x := by
-  simp [Fin.succAbove, predAboveI, Fin.ext_iff]
+  simp only [Fin.succAbove, predAboveI, Nat.succ_eq_add_one, Fin.val_fin_lt, Fin.ext_iff]
   split_ifs
   · rfl
   · rename_i h1 h2
     rw [Fin.lt_def] at h1 h2
-    simp
-    simp at h2
+    simp only [Fin.succ_mk, Nat.succ_eq_add_one, add_right_eq_self, one_ne_zero]
+    simp only [Fin.castSucc_mk, Fin.eta, Fin.val_fin_lt, not_lt] at h2
     rw [Fin.le_def] at h2
     omega
   · rename_i h1 h2
-    simp at h1
+    simp only [not_lt] at h1
     rw [Fin.le_def] at h1
     rw [Fin.lt_def] at h2
-    simp at h2
+    simp only [Fin.castSucc_mk] at h2
     omega
   · rename_i h1 h2
-    simp
-    simp at h1
+    simp only [Fin.succ_mk, Nat.succ_eq_add_one]
+    simp only [not_lt] at h1
     rw [Fin.le_def] at h1
     omega
 
 lemma predAboveI_eq_iff {i x : Fin n.succ.succ} (h : i ≠ x) (y : Fin n.succ) :
-    y = predAboveI i x  ↔ i.succAbove y  = x := by
+    y = predAboveI i x ↔ i.succAbove y = x := by
   apply Iff.intro
   · intro h
     subst h
@@ -83,19 +83,19 @@ lemma predAboveI_lt {i x : Fin n.succ.succ} (h : x.val < i.val) :
 
 lemma predAboveI_ge {i x : Fin n.succ.succ} (h : i.val < x.val) :
     predAboveI i x = ⟨x.val - 1, by omega⟩ := by
-  simp [predAboveI, h]
+  simp only [Nat.succ_eq_add_one, predAboveI, Fin.val_fin_lt, dite_eq_else, Fin.mk.injEq]
   omega
 
 lemma succAbove_succAbove_predAboveI (i : Fin n.succ.succ) (j : Fin n.succ) (x : Fin n) :
     i.succAbove (j.succAbove x) =
     (i.succAbove j).succAbove ((predAboveI (i.succAbove j) i).succAbove x) := by
   by_cases h1 : j.castSucc < i
-  · have hx := Fin.succAbove_of_castSucc_lt _  _ h1
+  · have hx := Fin.succAbove_of_castSucc_lt _ _ h1
     rw [hx]
     rw [predAboveI_ge h1]
     by_cases hx1 : x.castSucc < j
-    · rw [Fin.succAbove_of_castSucc_lt _  _ hx1]
-      rw  [Fin.succAbove_of_castSucc_lt _ _]
+    · rw [Fin.succAbove_of_castSucc_lt _ _ hx1]
+      rw [Fin.succAbove_of_castSucc_lt _ _]
       · nth_rewrite 2 [Fin.succAbove_of_castSucc_lt _ _]
         · rw [Fin.succAbove_of_castSucc_lt _ _]
           exact hx1
@@ -103,7 +103,7 @@ lemma succAbove_succAbove_predAboveI (i : Fin n.succ.succ) (j : Fin n.succ) (x :
           simp_all
           omega
       · exact Nat.lt_trans hx1 h1
-    · simp at hx1
+    · simp only [not_lt] at hx1
       rw [Fin.le_def] at hx1
       rw [Fin.lt_def] at h1
       rw [Fin.succAbove_of_le_castSucc _ _ hx1]
@@ -116,7 +116,7 @@ lemma succAbove_succAbove_predAboveI (i : Fin n.succ.succ) (j : Fin n.succ) (x :
         · rw [Fin.lt_def] at hx2 ⊢
           simp_all
           omega
-      · simp at hx2
+      · simp only [Nat.succ_eq_add_one, not_lt] at hx2
         rw [Fin.succAbove_of_le_castSucc _ _ hx2]
         nth_rewrite 2 [Fin.succAbove_of_le_castSucc]
         · rw [Fin.succAbove_of_le_castSucc]
@@ -124,8 +124,8 @@ lemma succAbove_succAbove_predAboveI (i : Fin n.succ.succ) (j : Fin n.succ) (x :
           exact Nat.le_succ_of_le hx1
         · rw [Fin.le_def] at hx2 ⊢
           simp_all
-  · simp at h1
-    have hx := Fin.succAbove_of_le_castSucc _  _ h1
+  · simp only [Nat.succ_eq_add_one, not_lt] at h1
+    have hx := Fin.succAbove_of_le_castSucc _ _ h1
     rw [hx]
     rw [predAboveI_lt (Nat.lt_add_one_of_le h1)]
     by_cases hx1 : j ≤ x.castSucc
@@ -141,7 +141,7 @@ lemma succAbove_succAbove_predAboveI (i : Fin n.succ.succ) (j : Fin n.succ) (x :
       · rw [Fin.le_def] at hx1 h1 ⊢
         simp_all
         omega
-    · simp at hx1
+    · simp only [Nat.succ_eq_add_one, not_le] at hx1
       rw [Fin.lt_def] at hx1
       rw [Fin.le_def] at h1
       rw [Fin.succAbove_of_castSucc_lt _ _ hx1]
@@ -149,12 +149,12 @@ lemma succAbove_succAbove_predAboveI (i : Fin n.succ.succ) (j : Fin n.succ) (x :
       · rw [Fin.succAbove_of_castSucc_lt _ _ hx2]
         nth_rewrite 2 [Fin.succAbove_of_castSucc_lt _ _]
         · rw [Fin.succAbove_of_castSucc_lt _ _]
-          rw [Fin.lt_def] at  hx2 ⊢
+          rw [Fin.lt_def] at hx2 ⊢
           simp_all
           omega
-        · rw [Fin.lt_def] at hx2  ⊢
+        · rw [Fin.lt_def] at hx2 ⊢
           simp_all
-      · simp at hx2
+      · simp only [not_lt] at hx2
         rw [Fin.succAbove_of_le_castSucc _ _ hx2]
         nth_rewrite 2 [Fin.succAbove_of_le_castSucc]
         · rw [Fin.succAbove_of_castSucc_lt]
@@ -175,11 +175,12 @@ def finExtractOne {n : ℕ} (i : Fin n.succ) : Fin n.succ ≃ Fin 1 ⊕ Fin n :=
 
 lemma finExtractOne_apply_eq {n : ℕ} (i : Fin n.succ) :
     finExtractOne i i = Sum.inl 0 := by
-  simp [finExtractOne]
+  simp only [Nat.succ_eq_add_one, finExtractOne, Equiv.trans_apply, finCongr_apply,
+    Equiv.sumCongr_apply, Equiv.coe_trans, Equiv.sumComm_apply, Equiv.coe_refl, Fin.isValue]
   have h1 : Fin.cast (finExtractOne.proof_1 i) i = Fin.castAdd ((n - ↑i)) ⟨i.1, lt_add_one i.1⟩ := by
     simp [Fin.ext_iff]
   rw [h1, finSumFinEquiv_symm_apply_castAdd]
-  simp
+  simp only [Nat.succ_eq_add_one, Sum.map_inl, Function.comp_apply, Fin.isValue]
   have h2 : @Fin.mk (↑i + 1) ↑i (lt_add_one i.1) = Fin.natAdd i.val 1 := by
     simp [Fin.ext_iff]
   rw [h2, finSumFinEquiv_symm_apply_natAdd]
@@ -245,12 +246,13 @@ lemma finExtractOne_symm_inl_apply {n : ℕ} (i : Fin n.succ) :
   rfl
 
 def finExtractOnPermHom (i : Fin n.succ.succ) (σ : Fin n.succ.succ ≃ Fin n.succ.succ) :
-   Fin n.succ → Fin n.succ := fun x => predAboveI (σ i) (σ ((finExtractOne i).symm (Sum.inr x)))
+    Fin n.succ → Fin n.succ := fun x => predAboveI (σ i) (σ ((finExtractOne i).symm (Sum.inr x)))
 
 lemma finExtractOnPermHom_inv (i : Fin n.succ.succ) (σ : Fin n.succ.succ ≃ Fin n.succ.succ) :
-  (finExtractOnPermHom (σ i) σ.symm) ∘ (finExtractOnPermHom i σ)  = id := by
+  (finExtractOnPermHom (σ i) σ.symm) ∘ (finExtractOnPermHom i σ) = id := by
   funext x
-  simp [finExtractOnPermHom]
+  simp only [Nat.succ_eq_add_one, Function.comp_apply, finExtractOnPermHom, Equiv.symm_apply_apply,
+    finExtractOne_symm_inr_apply, id_eq]
   by_cases h : σ (i.succAbove x) < σ i
   · rw [predAboveI_lt h, Fin.succAbove_of_castSucc_lt]
     · simp
@@ -261,18 +263,18 @@ lemma finExtractOnPermHom_inv (i : Fin n.succ.succ) (σ : Fin n.succ.succ ≃ Fi
   have hn : σ i < σ (i.succAbove x) := by omega
   rw [predAboveI_ge hn]
   rw [Fin.succAbove_of_le_castSucc]
-  · simp
-    trans  predAboveI i (σ.symm (σ (i.succAbove x)))
+  · simp only [Nat.succ_eq_add_one, Fin.succ_mk]
+    trans predAboveI i (σ.symm (σ (i.succAbove x)))
     · congr
       exact Nat.sub_add_cancel (Fin.lt_of_le_of_lt (Fin.zero_le (σ i)) hn)
     simp
   rw [Fin.le_def]
-  simp
+  simp only [Nat.succ_eq_add_one, Fin.castSucc_mk]
   omega
 
 def finExtractOnePerm (i : Fin n.succ.succ) (σ : Fin n.succ.succ ≃ Fin n.succ.succ) :
     Fin n.succ ≃ Fin n.succ where
-  toFun x :=  finExtractOnPermHom i σ x
+  toFun x := finExtractOnPermHom i σ x
   invFun x := finExtractOnPermHom (σ i) σ.symm x
   left_inv x := by
     simpa using congrFun (finExtractOnPermHom_inv i σ) x
@@ -290,7 +292,8 @@ def finExtractTwo {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) :
 @[simp]
 lemma finExtractTwo_apply_fst {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) :
     finExtractTwo i j i = Sum.inl (Sum.inl 0) := by
-  simp [finExtractTwo]
+  simp only [Nat.succ_eq_add_one, finExtractTwo, Equiv.trans_apply, Equiv.sumCongr_apply,
+    Equiv.coe_refl, Fin.isValue]
   simp [finExtractOne_apply_eq]
 
 lemma finExtractTwo_symm_inr {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) :
diff --git a/HepLean/SpaceTime/PauliMatrices/SelfAdjoint.lean b/HepLean/SpaceTime/PauliMatrices/SelfAdjoint.lean
index 6aebd8a..9c63a8a 100644
--- a/HepLean/SpaceTime/PauliMatrices/SelfAdjoint.lean
+++ b/HepLean/SpaceTime/PauliMatrices/SelfAdjoint.lean
@@ -379,7 +379,11 @@ lemma σSAL_repr_inr_2 (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
   simp only [Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
     Finset.sum_singleton, Fin.sum_univ_three] at hM
   have h0 := congrArg (fun A => - Matrix.trace (σ3 * A.1)/ 2) hM
-  simp [σSAL, σSAL', mul_add] at h0
+  simp only [σSAL, Basis.mk_repr, Fin.isValue, Basis.coe_mk, σSAL', AddSubgroup.coe_add,
+    selfAdjoint.val_smul, smul_neg, mul_add, Algebra.mul_smul_comm, mul_neg, trace_add, trace_smul,
+    σ3_σ0_trace, smul_zero, trace_neg, σ3_σ1_trace, neg_zero, σ3_σ2_trace, add_zero, σ3_σ3_trace,
+    real_smul, zero_add, neg_neg, isUnit_iff_ne_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true,
+    IsUnit.mul_div_cancel_right] at h0
   linear_combination (norm := ring_nf) -h0
   simp [σSAL]
 
diff --git a/HepLean/Tensors/ComplexLorentz/Lemmas.lean b/HepLean/Tensors/ComplexLorentz/Lemmas.lean
index 752371e..ac8bdd0 100644
--- a/HepLean/Tensors/ComplexLorentz/Lemmas.lean
+++ b/HepLean/Tensors/ComplexLorentz/Lemmas.lean
@@ -73,7 +73,7 @@ lemma coMetric_prod_antiSymm (A : (Lorentz.complexContr ⊗ Lorentz.complexContr
     (hA : (twoNodeE complexLorentzTensor Color.up Color.up A).tensor =
       (TensorTree.neg (perm
       (OverColor.equivToHomEq (Equality.finMapToEquiv ![1, 0] ![1, 0]) (by decide))
-      (twoNodeE complexLorentzTensor  Color.up  Color.up A))).tensor)
+      (twoNodeE complexLorentzTensor Color.up Color.up A))).tensor)
     (hs : {S | μ ν = S | ν μ}ᵀ) : {A | μ ν ⊗ S | μ ν}ᵀ.tensor = 0 := by
   have h1 : {A | μ ν ⊗ S | μ ν}ᵀ.tensor = - {A | μ ν ⊗ S | μ ν}ᵀ.tensor := by
     nth_rewrite 1 [contr_tensor_eq (contr_tensor_eq (prod_tensor_eq_fst hA))]
diff --git a/HepLean/Tensors/OverColor/Basic.lean b/HepLean/Tensors/OverColor/Basic.lean
index 6b0ed47..5371b58 100644
--- a/HepLean/Tensors/OverColor/Basic.lean
+++ b/HepLean/Tensors/OverColor/Basic.lean
@@ -42,7 +42,7 @@ namespace Hom
 
 variable {C : Type} {f g h : OverColor C}
 
-lemma ext (m n : f ⟶ g) (h : m.hom  = n.hom) : m = n := by
+lemma ext (m n : f ⟶ g) (h : m.hom = n.hom) : m = n := by
   apply CategoryTheory.Iso.ext h
 
 /-- Given a hom in `OverColor C` the underlying equivalence between types. -/
diff --git a/HepLean/Tensors/OverColor/Discrete.lean b/HepLean/Tensors/OverColor/Discrete.lean
index 2ca3b97..853c220 100644
--- a/HepLean/Tensors/OverColor/Discrete.lean
+++ b/HepLean/Tensors/OverColor/Discrete.lean
@@ -70,7 +70,7 @@ def pairIsoSep {c1 c2 : C} : F.obj (Discrete.mk c1) ⊗ F.obj (Discrete.mk c2) 
 
 lemma pairIsoSep_tmul {c1 c2 : C} (x : F.obj (Discrete.mk c1)) (y : F.obj (Discrete.mk c2)) :
     (pairIsoSep F).hom.hom (x ⊗ₜ[k] y) =
-    PiTensorProduct.tprod k (Fin.cases x (Fin.cases y (fun i  => Fin.elim0 i))) := by
+    PiTensorProduct.tprod k (Fin.cases x (Fin.cases y (fun i => Fin.elim0 i))) := by
   simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Action.instMonoidalCategory_tensorObj_V,
     pairIsoSep, Fin.isValue, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons,
     forgetLiftApp, Iso.trans_symm, Iso.symm_symm_eq, Iso.trans_assoc, Iso.trans_hom, Iso.symm_hom,
@@ -88,7 +88,7 @@ lemma pairIsoSep_tmul {c1 c2 : C} (x : F.obj (Discrete.mk c1)) (y : F.obj (Discr
   rw [lift.obj_μ_tprod_tmul F (mk fun _ => c1) (mk fun _ => c2)]
   change ((lift.obj F).map fin2Iso.inv).hom
     (((lift.obj F).map ((mkIso _).hom ⊗ (mkIso _).hom)).hom
-      ((PiTensorProduct.tprod k) _))  = _
+      ((PiTensorProduct.tprod k) _)) = _
   rw [lift.map_tprod]
   change ((lift.obj F).map fin2Iso.inv).hom ((PiTensorProduct.tprod k) fun i => _) = _
   rw [lift.map_tprod]
@@ -96,10 +96,18 @@ lemma pairIsoSep_tmul {c1 c2 : C} (x : F.obj (Discrete.mk c1)) (y : F.obj (Discr
   funext i
   match i with
   | (0 : Fin 2) =>
-    simp [fin2Iso, HepLean.PiTensorProduct.elimPureTensor, mkIso, mkSum]
+    simp only [mk_hom, Fin.isValue, Matrix.cons_val_zero, Nat.succ_eq_add_one, Nat.reduceAdd,
+      Matrix.cons_val_one, Matrix.head_cons, instMonoidalCategoryStruct_tensorObj_left, fin2Iso,
+      Equiv.symm_symm, mkSum, mkIso, Iso.trans_inv, tensorIso_inv,
+      instMonoidalCategoryStruct_tensorObj_hom, Functor.id_obj,
+      HepLean.PiTensorProduct.elimPureTensor, Fin.cases_zero]
     exact (LinearEquiv.eq_symm_apply _).mp rfl
   | (1 : Fin 2) =>
-    simp [fin2Iso, HepLean.PiTensorProduct.elimPureTensor, mkIso, mkSum]
+    simp only [mk_hom, Fin.isValue, Matrix.cons_val_one, Matrix.head_cons, Nat.succ_eq_add_one,
+      Nat.reduceAdd, Matrix.cons_val_zero, instMonoidalCategoryStruct_tensorObj_left, fin2Iso,
+      Equiv.symm_symm, mkSum, mkIso, Iso.trans_inv, tensorIso_inv,
+      instMonoidalCategoryStruct_tensorObj_hom, Functor.id_obj,
+      HepLean.PiTensorProduct.elimPureTensor]
     exact (LinearEquiv.eq_symm_apply _).mp rfl
 
 /-- The functor taking `c` to `F c ⊗ F (τ c)`. -/
@@ -108,7 +116,7 @@ def pairτ (τ : C → C) : Discrete C ⥤ Rep k G :=
 
 lemma pairτ_tmul {c : C} (x : F.obj (Discrete.mk c)) (y : ↑(((Action.functorCategoryEquivalence (ModuleCat k) (MonCat.of G)).symm.inverse.obj
         ((Discrete.functor (Discrete.mk ∘ τ) ⋙ F).obj { as := c })).obj
-        PUnit.unit)) (h : c = c1):
+        PUnit.unit)) (h : c = c1) :
     ((pairτ F τ).map (Discrete.eqToHom h)).hom (x ⊗ₜ[k] y)=
     ((F.map (Discrete.eqToHom h)).hom x) ⊗ₜ[k] ((F.map (Discrete.eqToHom (by simp [h]))).hom y) := by
   rfl
diff --git a/HepLean/Tensors/OverColor/Iso.lean b/HepLean/Tensors/OverColor/Iso.lean
index b5cf6f5..e2021a2 100644
--- a/HepLean/Tensors/OverColor/Iso.lean
+++ b/HepLean/Tensors/OverColor/Iso.lean
@@ -74,19 +74,20 @@ def fin2Iso {c : Fin 2 → C} : mk c ≅ mk ![c 0] ⊗ mk ![c 1] := by
 
 def extractOne {n : ℕ} (i : Fin n.succ.succ)
     {c1 c2 : Fin n.succ.succ → C} (σ : mk c1 ⟶ mk c2) :
-    mk (c1  ∘ Fin.succAbove ((Hom.toEquiv σ).symm i)) ⟶ mk (c2 ∘ Fin.succAbove i) :=
+    mk (c1 ∘ Fin.succAbove ((Hom.toEquiv σ).symm i)) ⟶ mk (c2 ∘ Fin.succAbove i) :=
   equivToHomEq ((finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ))) (by
     intro x
     simp_all only [Nat.succ_eq_add_one, Function.comp_apply]
     have h1 := Hom.toEquiv_comp_inv_apply σ (i.succAbove x)
-    simp at h1
+    simp only [Nat.succ_eq_add_one, Functor.const_obj_obj, mk_hom] at h1
     rw [← h1]
     apply congrArg
-    simp [finExtractOnePerm, finExtractOnPermHom]
+    simp only [finExtractOnePerm, Nat.succ_eq_add_one, finExtractOnPermHom,
+      finExtractOne_symm_inr_apply, Equiv.symm_apply_apply, Equiv.coe_fn_symm_mk]
     erw [Equiv.apply_symm_apply]
     rw [succsAbove_predAboveI]
     · rfl
-    simp
+    simp only [Nat.succ_eq_add_one, ne_eq]
     erw [Equiv.apply_eq_iff_eq]
     exact (Fin.succAbove_ne i x).symm)
 
@@ -98,11 +99,11 @@ lemma extractOne_homToEquiv {n : ℕ} (i : Fin n.succ.succ)
 
 def extractTwo {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ)
     {c1 c2 : Fin n.succ.succ → C} (σ : mk c1 ⟶ mk c2) :
-    mk (c1  ∘ Fin.succAbove ((Hom.toEquiv σ).symm i) ∘
+    mk (c1 ∘ Fin.succAbove ((Hom.toEquiv σ).symm i) ∘
       Fin.succAbove (((Hom.toEquiv (extractOne i σ))).symm j)) ⟶
     mk (c2 ∘ Fin.succAbove i ∘ Fin.succAbove j) :=
   match n with
-  | 0 =>  equivToHomEq (Equiv.refl _) (by simp)
+  | 0 => equivToHomEq (Equiv.refl _) (by simp)
   | Nat.succ n =>
     equivToHomEq (Equiv.refl _) (by simp) ≫ extractOne j (extractOne i σ) ≫
     equivToHomEq (Equiv.refl _) (by simp)
@@ -119,27 +120,29 @@ def extractTwoAux' {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ)
   mk ((c1 ∘ ⇑(finExtractTwo i j).symm) ∘ Sum.inl) :=
   equivToHomEq (Equiv.refl _) (by
     intro x
-    simp
+    simp only [Nat.succ_eq_add_one, Function.comp_apply, extractOne_homToEquiv, Equiv.refl_symm,
+      Equiv.coe_refl, id_eq]
     match x with
     | Sum.inl 0=>
-      simp
+      simp only [Fin.isValue, finExtractTwo_symm_inl_inl_apply]
       have h1 := Hom.toEquiv_comp_inv_apply σ i
       simpa using h1.symm
     | Sum.inr 0 =>
-      simp
+      simp only [Fin.isValue, finExtractTwo_symm_inl_inr_apply]
       have h1 := Hom.toEquiv_comp_inv_apply σ (i.succAbove j)
-      simp at h1
+      simp only [Nat.succ_eq_add_one, Functor.const_obj_obj, mk_hom] at h1
       rw [← h1]
       congr
-      simp [finExtractOnePerm, finExtractOnPermHom]
+      simp only [Nat.succ_eq_add_one, finExtractOnePerm, finExtractOnPermHom,
+        finExtractOne_symm_inr_apply, Equiv.symm_apply_apply, Equiv.coe_fn_symm_mk]
       erw [Equiv.apply_symm_apply]
       rw [succsAbove_predAboveI]
       rfl
-      simp
+      simp only [Nat.succ_eq_add_one, ne_eq]
       erw [Equiv.apply_eq_iff_eq]
       exact (Fin.succAbove_ne i j).symm)
 
-lemma extractTwo_finExtractTwo_succ  {n : ℕ} (i : Fin n.succ.succ.succ) (j : Fin n.succ.succ)
+lemma extractTwo_finExtractTwo_succ {n : ℕ} (i : Fin n.succ.succ.succ) (j : Fin n.succ.succ)
     {c c1 : Fin n.succ.succ.succ → C} (σ : mk c ⟶ mk c1) :
     σ ≫ (equivToIso (HepLean.Fin.finExtractTwo i j)).hom ≫ (mkSum (c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom =
     (equivToIso (HepLean.Fin.finExtractTwo ((Hom.toEquiv σ).symm i) (((Hom.toEquiv (extractOne i σ))).symm j))).hom
@@ -147,76 +150,82 @@ lemma extractTwo_finExtractTwo_succ  {n : ℕ} (i : Fin n.succ.succ.succ) (j : F
     ≫ ((extractTwoAux' i j σ) ⊗ (extractTwoAux i j σ)) := by
   apply IndexNotation.OverColor.Hom.ext
   ext x
-  simp [CategoryStruct.comp,extractTwoAux', extractTwoAux, mkSum,equivToIso, Hom.toIso]
+  simp only [Nat.succ_eq_add_one, instMonoidalCategoryStruct_tensorObj_left, CategoryStruct.comp,
+    equivToIso, Hom.toIso, mkSum, Iso.trans_hom, Over.isoMk_hom_left, Equiv.toIso_hom,
+    Discrete.mk_as, instMonoidalCategoryStruct_tensorObj_right_as, CostructuredArrow.right_eq_id,
+    ULift.rec.constant, Function.comp_apply, extractOne_homToEquiv, extractTwoAux', extractTwoAux,
+    instMonoidalCategoryStruct_tensorHom_hom_left]
   change ((finExtractTwo i j) ((Hom.toEquiv σ) x)) = Sum.map id ((finExtractOnePerm ((finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j)
             (finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ))))
     (((finExtractTwo ((Hom.toEquiv σ).symm i)
     ((finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j)) x))
-  simp [extractTwo]
+  simp only [Nat.succ_eq_add_one]
   obtain ⟨k, hk⟩ := (finExtractTwo ((Hom.toEquiv σ).symm i)
       ((finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j)).symm.surjective x
   subst hk
-  simp
+  simp only [Nat.succ_eq_add_one, Equiv.apply_symm_apply]
   match k with
   | Sum.inl (Sum.inl 0) =>
     simp
   | Sum.inl (Sum.inr 0) =>
-    simp
-    have h1 : ((Hom.toEquiv σ)  (Fin.succAbove
+    simp only [Fin.isValue, finExtractTwo_symm_inl_inr_apply, Sum.map_inl, id_eq]
+    have h1 : ((Hom.toEquiv σ) (Fin.succAbove
         ((Hom.toEquiv σ).symm i)
         ((finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j))) =
         i.succAbove j := by
-      simp [finExtractOnePerm, finExtractOnPermHom]
+      simp only [Nat.succ_eq_add_one, finExtractOnePerm, finExtractOnPermHom,
+        finExtractOne_symm_inr_apply, Equiv.symm_apply_apply, Equiv.coe_fn_symm_mk]
       erw [Equiv.apply_symm_apply]
       rw [succsAbove_predAboveI]
       exact Equiv.apply_symm_apply (Hom.toEquiv σ) (i.succAbove j)
-      simp
+      simp only [Nat.succ_eq_add_one, ne_eq]
       erw [Equiv.apply_eq_iff_eq]
       exact (Fin.succAbove_ne i j).symm
     rw [h1]
-    erw [Equiv.apply_eq_iff_eq_symm_apply ]
+    erw [Equiv.apply_eq_iff_eq_symm_apply]
     simp
   | Sum.inr x =>
-    simp
-    erw [Equiv.apply_eq_iff_eq_symm_apply ]
-    simp
-    simp [finExtractOnePerm, finExtractOnPermHom]
+    simp only [finExtractTwo_symm_inr_apply, Sum.map_inr]
+    erw [Equiv.apply_eq_iff_eq_symm_apply]
+    simp only [finExtractTwo_symm_inr_apply]
+    simp only [finExtractOnePerm, Nat.succ_eq_add_one, finExtractOnPermHom,
+      finExtractOne_symm_inr_apply, Equiv.symm_apply_apply, Equiv.coe_fn_symm_mk, Equiv.coe_fn_mk]
     erw [Equiv.apply_symm_apply]
     have h1 : (predAboveI i ((Hom.toEquiv σ)
             (Fin.succAbove ((Hom.toEquiv σ).symm i)
-              (predAboveI ((Hom.toEquiv σ).symm i) ((Hom.toEquiv σ).symm (i.succAbove j)))))) = j  := by
+              (predAboveI ((Hom.toEquiv σ).symm i) ((Hom.toEquiv σ).symm (i.succAbove j)))))) = j := by
         rw [succsAbove_predAboveI]
         · erw [Equiv.apply_symm_apply]
           simp
-        · simp
+        · simp only [Nat.succ_eq_add_one, ne_eq]
           erw [Equiv.apply_eq_iff_eq]
           exact (Fin.succAbove_ne i j).symm
     erw [h1]
-    let y := (Hom.toEquiv σ)  (Fin.succAbove ((Hom.toEquiv σ).symm i)
+    let y := (Hom.toEquiv σ) (Fin.succAbove ((Hom.toEquiv σ).symm i)
       ((predAboveI ((Hom.toEquiv σ).symm i) ((Hom.toEquiv σ).symm (i.succAbove j))).succAbove x))
-    change y = i.succAbove  (j.succAbove  (predAboveI j (predAboveI i y)))
+    change y = i.succAbove (j.succAbove (predAboveI j (predAboveI i y)))
     have hy : i ≠ y := by
-      simp [y]
-      erw [← Equiv.symm_apply_eq ]
+      simp only [Nat.succ_eq_add_one, ne_eq, y]
+      erw [← Equiv.symm_apply_eq]
       exact (Fin.succAbove_ne _ _).symm
     rw [succsAbove_predAboveI, succsAbove_predAboveI]
     exact hy
-    simp
+    simp only [Nat.succ_eq_add_one, ne_eq]
     rw [predAboveI_eq_iff]
-    simp [y]
-    erw [← Equiv.symm_apply_eq ]
+    simp only [Nat.succ_eq_add_one, y]
+    erw [← Equiv.symm_apply_eq]
     have h0 : (Hom.toEquiv σ).symm (i.succAbove j) =
       Fin.succAbove ((Hom.toEquiv σ).symm i)
         (predAboveI ((Hom.toEquiv σ).symm i) ((Hom.toEquiv σ).symm (i.succAbove j))) := by
       rw [succsAbove_predAboveI]
-      simp
+      simp only [Nat.succ_eq_add_one, ne_eq]
       erw [Equiv.apply_eq_iff_eq]
       exact (Fin.succAbove_ne i j).symm
     by_contra hn
     have hn' := hn.symm.trans h0
     erw [Fin.succAbove_right_injective.eq_iff] at hn'
     exact Fin.succAbove_ne
-             (predAboveI ((Hom.toEquiv σ).symm i) ((Hom.toEquiv σ).symm (i.succAbove j))) x hn'
+      (predAboveI ((Hom.toEquiv σ).symm i) ((Hom.toEquiv σ).symm (i.succAbove j))) x hn'
     exact hy
 
 lemma extractTwo_finExtractTwo {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ)
@@ -229,14 +238,18 @@ lemma extractTwo_finExtractTwo {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ)
   | 0 =>
     apply IndexNotation.OverColor.Hom.ext
     ext x
-    simp [CategoryStruct.comp,extractTwoAux', extractTwoAux, mkSum,equivToIso, Hom.toIso]
+    simp only [Nat.succ_eq_add_one, Nat.reduceAdd, instMonoidalCategoryStruct_tensorObj_left,
+      CategoryStruct.comp, equivToIso, Hom.toIso, mkSum, Iso.trans_hom, Over.isoMk_hom_left,
+      Equiv.toIso_hom, Discrete.mk_as, instMonoidalCategoryStruct_tensorObj_right_as,
+      CostructuredArrow.right_eq_id, ULift.rec.constant, Function.comp_apply, extractOne_homToEquiv,
+      extractTwoAux', extractTwoAux, instMonoidalCategoryStruct_tensorHom_hom_left]
     change ((finExtractTwo i j) (σ.hom.left x)) = Sum.map (Equiv.refl _) (Equiv.refl _) _
-    simp
+    simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Equiv.coe_refl, Sum.map_id_id, id_eq]
     change (finExtractTwo i j) ((Hom.toEquiv σ) x) = ((finExtractTwo ((Hom.toEquiv σ).symm i)
       ((finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j)) x)
     obtain ⟨k, hk⟩ := (Hom.toEquiv σ).symm.surjective x
     subst hk
-    simp
+    simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Equiv.apply_symm_apply]
     have hk : k = i ∨ k = i.succAbove j := by
       match i, j, k with
       | (0 : Fin 2), (0 : Fin 1), (0 : Fin 2) => exact Or.intro_left (0 = Fin.succAbove 0 0) rfl
@@ -245,15 +258,17 @@ lemma extractTwo_finExtractTwo {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ)
       | (1 : Fin 2), (0 : Fin 1), (1 : Fin 2) => exact Or.intro_left (1 = Fin.succAbove 1 0) rfl
     rcases hk with hk | hk
     subst hk
-    simp
+    simp only [finExtractTwo_apply_fst, Fin.isValue]
     subst hk
-    simp
+    simp only [finExtractTwo_apply_snd, Fin.isValue]
     rw [← Equiv.symm_apply_eq]
-    simp [finExtractOnePerm, finExtractOnPermHom]
+    simp only [finExtractOnePerm, Nat.succ_eq_add_one, Nat.reduceAdd, finExtractOnPermHom,
+      finExtractOne_symm_inr_apply, Equiv.symm_apply_apply, Equiv.coe_fn_symm_mk, Fin.isValue,
+      finExtractTwo_symm_inl_inr_apply]
     erw [Equiv.apply_symm_apply]
     rw [succsAbove_predAboveI]
     rfl
-    simp
+    simp only [Nat.succ_eq_add_one, Nat.reduceAdd, ne_eq]
     erw [Equiv.apply_eq_iff_eq]
     exact (Fin.succAbove_ne i j).symm
   | Nat.succ n => exact extractTwo_finExtractTwo_succ i j σ
diff --git a/HepLean/Tensors/OverColor/Lift.lean b/HepLean/Tensors/OverColor/Lift.lean
index 0862eda..4d9e282 100644
--- a/HepLean/Tensors/OverColor/Lift.lean
+++ b/HepLean/Tensors/OverColor/Lift.lean
@@ -648,15 +648,15 @@ noncomputable def lift : (Discrete C ⥤ Rep k G) ⥤ MonoidalFunctor (OverColor
 
 namespace lift
 
-lemma map_tprod (F :  Discrete C ⥤ Rep k G) {X Y : OverColor C} (f : X ⟶ Y)
+lemma map_tprod (F : Discrete C ⥤ Rep k G) {X Y : OverColor C} (f : X ⟶ Y)
     (p : (i : X.left) → F.obj (Discrete.mk <| X.hom i)) :
     ((lift.obj F).map f).hom (PiTensorProduct.tprod k p) =
     PiTensorProduct.tprod k fun (i : Y.left) => discreteFunctorMapEqIso F
     (OverColor.Hom.toEquiv_comp_inv_apply f i) (p ((OverColor.Hom.toEquiv f).symm i)) := by
-  simp [lift, obj']
+  simp only [lift, obj', objObj'_V_carrier, Functor.id_obj]
   erw [objMap'_tprod]
 
-lemma obj_μ_tprod_tmul (F :  Discrete C ⥤ Rep k G) (X Y : OverColor C)
+lemma obj_μ_tprod_tmul (F : Discrete C ⥤ Rep k G) (X Y : OverColor C)
     (p : (i : X.left) → (F.obj (Discrete.mk <| X.hom i)))
     (q : (i : Y.left) → F.obj (Discrete.mk <| Y.hom i)) :
     ((lift.obj F).μ X Y).hom (PiTensorProduct.tprod k p ⊗ₜ[k] PiTensorProduct.tprod k q) =
@@ -664,7 +664,7 @@ lemma obj_μ_tprod_tmul (F :  Discrete C ⥤ Rep k G) (X Y : OverColor C)
     discreteSumEquiv F i (HepLean.PiTensorProduct.elimPureTensor p q i) := by
   exact μ_tmul_tprod F p q
 
-lemma μIso_inv_tprod (F :  Discrete C ⥤ Rep k G) (X Y : OverColor C)
+lemma μIso_inv_tprod (F : Discrete C ⥤ Rep k G) (X Y : OverColor C)
     (p : (i : (X ⊗ Y).left) → F.obj (Discrete.mk <| (X ⊗ Y).hom i)) :
     ((lift.obj F).μIso X Y).inv.hom (PiTensorProduct.tprod k p) =
     (PiTensorProduct.tprod k (fun i => p (Sum.inl i))) ⊗ₜ[k]
@@ -709,7 +709,7 @@ def forgetLiftAppV (c : C) : ((lift.obj F).obj (OverColor.mk (fun (_ : Fin 1) =>
 @[simp]
 lemma forgetLiftAppV_symm_apply (c : C) (x : (F.obj (Discrete.mk c)).V) :
     (forgetLiftAppV F c).symm x = PiTensorProduct.tprod k (fun _ => x) := by
-  simp [forgetLiftAppV]
+  simp only [forgetLiftAppV, Fin.isValue, Functor.id_obj]
   erw [PiTensorProduct.subsingletonEquiv_symm_apply]
 
 /-- The `forgetLiftAppV` function takes an object `c` of type `C` and returns a isomorphism
diff --git a/HepLean/Tensors/Tree/Basic.lean b/HepLean/Tensors/Tree/Basic.lean
index 4a36ae4..b8cdbc8 100644
--- a/HepLean/Tensors/Tree/Basic.lean
+++ b/HepLean/Tensors/Tree/Basic.lean
@@ -70,21 +70,22 @@ lemma perm_contr_cond {n : ℕ} {c : Fin n.succ.succ → S.C} {c1 : Fin n.succ.s
     c (Fin.succAbove ((Hom.toEquiv σ).symm i) ((Hom.toEquiv (extractOne i σ)).symm j)) =
     S.τ (c ((Hom.toEquiv σ).symm i)) := by
   have h1 := Hom.toEquiv_comp_apply σ
-  simp at h1
+  simp only [Nat.succ_eq_add_one, Functor.const_obj_obj, mk_hom] at h1
   rw [h1, h1]
-  simp
+  simp only [Nat.succ_eq_add_one, extractOne_homToEquiv, Equiv.apply_symm_apply]
   rw [← h]
   congr
-  simp [HepLean.Fin.finExtractOnePerm, HepLean.Fin.finExtractOnPermHom]
+  simp only [Nat.succ_eq_add_one, HepLean.Fin.finExtractOnePerm, HepLean.Fin.finExtractOnPermHom,
+    HepLean.Fin.finExtractOne_symm_inr_apply, Equiv.symm_apply_apply, Equiv.coe_fn_symm_mk]
   erw [Equiv.apply_symm_apply]
   rw [HepLean.Fin.succsAbove_predAboveI]
   erw [Equiv.apply_symm_apply]
-  simp
+  simp only [Nat.succ_eq_add_one, ne_eq]
   erw [Equiv.apply_eq_iff_eq]
   exact (Fin.succAbove_ne i j).symm
 
 /-- The isomorphism between the image of a map `Fin 1 ⊕ Fin 1 → S.C` contructed by `finExtractTwo`
- under `S.F.obj`, and an object in the image of `OverColor.Discrete.pairτ S.FDiscrete`. -/
+  under `S.F.obj`, and an object in the image of `OverColor.Discrete.pairτ S.FDiscrete`. -/
 def contrFin1Fin1 {n : ℕ} (c : Fin n.succ.succ → S.C)
     (i : Fin n.succ.succ) (j : Fin n.succ) (h : c (i.succAbove j) = S.τ (c i)) :
     S.F.obj (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)) ≅
@@ -115,35 +116,54 @@ lemma contrFin1Fin1_inv_tmul {n : ℕ} (c : Fin n.succ.succ → S.C)
     PiTensorProduct.tprod S.k (fun k =>
     match k with | Sum.inl 0 => x | Sum.inr 0 => (S.FDiscrete.map
     (eqToHom (by simp [h]))).hom y) := by
-  simp [contrFin1Fin1]
+  simp only [Nat.succ_eq_add_one, contrFin1Fin1, Functor.comp_obj, Discrete.functor_obj_eq_as,
+    Function.comp_apply, Iso.trans_symm, Iso.symm_symm_eq, Iso.trans_inv, tensorIso_inv,
+    Iso.symm_inv, Functor.mapIso_hom, tensor_comp, MonoidalFunctor.μIso_hom, Category.assoc,
+    LaxMonoidalFunctor.μ_natural, Functor.mapIso_inv, Action.comp_hom,
+    Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorHom_hom,
+    Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
+    Action.FunctorCategoryEquivalence.functor_obj_obj, ModuleCat.coe_comp, Functor.id_obj, mk_hom,
+    Fin.isValue]
   change (S.F.map (OverColor.mkSum ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)).inv).hom
     ((S.F.map ((OverColor.mkIso _).hom ⊗ (OverColor.mkIso _).hom)).hom
       ((S.F.μ (OverColor.mk fun x => c i) (OverColor.mk fun x => S.τ (c i))).hom
         ((((OverColor.forgetLiftApp S.FDiscrete (c i)).inv.hom x) ⊗ₜ[S.k]
         ((OverColor.forgetLiftApp S.FDiscrete (S.τ (c i))).inv.hom y))))) = _
-  simp [OverColor.forgetLiftApp]
+  simp only [Nat.succ_eq_add_one, Action.instMonoidalCategory_tensorObj_V, Equivalence.symm_inverse,
+    Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
+    forgetLiftApp, Action.mkIso_inv_hom, LinearEquiv.toModuleIso_inv, Fin.isValue]
   erw [OverColor.forgetLiftAppV_symm_apply, OverColor.forgetLiftAppV_symm_apply S.FDiscrete (S.τ (c i))]
-  change  ((OverColor.lift.obj S.FDiscrete).map (OverColor.mkSum ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)).inv).hom
+  change ((OverColor.lift.obj S.FDiscrete).map (OverColor.mkSum ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)).inv).hom
     (((OverColor.lift.obj S.FDiscrete).map ((OverColor.mkIso _).hom ⊗ (OverColor.mkIso _).hom)).hom
       (((OverColor.lift.obj S.FDiscrete).μ (OverColor.mk fun x => c i) (OverColor.mk fun x => S.τ (c i))).hom
         (((PiTensorProduct.tprod S.k) fun x_1 => x) ⊗ₜ[S.k] (PiTensorProduct.tprod S.k) fun x => y))) = _
   rw [OverColor.lift.obj_μ_tprod_tmul S.FDiscrete]
   change ((OverColor.lift.obj S.FDiscrete).map (OverColor.mkSum ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)).inv).hom
     (((OverColor.lift.obj S.FDiscrete).map ((OverColor.mkIso _).hom ⊗ (OverColor.mkIso _).hom)).hom
-      ((PiTensorProduct.tprod S.k) _))  = _
+      ((PiTensorProduct.tprod S.k) _)) = _
   rw [OverColor.lift.map_tprod S.FDiscrete]
-  change  ((OverColor.lift.obj S.FDiscrete).map (OverColor.mkSum ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)).inv).hom
+  change ((OverColor.lift.obj S.FDiscrete).map (OverColor.mkSum ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)).inv).hom
     ((PiTensorProduct.tprod S.k _)) = _
   rw [OverColor.lift.map_tprod S.FDiscrete]
   apply congrArg
   funext r
   match r with
   | Sum.inl 0 =>
-    simp [OverColor.lift.discreteSumEquiv, HepLean.PiTensorProduct.elimPureTensor]
-    simp [OverColor.lift.discreteFunctorMapEqIso]
+    simp only [Nat.succ_eq_add_one, mk_hom, Fin.isValue, Function.comp_apply,
+      instMonoidalCategoryStruct_tensorObj_left, mkSum_inv_homToEquiv, Equiv.refl_symm,
+      instMonoidalCategoryStruct_tensorObj_hom, Functor.id_obj, lift.discreteSumEquiv, Sum.elim_inl,
+      Sum.elim_inr, HepLean.PiTensorProduct.elimPureTensor]
+    simp only [Fin.isValue, lift.discreteFunctorMapEqIso, eqToIso_refl, Functor.mapIso_refl,
+      Iso.refl_hom, Action.id_hom, Iso.refl_inv, LinearEquiv.ofLinear_apply]
     rfl
   | Sum.inr 0 =>
-    simp [OverColor.lift.discreteFunctorMapEqIso, OverColor.lift.discreteSumEquiv, HepLean.PiTensorProduct.elimPureTensor]
+    simp only [Nat.succ_eq_add_one, mk_hom, Fin.isValue, Function.comp_apply,
+      instMonoidalCategoryStruct_tensorObj_left, mkSum_inv_homToEquiv, Equiv.refl_symm,
+      instMonoidalCategoryStruct_tensorObj_hom, lift.discreteFunctorMapEqIso, eqToIso_refl,
+      Functor.mapIso_refl, Iso.refl_hom, Action.id_hom, Iso.refl_inv, Functor.mapIso_hom,
+      eqToIso.hom, Functor.mapIso_inv, eqToIso.inv, Functor.id_obj, lift.discreteSumEquiv,
+      Sum.elim_inl, Sum.elim_inr, HepLean.PiTensorProduct.elimPureTensor,
+      LinearEquiv.ofLinear_apply]
     rfl
 
 lemma contrFin1Fin1_hom_hom_tprod {n : ℕ} (c : Fin n.succ.succ → S.C)
@@ -163,7 +183,8 @@ lemma contrFin1Fin1_hom_hom_tprod {n : ℕ} (c : Fin n.succ.succ → S.C)
   | Sum.inl 0 =>
     simp
   | Sum.inr 0 =>
-    simp
+    simp only [Nat.succ_eq_add_one, Fin.isValue, mk_hom, Function.comp_apply,
+      Discrete.functor_obj_eq_as]
     change _ = ((S.FDiscrete.map (eqToHom _)) ≫ (S.FDiscrete.map (eqToHom _))).hom (x (Sum.inr 0))
     rw [← Functor.map_comp]
     simp
@@ -182,17 +203,16 @@ def contrIso {n : ℕ} (c : Fin n.succ.succ → S.C)
   refine tensorIso (S.contrFin1Fin1 c i j h) (S.F.mapIso (OverColor.mkIso (by ext x; simp)))
 
 lemma contrIso_hom_hom {n : ℕ} {c1 : Fin n.succ.succ → S.C}
-    {i : Fin n.succ.succ} {j : Fin n.succ}
-    {h : c1 (i.succAbove j) = S.τ (c1 i)} :
- (S.contrIso c1 i j h).hom.hom =
-  (S.F.map (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).hom ≫
-      (S.F.map (mkSum (c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).hom ≫
-        (S.F.μIso (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl))
-                (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv.hom ≫
-          ((S.contrFin1Fin1 c1 i j h).hom.hom ⊗ (S.F.map (mkIso (contrIso.proof_1 S c1 i j)).hom).hom)
-   := by
+    {i : Fin n.succ.succ} {j : Fin n.succ} {h : c1 (i.succAbove j) = S.τ (c1 i)} :
+    (S.contrIso c1 i j h).hom.hom =
+    (S.F.map (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).hom ≫
+    (S.F.map (mkSum (c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).hom ≫
+    (S.F.μIso (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl))
+    (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv.hom ≫
+    ((S.contrFin1Fin1 c1 i j h).hom.hom ⊗
+    (S.F.map (mkIso (contrIso.proof_1 S c1 i j)).hom).hom) := by
   rw [contrIso]
-  simp  [Nat.succ_eq_add_one, Action.instMonoidalCategory_tensorObj_V, Action.comp_hom,
+  simp [Nat.succ_eq_add_one, Action.instMonoidalCategory_tensorObj_V, Action.comp_hom,
     extractOne_homToEquiv, Action.instMonoidalCategory_tensorHom_hom]
 
 /-- `contrMap` is a function that takes a natural number `n`, a function `c` from
@@ -208,14 +228,14 @@ def contrMap {n : ℕ} (c : Fin n.succ.succ → S.C)
   (tensorHom (S.contr.app (Discrete.mk (c i))) (𝟙 _)) ≫
   (MonoidalCategory.leftUnitor _).hom
 
-def castToField (v : (↑((𝟙_ (Discrete S.C ⥤ Rep S.k S.G)).obj { as := c  }).V)) : S.k := v
+def castToField (v : (↑((𝟙_ (Discrete S.C ⥤ Rep S.k S.G)).obj { as := c }).V)) : S.k := v
 
 lemma contrMap_tprod {n : ℕ} (c : Fin n.succ.succ → S.C)
     (i : Fin n.succ.succ) (j : Fin n.succ) (h : c (i.succAbove j) = S.τ (c i))
     (x : (i : Fin n.succ.succ) → S.FDiscrete.obj (Discrete.mk (c i))) :
-    (S.contrMap c i j h).hom  (PiTensorProduct.tprod S.k x) =
+    (S.contrMap c i j h).hom (PiTensorProduct.tprod S.k x) =
     (S.castToField ((S.contr.app (Discrete.mk (c i))).hom ((x i) ⊗ₜ[S.k]
-    (S.FDiscrete.map (Discrete.eqToHom h)).hom (x (i.succAbove j)))): S.k)
+    (S.FDiscrete.map (Discrete.eqToHom h)).hom (x (i.succAbove j)))) : S.k)
     • (PiTensorProduct.tprod S.k (fun k => x (i.succAbove (j.succAbove k))) : S.F.obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove))) := by
   rw [contrMap, contrIso]
   simp only [Nat.succ_eq_add_one, S.F_def, Iso.trans_hom, Functor.mapIso_hom, Iso.symm_hom,
@@ -261,18 +281,15 @@ lemma contrMap_tprod {n : ℕ} (c : Fin n.succ.succ → S.C)
         ((TensorProduct.map (S.contrFin1Fin1 c i j h).hom.hom ((lift.obj S.FDiscrete).map (mkIso ⋯).hom).hom)
           (((PiTensorProduct.tprod S.k) fun i_1 =>
               (lift.discreteFunctorMapEqIso S.FDiscrete ⋯)
-                ((lift.discreteFunctorMapEqIso S.FDiscrete ⋯)
-                  (x
+                ((lift.discreteFunctorMapEqIso S.FDiscrete ⋯) (x
                     ((Hom.toEquiv (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).symm
                       ((Hom.toEquiv (mkSum (c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).symm
                         (Sum.inl i_1)))))) ⊗ₜ[S.k]
             (PiTensorProduct.tprod S.k) fun i_1 =>
-              (lift.discreteFunctorMapEqIso S.FDiscrete ⋯)
-                ((lift.discreteFunctorMapEqIso S.FDiscrete ⋯)
-                  (x
-                    ((Hom.toEquiv (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).symm
-                      ((Hom.toEquiv (mkSum (c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).symm (Sum.inr i_1)))))))) =
-   _
+    (lift.discreteFunctorMapEqIso S.FDiscrete ⋯) ((lift.discreteFunctorMapEqIso S.FDiscrete ⋯)
+    (x ((Hom.toEquiv (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).symm
+    ((Hom.toEquiv
+    (mkSum (c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).symm (Sum.inr i_1)))))))) = _
   rw [TensorProduct.map_tmul]
   rw [contrFin1Fin1_hom_hom_tprod]
   simp only [Nat.succ_eq_add_one, Action.instMonoidalCategory_tensorObj_V,
@@ -280,33 +297,37 @@ lemma contrMap_tprod {n : ℕ} (c : Fin n.succ.succ → S.C)
     Discrete.functor_obj_eq_as, instMonoidalCategoryStruct_tensorObj_left, mkSum_homToEquiv,
     Equiv.refl_symm, Functor.id_obj, ModuleCat.MonoidalCategory.whiskerRight_apply]
   rw [Action.instMonoidalCategory_leftUnitor_hom_hom]
-  simp
+  simp only [Monoidal.tensorUnit_obj, Action.instMonoidalCategory_tensorUnit_V, Fin.isValue,
+    ModuleCat.MonoidalCategory.leftUnitor_hom_apply]
   congr 1
   /- The contraction. -/
-  · simp [castToField]
+  · simp only [Fin.isValue, castToField]
     congr 2
-    · simp [lift.discreteFunctorMapEqIso]
+    · simp only [Fin.isValue, lift.discreteFunctorMapEqIso, eqToIso_refl, Functor.mapIso_refl,
+      Iso.refl_hom, Action.id_hom, Iso.refl_inv, LinearEquiv.ofLinear_apply]
       rfl
     · simp [lift.discreteFunctorMapEqIso, h]
       change (S.FDiscrete.map (eqToHom _)).hom
         (x (((HepLean.Fin.finExtractTwo i j)).symm ((Sum.inl (Sum.inr 0))))) = _
-      simp [CategoryTheory.Discrete.functor_map_id]
+      simp only [Nat.succ_eq_add_one, Fin.isValue]
       have h1' {a b d: Fin n.succ.succ} (hbd : b =d) (h : c d = S.τ (c a)) (h' : c b = S.τ (c a)) :
-        (S.FDiscrete.map (Discrete.eqToHom (h))).hom (x d) =
-         (S.FDiscrete.map (Discrete.eqToHom h')).hom (x b) := by
+          (S.FDiscrete.map (Discrete.eqToHom (h))).hom (x d) =
+          (S.FDiscrete.map (Discrete.eqToHom h')).hom (x b) := by
         subst hbd
         rfl
       refine h1' ?_ ?_ ?_
-      simp
+      simp only [Nat.succ_eq_add_one, Fin.isValue, HepLean.Fin.finExtractTwo_symm_inl_inr_apply]
       simp [h]
   /- The tensor. -/
   · erw [lift.map_tprod]
     apply congrArg
     funext d
-    simp [lift.discreteFunctorMapEqIso]
+    simp only [mk_hom, Function.comp_apply, lift.discreteFunctorMapEqIso, Functor.mapIso_hom,
+      eqToIso.hom, Functor.mapIso_inv, eqToIso.inv, eqToIso_refl, Functor.mapIso_refl, Iso.refl_hom,
+      Action.id_hom, Iso.refl_inv, LinearEquiv.ofLinear_apply]
     change (S.FDiscrete.map (eqToHom _)).hom
-        ((x ((HepLean.Fin.finExtractTwo i j).symm (Sum.inr (d))))) =  _
-    simp [CategoryTheory.Discrete.functor_map_id ]
+        ((x ((HepLean.Fin.finExtractTwo i j).symm (Sum.inr (d))))) = _
+    simp only [Nat.succ_eq_add_one]
     have h1 : ((HepLean.Fin.finExtractTwo i j).symm (Sum.inr d)) = (i.succAbove (j.succAbove d)) := by
       exact HepLean.Fin.finExtractTwo_symm_inr_apply i j d
     have h1' {a b : Fin n.succ.succ} (h : a = b) :
@@ -437,14 +458,14 @@ lemma constTwoNode_tensor {c1 c2 : S.C}
 
 lemma prod_tensor {c1 : Fin n → S.C} {c2 : Fin m → S.C} (t1 : TensorTree S c1) (t2 : TensorTree S c2) :
     (prod t1 t2).tensor = (S.F.map (OverColor.equivToIso finSumFinEquiv).hom).hom
-    ((S.F.μ _ _).hom (t1.tensor ⊗ₜ t2.tensor))  := rfl
+    ((S.F.μ _ _).hom (t1.tensor ⊗ₜ t2.tensor)) := rfl
 
 lemma add_tensor (t1 t2 : TensorTree S c) : (add t1 t2).tensor = t1.tensor + t2.tensor := rfl
 
 lemma perm_tensor (σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) (t : TensorTree S c) :
     (perm σ t).tensor = (S.F.map σ).hom t.tensor := rfl
 
-lemma contr_tensor {n : ℕ} {c : Fin n.succ.succ → S.C}  {i : Fin n.succ.succ} {j : Fin n.succ} {h : c (i.succAbove j) = S.τ (c i)}
+lemma contr_tensor {n : ℕ} {c : Fin n.succ.succ → S.C} {i : Fin n.succ.succ} {j : Fin n.succ} {h : c (i.succAbove j) = S.τ (c i)}
     (t : TensorTree S c) : (contr i j h t).tensor = (S.contrMap c i j h).hom t.tensor := rfl
 
 lemma neg_tensor (t : TensorTree S c) : (neg t).tensor = - t.tensor := rfl
@@ -462,17 +483,21 @@ lemma contr_tensor_eq {n : ℕ} {c : Fin n.succ.succ → S.C} {T1 T2 : TensorTre
   rw [h]
 
 lemma prod_tensor_eq_fst {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
-    {T1  T1' : TensorTree S c} { T2 : TensorTree S c1}
+    {T1 T1' : TensorTree S c} { T2 : TensorTree S c1}
     (h : T1.tensor = T1'.tensor) :
     (prod T1 T2).tensor = (prod T1' T2).tensor := by
-  simp [prod_tensor]
+  simp only [prod_tensor, Functor.id_obj, OverColor.mk_hom, Action.instMonoidalCategory_tensorObj_V,
+    Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
+    Action.FunctorCategoryEquivalence.functor_obj_obj]
   rw [h]
 
 lemma prod_tensor_eq_snd {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
     {T1 : TensorTree S c} {T2 T2' : TensorTree S c1}
     (h : T2.tensor = T2'.tensor) :
     (prod T1 T2).tensor = (prod T1 T2').tensor := by
-  simp [prod_tensor]
+  simp only [prod_tensor, Functor.id_obj, OverColor.mk_hom, Action.instMonoidalCategory_tensorObj_V,
+    Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
+    Action.FunctorCategoryEquivalence.functor_obj_obj]
   rw [h]
 
 end
diff --git a/HepLean/Tensors/Tree/Elab.lean b/HepLean/Tensors/Tree/Elab.lean
index 037c1ff..61fa85b 100644
--- a/HepLean/Tensors/Tree/Elab.lean
+++ b/HepLean/Tensors/Tree/Elab.lean
@@ -266,13 +266,13 @@ def withoutContr (stx : Syntax) : TermElabM (List (TSyntax `indexExpr)) := do
 def toPairs (l : List ℕ) : List (ℕ × ℕ) :=
   match l with
   | x1 :: x2 :: xs => (x1, x2) :: toPairs xs
-  | []             => []
-  | [x]     => [(x, 0)]
+  | [] => []
+  | [x] => [(x, 0)]
 
 def contrListAdjust (l : List (ℕ × ℕ)) : List (ℕ × ℕ) :=
   let l' := l.bind (fun p => [p.1, p.2])
   let l'' := List.mapAccumr
-    (fun  x  (prev : List ℕ) =>
+    (fun x (prev : List ℕ) =>
       let e := prev.countP (fun y => y < x)
       (x :: prev, x - e)) l'.reverse []
   toPairs l''.2.reverse
@@ -419,8 +419,8 @@ def finMapToEquiv (f1 f2 : Fin n → Fin n) (h : ∀ x, f1 (f2 x) = x := by deci
 def getPermutationSyntax (l1 l2 : List (TSyntax `indexExpr)) : TermElabM Term := do
   let lPerm ← getPermutation l1 l2
   let l2Perm ← getPermutation l1 l2
-  let permString := "![" ++ String.intercalate  ", " (lPerm.map toString) ++ "]"
-  let perm2String := "![" ++ String.intercalate  ", " (l2Perm.map toString) ++ "]"
+  let permString := "![" ++ String.intercalate ", " (lPerm.map toString) ++ "]"
+  let perm2String := "![" ++ String.intercalate ", " (l2Perm.map toString) ++ "]"
   let P1 ← TensorNode.stringToTerm permString
   let P2 ← TensorNode.stringToTerm perm2String
   let stx := Syntax.mkApp (mkIdent ``finMapToEquiv) #[P1, P2]
diff --git a/HepLean/Tensors/Tree/NodeIdentities/Basic.lean b/HepLean/Tensors/Tree/NodeIdentities/Basic.lean
index 1ee40cb..099c1d2 100644
--- a/HepLean/Tensors/Tree/NodeIdentities/Basic.lean
+++ b/HepLean/Tensors/Tree/NodeIdentities/Basic.lean
@@ -53,7 +53,7 @@ lemma neg_neg (t : TensorTree S c) : (neg (neg t)).tensor = t.tensor := by
   simp only [neg_tensor, _root_.neg_neg]
 
 @[simp]
-lemma neg_fst_prod  {c1 : Fin n → S.C} {c2 : Fin m → S.C} (T1 : TensorTree S c1)
+lemma neg_fst_prod {c1 : Fin n → S.C} {c2 : Fin m → S.C} (T1 : TensorTree S c1)
     (T2 : TensorTree S c2) :
     (prod (neg T1) T2).tensor = (neg (prod T1 T2)).tensor := by
   simp only [prod_tensor, Functor.id_obj, Action.instMonoidalCategory_tensorObj_V,
@@ -61,7 +61,7 @@ lemma neg_fst_prod  {c1 : Fin n → S.C} {c2 : Fin m → S.C} (T1 : TensorTree S
     Action.FunctorCategoryEquivalence.functor_obj_obj, neg_tensor, neg_tmul, map_neg]
 
 @[simp]
-lemma neg_snd_prod  {c1 : Fin n → S.C} {c2 : Fin m → S.C} (T1 : TensorTree S c1)
+lemma neg_snd_prod {c1 : Fin n → S.C} {c2 : Fin m → S.C} (T1 : TensorTree S c1)
     (T2 : TensorTree S c2) :
     (prod T1 (neg T2)).tensor = (neg (prod T1 T2)).tensor := by
   simp only [prod_tensor, Functor.id_obj, Action.instMonoidalCategory_tensorObj_V,
diff --git a/HepLean/Tensors/Tree/NodeIdentities/ContrContr.lean b/HepLean/Tensors/Tree/NodeIdentities/ContrContr.lean
index e57ef35..c03cd6e 100644
--- a/HepLean/Tensors/Tree/NodeIdentities/ContrContr.lean
+++ b/HepLean/Tensors/Tree/NodeIdentities/ContrContr.lean
@@ -38,12 +38,12 @@ def swapI : Fin n.succ.succ.succ.succ := q.i.succAbove (q.j.succAbove q.k)
 def swapJ : Fin n.succ.succ.succ := (predAboveI (q.i.succAbove (q.j.succAbove q.k)) q.i).succAbove
   ((predAboveI (q.j.succAbove q.k) q.j).succAbove q.l)
 
-def swapK :  Fin n.succ.succ :=  predAboveI
+def swapK : Fin n.succ.succ := predAboveI
     ((predAboveI (q.i.succAbove (q.j.succAbove q.k)) q.i).succAbove
       ((predAboveI (q.j.succAbove q.k) q.j).succAbove q.l))
     (predAboveI (q.i.succAbove (q.j.succAbove q.k)) q.i)
 
-def swapL :  Fin n.succ :=  predAboveI ((predAboveI (q.j.succAbove q.k) q.j).succAbove q.l)
+def swapL : Fin n.succ := predAboveI ((predAboveI (q.j.succAbove q.k) q.j).succAbove q.l)
   (predAboveI (q.j.succAbove q.k) q.j)
 
 lemma swap_map_eq (x : Fin n) : (q.swapI.succAbove (q.swapJ.succAbove
@@ -58,25 +58,25 @@ lemma swap_map_eq (x : Fin n) : (q.swapI.succAbove (q.swapJ.succAbove
 
 @[simp]
 lemma swapI_neq_i : ¬ q.swapI = q.i := by
-  simp [swapI]
+  simp only [Nat.succ_eq_add_one, swapI]
   exact Fin.succAbove_ne q.i (q.j.succAbove q.k)
 
 @[simp]
 lemma swapI_neq_succAbove : ¬ q.swapI = q.i.succAbove q.j := by
-  simp [swapI]
+  simp only [Nat.succ_eq_add_one, swapI]
   apply Function.Injective.ne Fin.succAbove_right_injective
   exact Fin.succAbove_ne q.j q.k
 
 @[simp]
 lemma swapI_neq_i_j_k_l_succAbove : ¬ q.swapI = q.i.succAbove (q.j.succAbove (q.k.succAbove q.l)) := by
-  simp [swapI]
+  simp only [Nat.succ_eq_add_one, swapI]
   apply Function.Injective.ne Fin.succAbove_right_injective
   apply Function.Injective.ne Fin.succAbove_right_injective
   exact Fin.ne_succAbove q.k q.l
 
 lemma swapJ_swapI_succAbove : q.swapI.succAbove q.swapJ = q.i.succAbove
     (q.j.succAbove (q.k.succAbove q.l)) := by
-  simp [swapI, swapJ]
+  simp only [swapI, swapJ]
   rw [← succAbove_succAbove_predAboveI]
   rw [← succAbove_succAbove_predAboveI]
 
@@ -87,7 +87,7 @@ lemma swapJ_eq_swapI_predAbove : q.swapJ = predAboveI q.swapI (q.i.succAbove
   exact swapI_neq_i_j_k_l_succAbove q
 
 @[simp]
-lemma swapK_swapJ_succAbove :  (q.swapJ.succAbove q.swapK) = predAboveI q.swapI q.i := by
+lemma swapK_swapJ_succAbove : (q.swapJ.succAbove q.swapK) = predAboveI q.swapI q.i := by
   rw [swapJ, swapK]
   rw [succsAbove_predAboveI]
   rfl
@@ -130,19 +130,19 @@ def contrMapFst := S.contrMap c q.i q.j q.hij
 def contrMapSnd := S.contrMap (c ∘ q.i.succAbove ∘ q.j.succAbove) q.k q.l q.hkl
 
 def contrSwapHom : (OverColor.mk ((c ∘ q.swap.i.succAbove ∘ q.swap.j.succAbove) ∘ q.swap.k.succAbove ∘ q.swap.l.succAbove)) ⟶
-  (OverColor.mk fun x => c (q.i.succAbove (q.j.succAbove (q.k.succAbove (q.l.succAbove x))))):=
+  (OverColor.mk fun x => c (q.i.succAbove (q.j.succAbove (q.k.succAbove (q.l.succAbove x))))) :=
   (mkIso (funext fun x => congrArg c (swap_map_eq q x))).hom
 
 lemma contrSwapHom_contrMapSnd_tprod (x : (i : (𝟭 Type).obj (OverColor.mk c).left) → CoeSort.coe (S.FDiscrete.obj { as := (OverColor.mk c).hom i })) :
     ((lift.obj S.FDiscrete).map q.contrSwapHom).hom
     (q.swap.contrMapSnd.hom ((PiTensorProduct.tprod S.k) fun k => x (q.swap.i.succAbove (q.swap.j.succAbove k))))
-    =  ((S.castToField
-          ((S.contr.app { as := (c ∘ q.swap.i.succAbove ∘ q.swap.j.succAbove) q.swap.k }).hom
-            (x (q.swap.i.succAbove (q.swap.j.succAbove q.swap.k)) ⊗ₜ[S.k]
-              (S.FDiscrete.map (Discrete.eqToHom q.swap.hkl)).hom
-                (x (q.swap.i.succAbove (q.swap.j.succAbove (q.swap.k.succAbove q.swap.l))))))) •
-       ((lift.obj S.FDiscrete).map q.contrSwapHom).hom ((PiTensorProduct.tprod S.k) fun k =>
-          x (q.swap.i.succAbove (q.swap.j.succAbove (q.swap.k.succAbove (q.swap.l.succAbove k)))))) := by
+    = ((S.castToField
+    ((S.contr.app { as := (c ∘ q.swap.i.succAbove ∘ q.swap.j.succAbove) q.swap.k }).hom
+    (x (q.swap.i.succAbove (q.swap.j.succAbove q.swap.k)) ⊗ₜ[S.k]
+    (S.FDiscrete.map (Discrete.eqToHom q.swap.hkl)).hom
+    (x (q.swap.i.succAbove (q.swap.j.succAbove (q.swap.k.succAbove q.swap.l))))))) •
+    ((lift.obj S.FDiscrete).map q.contrSwapHom).hom ((PiTensorProduct.tprod S.k) fun k =>
+    x (q.swap.i.succAbove (q.swap.j.succAbove (q.swap.k.succAbove (q.swap.l.succAbove k)))))) := by
   rw [contrMapSnd,TensorStruct.contrMap_tprod]
   change ((lift.obj S.FDiscrete).map q.contrSwapHom).hom
     (_ • ((PiTensorProduct.tprod S.k) fun k =>
@@ -161,11 +161,11 @@ lemma contrSwapHom_tprod (x : (i : (𝟭 Type).obj (OverColor.mk c).left) → Co
   rw [lift.map_tprod]
   apply congrArg
   funext i
-  simp
+  simp only [Nat.succ_eq_add_one, mk_hom, Function.comp_apply]
   rw [lift.discreteFunctorMapEqIso]
-  change _ =  (S.FDiscrete.map (Discrete.eqToIso _).hom).hom _
+  change _ = (S.FDiscrete.map (Discrete.eqToIso _).hom).hom _
   have h1' {a b : Fin n.succ.succ.succ.succ} (h : a = b) :
-      x b =  (S.FDiscrete.map  (Discrete.eqToIso (by rw [h])).hom).hom (x a) := by
+      x b = (S.FDiscrete.map (Discrete.eqToIso (by rw [h])).hom).hom (x a) := by
       subst h
       simp
   exact h1' (q.swap_map_eq i)
@@ -179,7 +179,7 @@ lemma contrMapFst_contrMapSnd_swap :
   refine PiTensorProduct.induction_on' x (fun r x => ?_) <| fun x y hx hy => by
       simp only [CategoryTheory.Functor.id_obj, map_add, hx, ModuleCat.coe_comp,
         Function.comp_apply, hy]
-  simp only [Nat.succ_eq_add_one, Functor.id_obj,  PiTensorProduct.tprodCoeff_eq_smul_tprod,
+  simp only [Nat.succ_eq_add_one, Functor.id_obj, PiTensorProduct.tprodCoeff_eq_smul_tprod,
     map_smul]
   apply congrArg
   rw [contrMapFst, contrMapFst]
@@ -205,21 +205,25 @@ lemma contrMapFst_contrMapSnd_swap :
     congr 1
     · congr 3
       have h1' {a b d: Fin n.succ.succ.succ.succ} (hbd : b =d) (h : c d = S.τ (c a)) (h' : c b = S.τ (c a)) :
-        (S.FDiscrete.map (Discrete.eqToHom (h))).hom (x d) =
-         (S.FDiscrete.map (Discrete.eqToHom h')).hom (x b) := by
+          (S.FDiscrete.map (Discrete.eqToHom (h))).hom (x d) =
+          (S.FDiscrete.map (Discrete.eqToHom h')).hom (x b) := by
         subst hbd
         rfl
       refine h1' ?_ ?_ ?_
       erw [swapJ_swapI_succAbove]
       rfl
     · congr 1
-      simp
+      simp only [Monoidal.tensorUnit_obj, Action.instMonoidalCategory_tensorUnit_V,
+        Nat.succ_eq_add_one, Function.comp_apply, Equivalence.symm_inverse,
+        Action.functorCategoryEquivalence_functor,
+        Action.FunctorCategoryEquivalence.functor_obj_obj, Functor.comp_obj,
+        Discrete.functor_obj_eq_as]
       have h' {a a' b b' : Fin n.succ.succ.succ.succ} (hab : c b = S.τ (c a))
-        (hab' : c b' = S.τ (c a')) (ha : a = a') (hb : b= b') :
-        (S.contr.app { as := c a }).hom (x a ⊗ₜ[S.k] (S.FDiscrete.map (Discrete.eqToHom hab)).hom (x b)) =
-        (S.contr.app { as := c a' }).hom (x a' ⊗ₜ[S.k]
-        (S.FDiscrete.map (Discrete.eqToHom hab')).hom
-         (x b')) := by
+          (hab' : c b' = S.τ (c a')) (ha : a = a') (hb : b= b') :
+          (S.contr.app { as := c a }).hom
+          (x a ⊗ₜ[S.k] (S.FDiscrete.map (Discrete.eqToHom hab)).hom (x b)) =
+          (S.contr.app { as := c a' }).hom (x a' ⊗ₜ[S.k]
+          (S.FDiscrete.map (Discrete.eqToHom hab')).hom (x b')) := by
         subst ha hb
         rfl
       apply h'
@@ -252,12 +256,12 @@ theorem contr_contr {n : ℕ} {c : Fin n.succ.succ.succ.succ → S.C} {i : Fin n
     {j : Fin n.succ.succ.succ} {k : Fin n.succ.succ} {l : Fin n.succ}
     (hij : c (i.succAbove j) = S.τ (c i)) (hkl : (c ∘ i.succAbove ∘ j.succAbove) (k.succAbove l) =
     S.τ ((c ∘ i.succAbove ∘ j.succAbove) k))
-    (t : TensorTree S c)  :
+    (t : TensorTree S c) :
     (contr k l hkl (contr i j hij t)).tensor =
     (perm (ContrQuartet.mk i j k l hij hkl).contrSwapHom
     (contr (ContrQuartet.mk i j k l hij hkl).swapK (ContrQuartet.mk i j k l hij hkl).swapL
     (ContrQuartet.mk i j k l hij hkl).swap.hkl (contr (ContrQuartet.mk i j k l hij hkl).swapI
-    (ContrQuartet.mk i j k l hij hkl).swapJ (ContrQuartet.mk i j k l hij hkl).swap.hij t))).tensor  := by
+    (ContrQuartet.mk i j k l hij hkl).swapJ (ContrQuartet.mk i j k l hij hkl).swap.hij t))).tensor := by
   exact ContrQuartet.contr_contr (ContrQuartet.mk i j k l hij hkl) t
 
 end TensorTree
diff --git a/HepLean/Tensors/Tree/NodeIdentities/PermContr.lean b/HepLean/Tensors/Tree/NodeIdentities/PermContr.lean
index ded8076..94b79bf 100644
--- a/HepLean/Tensors/Tree/NodeIdentities/PermContr.lean
+++ b/HepLean/Tensors/Tree/NodeIdentities/PermContr.lean
@@ -39,9 +39,9 @@ lemma contrFin1Fin1_naturality {n : ℕ} {c c1 : Fin n.succ.succ → S.C}
       (perm_contr_cond S h σ)).hom
     ≫ ((Discrete.pairτ S.FDiscrete S.τ).map (Discrete.eqToHom (Hom.toEquiv_comp_inv_apply σ i)
       : (Discrete.mk (c ((Hom.toEquiv σ).symm i))) ⟶ (Discrete.mk (c1 i)))) := by
-    erw [← CategoryTheory.Iso.eq_comp_inv ]
+    erw [← CategoryTheory.Iso.eq_comp_inv]
     rw [CategoryTheory.Category.assoc]
-    erw [← CategoryTheory.Iso.inv_comp_eq ]
+    erw [← CategoryTheory.Iso.inv_comp_eq]
     ext1
     apply TensorProduct.ext'
     intro x y
@@ -51,7 +51,11 @@ lemma contrFin1Fin1_naturality {n : ℕ} {c c1 : Fin n.succ.succ → S.C}
       extractOne_homToEquiv, Action.Hom.comp_hom, LinearMap.coe_comp]
     trans (S.F.map (extractTwoAux' i j σ)).hom (PiTensorProduct.tprod S.k (fun k =>
       match k with | Sum.inl 0 => x | Sum.inr 0 => (S.FDiscrete.map
-      (eqToHom (by simp; erw [perm_contr_cond S h σ]))).hom y))
+      (eqToHom (by
+        simp only [Nat.succ_eq_add_one, Discrete.functor_obj_eq_as, Function.comp_apply,
+          extractOne_homToEquiv, Fin.isValue, mk_hom, finExtractTwo_symm_inl_inr_apply,
+          Discrete.mk.injEq]
+        erw [perm_contr_cond S h σ]))).hom y))
     · apply congrArg
       have h1' {α :Type} {a b c d : α} (hab : a= b) (hcd : c = d) (h : a = d) : b = c := by
           rw [← hab, hcd]
@@ -77,8 +81,11 @@ lemma contrFin1Fin1_naturality {n : ℕ} {c c1 : Fin n.succ.succ → S.C}
     match i with
     | Sum.inl 0 => rfl
     | Sum.inr 0 =>
-      simp [lift.discreteFunctorMapEqIso]
-      change  ((S.FDiscrete.map (eqToHom _)) ≫ S.FDiscrete.map (eqToHom _)).hom y = ((S.FDiscrete.map (eqToHom _)) ≫ S.FDiscrete.map (eqToHom _)).hom y
+      simp only [Nat.succ_eq_add_one, mk_hom, Fin.isValue, Function.comp_apply,
+        extractOne_homToEquiv, lift.discreteFunctorMapEqIso, Functor.mapIso_hom, eqToIso.hom,
+        Functor.mapIso_inv, eqToIso.inv, Functor.id_obj, Discrete.functor_obj_eq_as,
+        LinearEquiv.ofLinear_apply]
+      change ((S.FDiscrete.map (eqToHom _)) ≫ S.FDiscrete.map (eqToHom _)).hom y = ((S.FDiscrete.map (eqToHom _)) ≫ S.FDiscrete.map (eqToHom _)).hom y
       rw [← Functor.map_comp, ← Functor.map_comp]
       simp only [Fin.isValue, Nat.succ_eq_add_one, Discrete.functor_obj_eq_as, Function.comp_apply,
         eqToHom_trans]
@@ -89,12 +96,11 @@ lemma contrIso_comm_aux_1 {n : ℕ} {c c1 : Fin n.succ.succ → S.C}
     (σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) :
     ((S.F.map σ).hom ≫ (S.F.map (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).hom) ≫
         (S.F.map (mkSum (c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).hom =
-     (S.F.map (equivToIso (HepLean.Fin.finExtractTwo ((Hom.toEquiv σ).symm i)
-     ((HepLean.Fin.finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j))).hom).hom  ≫ (S.F.map
-     (mkSum (c ∘ ⇑(HepLean.Fin.finExtractTwo ((Hom.toEquiv σ).symm i)
+    (S.F.map (equivToIso (HepLean.Fin.finExtractTwo ((Hom.toEquiv σ).symm i)
+    ((HepLean.Fin.finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j))).hom).hom ≫ (S.F.map
+    (mkSum (c ∘ ⇑(HepLean.Fin.finExtractTwo ((Hom.toEquiv σ).symm i)
     ((HepLean.Fin.finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j)).symm)).hom).hom
-     ≫ (S.F.map (extractTwoAux' i j σ ⊗ extractTwoAux i j σ)).hom
-     := by
+    ≫ (S.F.map (extractTwoAux' i j σ ⊗ extractTwoAux i j σ)).hom := by
   ext X
   change ((S.F.map σ) ≫ (S.F.map (equivToIso (HepLean.Fin.finExtractTwo i j)).hom) ≫ (S.F.map (mkSum (c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom)).hom X = _
   rw [← Functor.map_comp, ← Functor.map_comp]
@@ -109,14 +115,14 @@ lemma contrIso_comm_aux_2 {n : ℕ} {c c1 : Fin n.succ.succ → S.C}
     (S.F.map (extractTwoAux' i j σ ⊗ extractTwoAux i j σ)).hom ≫
     (S.F.μIso (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl))
     (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv.hom =
-    (S.F.μIso _ _).inv.hom ≫ (S.F.map (extractTwoAux' i j σ) ⊗ S.F.map (extractTwoAux i j σ)).hom
-     := by
+    (S.F.μIso _ _).inv.hom ≫
+    (S.F.map (extractTwoAux' i j σ) ⊗ S.F.map (extractTwoAux i j σ)).hom := by
   have h1 : (S.F.map (extractTwoAux' i j σ ⊗ extractTwoAux i j σ)) ≫
     (S.F.μIso (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl))
     (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv =
     (S.F.μIso _ _).inv ≫ (S.F.map (extractTwoAux' i j σ) ⊗ S.F.map (extractTwoAux i j σ)) := by
     erw [CategoryTheory.IsIso.comp_inv_eq, CategoryTheory.Category.assoc]
-    erw [CategoryTheory.IsIso.eq_inv_comp ]
+    erw [CategoryTheory.IsIso.eq_inv_comp]
     exact Eq.symm
         (LaxMonoidalFunctor.μ_natural S.F.toLaxMonoidalFunctor (extractTwoAux' i j σ)
           (extractTwoAux i j σ))
@@ -143,8 +149,9 @@ lemma contrIso_comm_aux_3 {n : ℕ} {c c1 : Fin n.succ.succ → S.C}
 
 def contrIsoComm {n : ℕ} {c c1 : Fin n.succ.succ → S.C}
     {i : Fin n.succ.succ} {j : Fin n.succ} (σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) :=
-     (((Discrete.pairτ S.FDiscrete S.τ).map (Discrete.eqToHom (Hom.toEquiv_comp_inv_apply σ i)
-      : (Discrete.mk (c ((Hom.toEquiv σ).symm i))) ⟶ (Discrete.mk (c1 i)))) ⊗ (S.F.map (extractTwo i j σ)))
+  (((Discrete.pairτ S.FDiscrete S.τ).map (Discrete.eqToHom (Hom.toEquiv_comp_inv_apply σ i) :
+  (Discrete.mk (c ((Hom.toEquiv σ).symm i))) ⟶
+  (Discrete.mk (c1 i)))) ⊗ (S.F.map (extractTwo i j σ)))
 
 lemma contrIso_comm_aux_5 {n : ℕ} {c c1 : Fin n.succ.succ → S.C}
     {i : Fin n.succ.succ} {j : Fin n.succ} (h : c1 (i.succAbove j) = S.τ (c1 i))
@@ -155,8 +162,7 @@ lemma contrIso_comm_aux_5 {n : ℕ} {c c1 : Fin n.succ.succ → S.C}
       ((HepLean.Fin.finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j)
       (perm_contr_cond S h σ)).hom.hom ⊗ (S.F.map (mkIso (contrIso.proof_1 S c ((Hom.toEquiv σ).symm i)
     ((HepLean.Fin.finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j))).hom).hom)
-    ≫ (S.contrIsoComm σ).hom
-     := by
+    ≫ (S.contrIsoComm σ).hom := by
   erw [← CategoryTheory.MonoidalCategory.tensor_comp (f₁ := (S.F.map (extractTwoAux' i j σ)).hom)]
   rw [contrIso_comm_aux_3 S σ]
   rw [contrFin1Fin1_naturality S h σ]