diff --git a/HepLean/Tensors/OverColor/Discrete.lean b/HepLean/Tensors/OverColor/Discrete.lean
index fe755508..ad96e65d 100644
--- a/HepLean/Tensors/OverColor/Discrete.lean
+++ b/HepLean/Tensors/OverColor/Discrete.lean
@@ -77,14 +77,16 @@ lemma pairIsoSep_tmul {c1 c2 : C} (x : F.obj (Discrete.mk c1)) (y : F.obj (Discr
     Category.assoc, Functor.LaxMonoidal.μ_natural_assoc, Action.comp_hom,
     Action.instMonoidalCategory_tensorHom_hom, Action.mkIso_inv_hom, ModuleCat.hom_comp,
     Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
-    Action.FunctorCategoryEquivalence.functor_obj_obj, mk_hom, mk_left, Functor.id_obj]
+    Action.FunctorCategoryEquivalence.functor_obj_obj, mk_hom, Functor.id_obj]
   simp only [LinearMap.coe_comp, Function.comp_apply, ModuleCat.MonoidalCategory.tensorHom_tmul,
-    LinearEquiv.coe_coe, forgetLiftAppV_symm_apply, mk_left, Functor.id_obj]
-  change ((lift.obj F).map fin2Iso.inv).hom
-    (((lift.obj F).map ((mkIso _).hom ⊗ (mkIso _).hom)).hom
-      ((Functor.LaxMonoidal.μ (lift.obj F).toFunctor (mk fun _ => c1) (mk fun _ => c2)).hom
-        (((PiTensorProduct.tprod k) fun _ => x) ⊗ₜ[k] (PiTensorProduct.tprod k) fun _ => y))) = _
-  rw [lift.obj_μ_tprod_tmul F (mk fun _ => c1) (mk fun _ => c2)]
+    LinearEquiv.coe_coe, forgetLiftAppV_symm_apply, Functor.id_obj]
+  rw [ModuleCat.Hom.hom, ModuleCat.Hom.hom, ModuleCat.Hom.hom, ConcreteCategory.hom]
+  simp only [LinearEquiv.toModuleIso_inv, ModuleCat.instConcreteCategoryLinearMapIdCarrier]
+  conv_lhs =>
+    enter [2, 2]
+    change ((Functor.LaxMonoidal.μ (lift.obj F).toFunctor (mk fun _ => c1) (mk fun _ => c2)).hom
+        (((PiTensorProduct.tprod k) fun _ => x) ⊗ₜ[k] (PiTensorProduct.tprod k) fun _ => y))
+    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) _)) = _
@@ -119,8 +121,12 @@ lemma pairIsoSep_inv_tprod {c1 c2 : C} (fx : (i : (𝟭 Type).obj (OverColor.mk
     Functor.id_obj, mk_hom, ModuleCat.hom_comp, Function.comp_apply, Equivalence.symm_inverse,
     Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj]
   simp_rw [LinearMap.comp_apply]
-  erw [lift.map_tprod]
-  erw [lift.μIso_inv_tprod]
+  conv_lhs =>
+    enter [2, 2, 2]
+    erw [lift.map_tprod]
+  conv_lhs =>
+    enter [2, 2]
+    erw [lift.μIso_inv_tprod]
   change (((forgetLiftApp F c1).hom.hom (((lift.obj F).map (mkIso _).inv).hom
     ((PiTensorProduct.tprod k) fun i =>
     (lift.discreteFunctorMapEqIso F _) (fx ((Hom.toEquiv fin2Iso.hom).symm (Sum.inl i)))))) ⊗ₜ[k]
@@ -218,15 +224,19 @@ lemma tripleIsoSep_tmul {c1 c2 c3 : C} (x : F.obj (Discrete.mk c1)) (y : F.obj (
     tripleIsoSep, Functor.mapIso_symm, Iso.trans_hom, whiskerLeftIso_hom, whiskerRightIso_hom,
     Iso.symm_hom, Functor.mapIso_inv, Action.comp_hom,
     Action.instMonoidalCategory_whiskerLeft_hom, Action.instMonoidalCategory_whiskerRight_hom,
-    Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
+    Action.functorCategoryEquivalence_functor,
     Action.FunctorCategoryEquivalence.functor_obj_obj, ModuleCat.hom_comp, Function.comp_apply,
     ModuleCat.MonoidalCategory.whiskerLeft_apply, ModuleCat.MonoidalCategory.whiskerRight_apply,
     Functor.id_obj, mk_hom]
   simp only [Functor.Monoidal.μIso_hom, Functor.CoreMonoidal.toMonoidal_toLaxMonoidal,
     LinearMap.coe_comp, Function.comp_apply, ModuleCat.MonoidalCategory.whiskerLeft_apply,
     ModuleCat.MonoidalCategory.whiskerRight_apply, mk_left]
-  erw [pairIsoSep_tmul F y z]
-  erw [forgetLiftAppV_symm_apply F c1]
+  conv_lhs =>
+    enter [2, 2]
+    erw [pairIsoSep_tmul F y z]
+  conv_lhs =>
+    enter [2, 2, 2]
+    erw [forgetLiftAppV_symm_apply F c1]
   conv_lhs =>
     enter [2]
     erw [lift.obj_μ_tprod_tmul F _ _]
diff --git a/HepLean/Tensors/OverColor/Lift.lean b/HepLean/Tensors/OverColor/Lift.lean
index 7181aa74..ce691433 100644
--- a/HepLean/Tensors/OverColor/Lift.lean
+++ b/HepLean/Tensors/OverColor/Lift.lean
@@ -91,13 +91,10 @@ lemma objObj'_ρ_tprod (f : OverColor C) (M : G) (x : (i : f.left) → F.obj (Di
 
 @[simp]
 lemma objObj'_ρ_empty (g : G) : (objObj' F (𝟙_ (OverColor C))).ρ g = LinearMap.id := by
-  erw [objObj'_ρ]
+  rw [objObj'_ρ]
   ext x
   refine PiTensorProduct.induction_on' x (fun r x => ?_) <| fun x y hx hy => by
-    simp only [CategoryTheory.Functor.id_obj, map_add, hx, ModuleCat.hom_comp,
-      Function.comp_apply, hy]
-    erw [hx, hy]
-    rfl
+    simp_all
   simp only [OverColor.instMonoidalCategoryStruct_tensorUnit_left, Functor.id_obj,
     OverColor.instMonoidalCategoryStruct_tensorUnit_hom, PiTensorProduct.tprodCoeff_eq_smul_tprod,
     _root_.map_smul, PiTensorProduct.map_tprod, LinearMap.id_coe, id_eq]
diff --git a/HepLean/Tensors/TensorSpecies/Basic.lean b/HepLean/Tensors/TensorSpecies/Basic.lean
index 2054c584..4a6ef972 100644
--- a/HepLean/Tensors/TensorSpecies/Basic.lean
+++ b/HepLean/Tensors/TensorSpecies/Basic.lean
@@ -189,7 +189,10 @@ lemma evalIso_tprod {n : ℕ} {c : Fin n.succ → S.C} (i : Fin n.succ)
     (((lift.obj S.FD).map (mkSum (c ∘ ⇑(HepLean.Fin.finExtractOne i).symm)).hom).hom
     (((lift.obj S.FD).map (equivToIso (HepLean.Fin.finExtractOne i)).hom).hom
     ((PiTensorProduct.tprod S.k) _)))) =_
-  rw [lift.map_tprod]
+  conv_lhs =>
+    enter [2, 2, 2]
+    rw [lift.map_tprod]
+
   change (((lift.obj S.FD).map (mkIso _).hom).hom ≫
     (forgetLiftApp S.FD (c i)).hom.hom ⊗
     ((lift.obj S.FD).map (mkIso _).hom).hom)
@@ -198,7 +201,9 @@ lemma evalIso_tprod {n : ℕ} {c : Fin n.succ → S.C} (i : Fin n.succ)
     (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractOne i).symm) ∘ Sum.inr))).inv.hom
     (((lift.obj S.FD).map (mkSum (c ∘ ⇑(HepLean.Fin.finExtractOne i).symm)).hom).hom
     (((PiTensorProduct.tprod S.k) _)))) =_
-  rw [lift.map_tprod]
+  conv_lhs =>
+    enter [2, 2]
+    rw [lift.map_tprod]
   change ((TensorProduct.map (((lift.obj S.FD).map (mkIso _).hom).hom ≫
     (forgetLiftApp S.FD (c i)).hom.hom).hom
     ((lift.obj S.FD).map (mkIso _).hom).hom.hom))
@@ -208,11 +213,11 @@ lemma evalIso_tprod {n : ℕ} {c : Fin n.succ → S.C} (i : Fin n.succ)
     ((((PiTensorProduct.tprod S.k) _)))) =_
   rw [lift.μIso_inv_tprod]
   rw [TensorProduct.map_tmul]
-  erw [lift.map_tprod]
-  simp only [Nat.succ_eq_add_one, CategoryStruct.comp, Functor.id_obj,
+  conv_lhs =>
+    erw [lift.map_tprod]
+  simp only [ CategoryStruct.comp, Functor.id_obj,
     instMonoidalCategoryStruct_tensorObj_hom, mk_hom, Sum.elim_inl, Function.comp_apply,
-    instMonoidalCategoryStruct_tensorObj_left, mkSum_homToEquiv, Equiv.refl_symm,
-    LinearMap.coe_comp, Sum.elim_inr]
+    instMonoidalCategoryStruct_tensorObj_left, mkSum_homToEquiv, Equiv.refl_symm]
   congr 1
   · change (forgetLiftApp S.FD (c i)).hom.hom
       (((lift.obj S.FD).map (mkIso _).hom).hom
diff --git a/HepLean/Tensors/TensorSpecies/MetricTensor.lean b/HepLean/Tensors/TensorSpecies/MetricTensor.lean
index c2b300fa..32f313d6 100644
--- a/HepLean/Tensors/TensorSpecies/MetricTensor.lean
+++ b/HepLean/Tensors/TensorSpecies/MetricTensor.lean
@@ -108,6 +108,8 @@ lemma metricTensor_contr_dual_metricTensor_outer_eq_unit (c : S.C) :
   conv_lhs =>
     right
     rw [extractTwo_hom_left_apply]
+  rw [extractTwo_hom_left_apply 0 2 (braidPerm ![c, c] ![S.τ c, S.τ c]) _]
+  rw [braidPerm_toEquiv]
   simp only [mk_left, braidPerm_toEquiv, permProdRight_toEquiv, equivToHomEq_toEquiv,
     finExtractOnePerm_apply, finExtractOne_symm_inr_apply, extractTwo_hom_left_apply]
   fin_cases i
diff --git a/HepLean/Tensors/Tree/NodeIdentities/PermContr.lean b/HepLean/Tensors/Tree/NodeIdentities/PermContr.lean
index 41e229f0..e3c2de35 100644
--- a/HepLean/Tensors/Tree/NodeIdentities/PermContr.lean
+++ b/HepLean/Tensors/Tree/NodeIdentities/PermContr.lean
@@ -237,9 +237,8 @@ lemma contrMap_naturality {n : ℕ} {c c1 : Fin n.succ.succ → S.C}
   rw [← tensor_comp]
   have h1 : 𝟙_ (Rep S.k S.G) ◁ S.F.map (extractTwo i j σ) = 𝟙 _ ⊗ S.F.map (extractTwo i j σ) := by
     rfl
-  rw [h1, ← tensor_comp]
-  rw [CategoryTheory.Category.id_comp]
-  erw [CategoryTheory.Category.comp_id, CategoryTheory.Category.comp_id]
+  rw [h1, ← tensor_comp, Category.id_comp]
+  erw [Category.comp_id, Category.comp_id]
   rw [S.contr.naturality]
   rfl
 
diff --git a/HepLean/Tensors/Tree/NodeIdentities/ProdContr.lean b/HepLean/Tensors/Tree/NodeIdentities/ProdContr.lean
index e6721d99..15f99d4b 100644
--- a/HepLean/Tensors/Tree/NodeIdentities/ProdContr.lean
+++ b/HepLean/Tensors/Tree/NodeIdentities/ProdContr.lean
@@ -235,9 +235,7 @@ lemma contrMap_prod_tprod (p : (i : (𝟭 Type).obj (OverColor.mk c).left) →
     refine h1' ?_ ?_ ?_
     · simp only [leftContr, Nat.succ_eq_add_one, Equiv.toFun_as_coe, leftContrI,
       Equiv.symm_apply_apply, finSumFinEquiv_symm_apply_castAdd, Sum.elim_inl]
-    · erw [ModuleCat.id_apply, ModuleCat.id_apply, ModuleCat.id_apply, ModuleCat.id_apply]
-      simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, equivToIso_homToEquiv,
-        LinearEquiv.coe_coe]
+    · simp only [mk_left, equivToIso_homToEquiv, ModuleCat.hom_id, LinearMap.id_coe, id_eq]
       apply contrMap_prod_tprod_aux_2
       exact Eq.symm ((fun f => (Equiv.apply_eq_iff_eq_symm_apply f).mp) finSumFinEquiv rfl)
     · simp only [Discrete.functor_obj_eq_as, Function.comp_apply, AddHom.toFun_eq_coe,
@@ -272,7 +270,7 @@ lemma contrMap_prod_tprod (p : (i : (𝟭 Type).obj (OverColor.mk c).left) →
         (Hom.toEquiv_comp_inv_apply (mkIso (leftContr_map_eq q)).hom k)
     · obtain ⟨k, hk⟩ := finSumFinEquiv.surjective k
       subst hk
-      erw [Equiv.symm_apply_apply]
+      simp only [mk_left, Equiv.refl_apply, Equiv.symm_apply_apply]
       match k with
       | Sum.inl k => exact q.sum_inl_succAbove_leftContrI_leftContrJ _
       | Sum.inr k => exact q.sum_inr_succAbove_leftContrI_leftContrJ _