diff --git a/Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean b/Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean
index 326c4ee2370785..56103d1581601d 100644
--- a/Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean
+++ b/Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean
@@ -85,7 +85,7 @@ noncomputable instance instMonoidalCategory : MonoidalCategory (AlgebraCat.{u} R
       leftUnitor_eq := fun X => by
         dsimp only [forget₂_module_obj, forget₂_module_map, Iso.refl_symm, Iso.trans_hom,
           Iso.refl_hom, tensorIso_hom]
-        simp only [MonoidalCategory.leftUnitor_conjugation, Category.id_comp, Iso.hom_inv_id]
+        erw [Category.id_comp, MonoidalCategory.tensor_id, Category.id_comp]
         rfl
       rightUnitor_eq := fun X => by
         dsimp
diff --git a/Mathlib/CategoryTheory/Bicategory/SingleObj.lean b/Mathlib/CategoryTheory/Bicategory/SingleObj.lean
index d19bfd4843cb4f..d039080525e0cc 100644
--- a/Mathlib/CategoryTheory/Bicategory/SingleObj.lean
+++ b/Mathlib/CategoryTheory/Bicategory/SingleObj.lean
@@ -68,8 +68,6 @@ protected def star : MonoidalSingleObj C :=
   PUnit.unit
 #align category_theory.monoidal_single_obj.star CategoryTheory.MonoidalSingleObj.star
 
-attribute [local simp] id_tensorHom tensorHom_id in
-
 /-- The monoidal functor from the endomorphisms of the single object
 when we promote a monoidal category to a single object bicategory,
 to the original monoidal category.
diff --git a/Mathlib/CategoryTheory/Closed/Monoidal.lean b/Mathlib/CategoryTheory/Closed/Monoidal.lean
index 9bf935d482eb43..ff1d394553d006 100644
--- a/Mathlib/CategoryTheory/Closed/Monoidal.lean
+++ b/Mathlib/CategoryTheory/Closed/Monoidal.lean
@@ -72,7 +72,7 @@ def unitClosed : Closed (𝟙_ C) where
                 right_inv := by aesop_cat }
             homEquiv_naturality_left_symm := fun f g => by
               dsimp
-              rw [leftUnitor_naturality'_assoc]
+              rw [leftUnitor_naturality_assoc]
             -- This used to be automatic before leanprover/lean4#2644
             homEquiv_naturality_right := by  -- aesop failure
               dsimp
diff --git a/Mathlib/CategoryTheory/Enriched/Basic.lean b/Mathlib/CategoryTheory/Enriched/Basic.lean
index 5499018e5c2065..6f303197d6c156 100644
--- a/Mathlib/CategoryTheory/Enriched/Basic.lean
+++ b/Mathlib/CategoryTheory/Enriched/Basic.lean
@@ -53,10 +53,10 @@ class EnrichedCategory (C : Type u₁) where
   Hom : C → C → V
   id (X : C) : 𝟙_ V ⟶ Hom X X
   comp (X Y Z : C) : Hom X Y ⊗ Hom Y Z ⟶ Hom X Z
-  id_comp (X Y : C) : (λ_ (Hom X Y)).inv ≫ (id X ⊗ 𝟙 _) ≫ comp X X Y = 𝟙 _ := by aesop_cat
-  comp_id (X Y : C) : (ρ_ (Hom X Y)).inv ≫ (𝟙 _ ⊗ id Y) ≫ comp X Y Y = 𝟙 _ := by aesop_cat
-  assoc (W X Y Z : C) : (α_ _ _ _).inv ≫ (comp W X Y ⊗ 𝟙 _) ≫ comp W Y Z =
-    (𝟙 _ ⊗ comp X Y Z) ≫ comp W X Z := by aesop_cat
+  id_comp (X Y : C) : (λ_ (Hom X Y)).inv ≫ id X ▷ _ ≫ comp X X Y = 𝟙 _ := by aesop_cat
+  comp_id (X Y : C) : (ρ_ (Hom X Y)).inv ≫ _ ◁ id Y ≫ comp X Y Y = 𝟙 _ := by aesop_cat
+  assoc (W X Y Z : C) : (α_ _ _ _).inv ≫ comp W X Y ▷ _ ≫ comp W Y Z =
+    _ ◁ comp X Y Z ≫ comp W X Z := by aesop_cat
 #align category_theory.enriched_category CategoryTheory.EnrichedCategory
 
 notation X " ⟶[" V "] " Y:10 => (EnrichedCategory.Hom X Y : V)
@@ -78,20 +78,20 @@ def eComp (X Y Z : C) : ((X ⟶[V] Y) ⊗ Y ⟶[V] Z) ⟶ X ⟶[V] Z :=
 -- We don't just use `restate_axiom` here; that would leave `V` as an implicit argument.
 @[reassoc (attr := simp)]
 theorem e_id_comp (X Y : C) :
-    (λ_ (X ⟶[V] Y)).inv ≫ (eId V X ⊗ 𝟙 _) ≫ eComp V X X Y = 𝟙 (X ⟶[V] Y) :=
+    (λ_ (X ⟶[V] Y)).inv ≫ eId V X ▷ _ ≫ eComp V X X Y = 𝟙 (X ⟶[V] Y) :=
   EnrichedCategory.id_comp X Y
 #align category_theory.e_id_comp CategoryTheory.e_id_comp
 
 @[reassoc (attr := simp)]
 theorem e_comp_id (X Y : C) :
-    (ρ_ (X ⟶[V] Y)).inv ≫ (𝟙 _ ⊗ eId V Y) ≫ eComp V X Y Y = 𝟙 (X ⟶[V] Y) :=
+    (ρ_ (X ⟶[V] Y)).inv ≫ _ ◁ eId V Y ≫ eComp V X Y Y = 𝟙 (X ⟶[V] Y) :=
   EnrichedCategory.comp_id X Y
 #align category_theory.e_comp_id CategoryTheory.e_comp_id
 
 @[reassoc (attr := simp)]
 theorem e_assoc (W X Y Z : C) :
-    (α_ _ _ _).inv ≫ (eComp V W X Y ⊗ 𝟙 _) ≫ eComp V W Y Z =
-      (𝟙 _ ⊗ eComp V X Y Z) ≫ eComp V W X Z :=
+    (α_ _ _ _).inv ≫ eComp V W X Y ▷ _ ≫ eComp V W Y Z =
+      _ ◁ eComp V X Y Z ≫ eComp V W X Z :=
   EnrichedCategory.assoc W X Y Z
 #align category_theory.e_assoc CategoryTheory.e_assoc
 
@@ -114,18 +114,23 @@ instance (F : LaxMonoidalFunctor V W) : EnrichedCategory W (TransportEnrichment
   id := fun X : C => F.ε ≫ F.map (eId V X)
   comp := fun X Y Z : C => F.μ _ _ ≫ F.map (eComp V X Y Z)
   id_comp X Y := by
-    rw [comp_tensor_id, Category.assoc, ← F.toFunctor.map_id, F.μ_natural_assoc,
-      F.toFunctor.map_id, F.left_unitality_inv_assoc, ← F.toFunctor.map_comp, ←
-      F.toFunctor.map_comp, e_id_comp, F.toFunctor.map_id]
+    simp only [comp_whiskerRight, Category.assoc, LaxMonoidalFunctor.μ_natural_left_assoc,
+      LaxMonoidalFunctor.left_unitality_inv_assoc]
+    simp_rw [← F.map_comp]
+    convert F.map_id _
+    simp
   comp_id X Y := by
-    rw [id_tensor_comp, Category.assoc, ← F.toFunctor.map_id, F.μ_natural_assoc,
-      F.toFunctor.map_id, F.right_unitality_inv_assoc, ← F.toFunctor.map_comp, ←
-      F.toFunctor.map_comp, e_comp_id, F.toFunctor.map_id]
+    simp only [MonoidalCategory.whiskerLeft_comp, Category.assoc,
+      LaxMonoidalFunctor.μ_natural_right_assoc,
+      LaxMonoidalFunctor.right_unitality_inv_assoc]
+    simp_rw [← F.map_comp]
+    convert F.map_id _
+    simp
   assoc P Q R S := by
-    rw [comp_tensor_id, Category.assoc, ← F.toFunctor.map_id, F.μ_natural_assoc,
-      F.toFunctor.map_id, ← F.associativity_inv_assoc, ← F.toFunctor.map_comp, ←
-      F.toFunctor.map_comp, e_assoc, id_tensor_comp, Category.assoc, ← F.toFunctor.map_id,
-      F.μ_natural_assoc, F.toFunctor.map_comp]
+    rw [comp_whiskerRight, Category.assoc, F.μ_natural_left_assoc,
+      ← F.associativity_inv_assoc, ← F.map_comp, ← F.map_comp, e_assoc,
+      F.map_comp, MonoidalCategory.whiskerLeft_comp, Category.assoc,
+      LaxMonoidalFunctor.μ_natural_right_assoc]
 
 end
 
diff --git a/Mathlib/CategoryTheory/Monoidal/Bimod.lean b/Mathlib/CategoryTheory/Monoidal/Bimod.lean
index 260ada925481ef..6731d26102bf31 100644
--- a/Mathlib/CategoryTheory/Monoidal/Bimod.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Bimod.lean
@@ -255,7 +255,7 @@ theorem one_act_left' : (R.one ▷ _) ≫ actLeft P Q = (λ_ _).hom := by
   slice_lhs 2 3 => rw [whiskerLeft_π_actLeft]
   slice_lhs 1 2 => rw [associator_inv_naturality_left]
   slice_lhs 2 3 => rw [← comp_whiskerRight, one_actLeft]
-  slice_rhs 1 2 => rw [leftUnitor_naturality']
+  slice_rhs 1 2 => rw [leftUnitor_naturality]
   coherence
 set_option linter.uppercaseLean3 false in
 #align Bimod.tensor_Bimod.one_act_left' Bimod.TensorBimod.one_act_left'
@@ -668,7 +668,7 @@ theorem hom_inv_id : hom P ≫ inv P = 𝟙 _ := by
   dsimp only [hom, inv, TensorBimod.X]
   ext; dsimp
   slice_lhs 1 2 => rw [coequalizer.π_desc]
-  slice_lhs 1 2 => rw [leftUnitor_inv_naturality']
+  slice_lhs 1 2 => rw [leftUnitor_inv_naturality]
   slice_lhs 2 3 => rw [whisker_exchange]
   slice_lhs 3 3 => rw [← Iso.inv_hom_id_assoc (α_ R.X R.X P.X) (R.X ◁ P.actLeft)]
   slice_lhs 4 6 => rw [← Category.assoc, ← coequalizer.condition]
@@ -736,7 +736,7 @@ theorem hom_inv_id : hom P ≫ inv P = 𝟙 _ := by
   dsimp only [hom, inv, TensorBimod.X]
   ext; dsimp
   slice_lhs 1 2 => rw [coequalizer.π_desc]
-  slice_lhs 1 2 => rw [rightUnitor_inv_naturality']
+  slice_lhs 1 2 => rw [rightUnitor_inv_naturality]
   slice_lhs 2 3 => rw [← whisker_exchange]
   slice_lhs 3 4 => rw [coequalizer.condition]
   slice_lhs 2 3 => rw [associator_naturality_right]
@@ -858,7 +858,7 @@ theorem id_whiskerLeft_bimod {X Y : Mon_ C} {M N : Bimod X Y} (f : M ⟶ N) :
   slice_rhs 1 2 => rw [coequalizer.π_desc]
   dsimp [LeftUnitorBimod.inv]
   slice_rhs 1 2 => rw [Hom.left_act_hom]
-  slice_rhs 2 3 => rw [leftUnitor_inv_naturality']
+  slice_rhs 2 3 => rw [leftUnitor_inv_naturality]
   slice_rhs 3 4 => rw [whisker_exchange]
   slice_rhs 4 4 => rw [← Iso.inv_hom_id_assoc (α_ X.X X.X N.X) (X.X ◁ N.actLeft)]
   slice_rhs 5 7 => rw [← Category.assoc, ← coequalizer.condition]
@@ -918,7 +918,7 @@ theorem whiskerRight_id_bimod {X Y : Mon_ C} {M N : Bimod X Y} (f : M ⟶ N) :
   slice_rhs 1 2 => rw [coequalizer.π_desc]
   dsimp [RightUnitorBimod.inv]
   slice_rhs 1 2 => rw [Hom.right_act_hom]
-  slice_rhs 2 3 => rw [rightUnitor_inv_naturality']
+  slice_rhs 2 3 => rw [rightUnitor_inv_naturality]
   slice_rhs 3 4 => rw [← whisker_exchange]
   slice_rhs 4 5 => rw [coequalizer.condition]
   slice_rhs 3 4 => rw [associator_naturality_right]
diff --git a/Mathlib/CategoryTheory/Monoidal/Braided.lean b/Mathlib/CategoryTheory/Monoidal/Braided.lean
index a75609e2cefda8..6c78ad50cccbb8 100644
--- a/Mathlib/CategoryTheory/Monoidal/Braided.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Braided.lean
@@ -206,37 +206,37 @@ def braidedCategoryOfFaithful {C D : Type*} [Category C] [Category D] [MonoidalC
     intros
     apply F.map_injective
     refine (cancel_epi (F.μ ?_ ?_)).1 ?_
-    rw [Functor.map_comp, ← LaxMonoidalFunctor.μ_natural_left'_assoc, w, Functor.map_comp,
-      reassoc_of% w, braiding_naturality_left_assoc, LaxMonoidalFunctor.μ_natural_right']
+    rw [Functor.map_comp, ← LaxMonoidalFunctor.μ_natural_left_assoc, w, Functor.map_comp,
+      reassoc_of% w, braiding_naturality_left_assoc, LaxMonoidalFunctor.μ_natural_right]
   braiding_naturality_right := by
     intros
     apply F.map_injective
     refine (cancel_epi (F.μ ?_ ?_)).1 ?_
-    rw [Functor.map_comp, ← LaxMonoidalFunctor.μ_natural_right'_assoc, w, Functor.map_comp,
-      reassoc_of% w, braiding_naturality_right_assoc, LaxMonoidalFunctor.μ_natural_left']
+    rw [Functor.map_comp, ← LaxMonoidalFunctor.μ_natural_right_assoc, w, Functor.map_comp,
+      reassoc_of% w, braiding_naturality_right_assoc, LaxMonoidalFunctor.μ_natural_left]
   hexagon_forward := by
     intros
     apply F.map_injective
     refine (cancel_epi (F.μ _ _)).1 ?_
     refine (cancel_epi (F.μ _ _ ▷ _)).1 ?_
     rw [Functor.map_comp, Functor.map_comp, Functor.map_comp, Functor.map_comp, ←
-      LaxMonoidalFunctor.μ_natural_left'_assoc, ← comp_whiskerRight_assoc, w,
-      comp_whiskerRight_assoc, LaxMonoidalFunctor.associativity'_assoc,
-      LaxMonoidalFunctor.associativity'_assoc, ← LaxMonoidalFunctor.μ_natural_right', ←
+      LaxMonoidalFunctor.μ_natural_left_assoc, ← comp_whiskerRight_assoc, w,
+      comp_whiskerRight_assoc, LaxMonoidalFunctor.associativity_assoc,
+      LaxMonoidalFunctor.associativity_assoc, ← LaxMonoidalFunctor.μ_natural_right, ←
       MonoidalCategory.whiskerLeft_comp_assoc, w, MonoidalCategory.whiskerLeft_comp_assoc,
       reassoc_of% w, braiding_naturality_right_assoc,
-      LaxMonoidalFunctor.associativity', hexagon_forward_assoc]
+      LaxMonoidalFunctor.associativity, hexagon_forward_assoc]
   hexagon_reverse := by
     intros
     apply F.toFunctor.map_injective
     refine (cancel_epi (F.μ _ _)).1 ?_
     refine (cancel_epi (_ ◁ F.μ _ _)).1 ?_
     rw [Functor.map_comp, Functor.map_comp, Functor.map_comp, Functor.map_comp, ←
-      LaxMonoidalFunctor.μ_natural_right'_assoc, ← MonoidalCategory.whiskerLeft_comp_assoc, w,
-      MonoidalCategory.whiskerLeft_comp_assoc, LaxMonoidalFunctor.associativity_inv'_assoc,
-      LaxMonoidalFunctor.associativity_inv'_assoc, ← LaxMonoidalFunctor.μ_natural_left',
+      LaxMonoidalFunctor.μ_natural_right_assoc, ← MonoidalCategory.whiskerLeft_comp_assoc, w,
+      MonoidalCategory.whiskerLeft_comp_assoc, LaxMonoidalFunctor.associativity_inv_assoc,
+      LaxMonoidalFunctor.associativity_inv_assoc, ← LaxMonoidalFunctor.μ_natural_left,
       ← comp_whiskerRight_assoc, w, comp_whiskerRight_assoc, reassoc_of% w,
-      braiding_naturality_left_assoc, LaxMonoidalFunctor.associativity_inv', hexagon_reverse_assoc]
+      braiding_naturality_left_assoc, LaxMonoidalFunctor.associativity_inv, hexagon_reverse_assoc]
 #align category_theory.braided_category_of_faithful CategoryTheory.braidedCategoryOfFaithful
 
 /-- Pull back a braiding along a fully faithful monoidal functor. -/
@@ -290,7 +290,7 @@ theorem braiding_leftUnitor_aux₂ (X : C) :
     _ = (α_ _ _ _).hom ≫ (_ ◁ (λ_ _).hom) ≫ (β_ _ _).hom ≫ (β_ X _).inv :=
       by (slice_lhs 2 3 => rw [← braiding_naturality_right]); simp only [assoc]
     _ = (α_ _ _ _).hom ≫ (_ ◁ (λ_ _).hom) := by rw [Iso.hom_inv_id, comp_id]
-    _ = (ρ_ X).hom ▷ 𝟙_ C := by rw [triangle']
+    _ = (ρ_ X).hom ▷ 𝟙_ C := by rw [triangle]
 
 #align category_theory.braiding_left_unitor_aux₂ CategoryTheory.braiding_leftUnitor_aux₂
 
@@ -323,7 +323,7 @@ theorem braiding_rightUnitor_aux₂ (X : C) :
     _ = (α_ _ _ _).inv ≫ ((ρ_ _).hom ▷ _) ≫ (β_ _ X).hom ≫ (β_ _ _).inv :=
       by (slice_lhs 2 3 => rw [← braiding_naturality_left]); simp only [assoc]
     _ = (α_ _ _ _).inv ≫ ((ρ_ _).hom ▷ _) := by rw [Iso.hom_inv_id, comp_id]
-    _ = 𝟙_ C ◁ (λ_ X).hom := by rw [triangle_assoc_comp_right']
+    _ = 𝟙_ C ◁ (λ_ X).hom := by rw [triangle_assoc_comp_right]
 
 #align category_theory.braiding_right_unitor_aux₂ CategoryTheory.braiding_rightUnitor_aux₂
 
@@ -552,8 +552,6 @@ theorem tensor_μ_natural {X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C} (f₁ :
   simp only [assoc]
 #align category_theory.tensor_μ_natural CategoryTheory.tensor_μ_natural
 
-attribute [local simp] id_tensorHom tensorHom_id
-
 @[reassoc]
 theorem tensor_μ_natural_left {X₁ X₂ Y₁ Y₂ : C} (f₁: X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (Z₁ Z₂ : C) :
     (f₁ ⊗ f₂) ▷ (Z₁ ⊗ Z₂) ≫ tensor_μ C (Y₁, Y₂) (Z₁, Z₂) =
@@ -737,11 +735,10 @@ monoidal opposite, upgraded to a braided functor. -/
 @[simps!] def mopBraidedFunctor : BraidedFunctor C Cᴹᵒᵖ where
   μ X Y := (β_ (mop X) (mop Y)).hom
   ε := 𝟙 (𝟙_ Cᴹᵒᵖ)
-  -- `id_tensorHom`, `tensorHom_id` should be simp lemmas when #6307 is merged
-  -- we could then make this fully automated if we mark `yang_baxter` as simp
+  -- we could make this fully automated if we mark `← yang_baxter_assoc` as simp
   -- should it be marked as such?
   associativity X Y Z := by
-    simp [id_tensorHom, tensorHom_id, ← yang_baxter_assoc]
+    simp [← yang_baxter_assoc]
   __ := mopFunctor C
 
 /-- The identity functor on `C`, viewed as a functor from the
@@ -750,7 +747,7 @@ monoidal opposite of `C` to `C`, upgraded to a braided functor. -/
   μ X Y := (β_ (unmop X) (unmop Y)).hom
   ε := 𝟙 (𝟙_ C)
   associativity X Y Z := by
-    simp [id_tensorHom, tensorHom_id, ← yang_baxter_assoc]
+    simp [← yang_baxter_assoc]
   __ := unmopFunctor C
 
 end MonoidalOpposite
diff --git a/Mathlib/CategoryTheory/Monoidal/Category.lean b/Mathlib/CategoryTheory/Monoidal/Category.lean
index 08bbccfe88013d..81af11efc5d256 100644
--- a/Mathlib/CategoryTheory/Monoidal/Category.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Category.lean
@@ -181,34 +181,33 @@ class MonoidalCategory (C : Type u) [𝒞 : Category.{v} C] extends MonoidalCate
   Naturality of the left unitor, commutativity of `𝟙_ C ⊗ X ⟶ 𝟙_ C ⊗ Y ⟶ Y` and `𝟙_ C ⊗ X ⟶ X ⟶ Y`
   -/
   leftUnitor_naturality :
-    ∀ {X Y : C} (f : X ⟶ Y), (𝟙 (𝟙_ _) ⊗ f) ≫ (λ_ Y).hom = (λ_ X).hom ≫ f := by
+    ∀ {X Y : C} (f : X ⟶ Y), 𝟙_ _ ◁ f ≫ (λ_ Y).hom = (λ_ X).hom ≫ f := by
     aesop_cat
   /--
   Naturality of the right unitor: commutativity of `X ⊗ 𝟙_ C ⟶ Y ⊗ 𝟙_ C ⟶ Y` and `X ⊗ 𝟙_ C ⟶ X ⟶ Y`
   -/
   rightUnitor_naturality :
-    ∀ {X Y : C} (f : X ⟶ Y), (f ⊗ 𝟙 (𝟙_ _)) ≫ (ρ_ Y).hom = (ρ_ X).hom ≫ f := by
+    ∀ {X Y : C} (f : X ⟶ Y), f ▷ 𝟙_ _ ≫ (ρ_ Y).hom = (ρ_ X).hom ≫ f := by
     aesop_cat
   /--
   The pentagon identity relating the isomorphism between `X ⊗ (Y ⊗ (Z ⊗ W))` and `((X ⊗ Y) ⊗ Z) ⊗ W`
   -/
   pentagon :
     ∀ W X Y Z : C,
-      ((α_ W X Y).hom ⊗ 𝟙 Z) ≫ (α_ W (X ⊗ Y) Z).hom ≫ (𝟙 W ⊗ (α_ X Y Z).hom) =
+      (α_ W X Y).hom ▷ Z ≫ (α_ W (X ⊗ Y) Z).hom ≫ W ◁ (α_ X Y Z).hom =
         (α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom := by
     aesop_cat
   /--
-  The identity relating the isomorphisms between `X ⊗ (𝟙_C ⊗ Y)`, `(X ⊗ 𝟙_C) ⊗ Y` and `X ⊗ Y`
+  The identity relating the isomorphisms between `X ⊗ (𝟙_ C ⊗ Y)`, `(X ⊗ 𝟙_ C) ⊗ Y` and `X ⊗ Y`
   -/
   triangle :
-    ∀ X Y : C, (α_ X (𝟙_ _) Y).hom ≫ (𝟙 X ⊗ (λ_ Y).hom) = ((ρ_ X).hom ⊗ 𝟙 Y) := by
+    ∀ X Y : C, (α_ X (𝟙_ _) Y).hom ≫ X ◁ (λ_ Y).hom = (ρ_ X).hom ▷ Y := by
     aesop_cat
 #align category_theory.monoidal_category CategoryTheory.MonoidalCategory
 
 attribute [reassoc] MonoidalCategory.tensorHom_def
 attribute [reassoc, simp] MonoidalCategory.whiskerLeft_id
 attribute [reassoc, simp] MonoidalCategory.id_whiskerRight
-attribute [simp] MonoidalCategory.tensor_id
 attribute [reassoc] MonoidalCategory.tensor_comp
 attribute [simp] MonoidalCategory.tensor_comp
 attribute [reassoc] MonoidalCategory.associator_naturality
@@ -221,12 +220,12 @@ namespace MonoidalCategory
 
 variable {C : Type u} [𝒞 : Category.{v} C] [MonoidalCategory C]
 
--- Note: this will be a simp lemma after merging #6307.
+@[simp]
 theorem id_tensorHom (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂) :
     𝟙 X ⊗ f = X ◁ f := by
   simp [tensorHom_def]
 
--- Note: this will be a simp lemma after merging #6307.
+@[simp]
 theorem tensorHom_id {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) :
     f ⊗ 𝟙 Y = f ▷ Y := by
   simp [tensorHom_def]
@@ -240,6 +239,7 @@ theorem whiskerLeft_comp (W : C) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
 theorem id_whiskerLeft {X Y : C} (f : X ⟶ Y) :
     𝟙_ C ◁ f = (λ_ X).hom ≫ f ≫ (λ_ Y).inv := by
   intros; rw [← assoc, ← leftUnitor_naturality]; simp [id_tensorHom]
+#align category_theory.monoidal_category.left_unitor_conjugation CategoryTheory.MonoidalCategory.id_whiskerLeft
 
 @[reassoc, simp]
 theorem tensor_whiskerLeft (X Y : C) {Z Z' : C} (f : Z ⟶ Z') :
@@ -258,6 +258,7 @@ theorem comp_whiskerRight {W X Y : C} (f : W ⟶ X) (g : X ⟶ Y) (Z : C) :
 theorem whiskerRight_id {X Y : C} (f : X ⟶ Y) :
     f ▷ 𝟙_ C = (ρ_ X).hom ≫ f ≫ (ρ_ Y).inv := by
    intros; rw [← assoc, ← rightUnitor_naturality]; simp [tensorHom_id]
+#align category_theory.monoidal_category.right_unitor_conjugation CategoryTheory.MonoidalCategory.whiskerRight_id
 
 @[reassoc, simp]
 theorem whiskerRight_tensor {X X' : C} (f : X ⟶ X') (Y Z : C) :
@@ -492,13 +493,9 @@ theorem tensor_whiskerLeft_symm (X Y : C) {Z Z' : C} (f : Z ⟶ Z') :
     X ◁ Y ◁ f = (α_ X Y Z).inv ≫ (X ⊗ Y) ◁ f ≫ (α_ X Y Z').hom := by simp
 
 @[reassoc]
-theorem leftUnitor_naturality' {X Y : C} (f : X ⟶ Y) :
-    (𝟙_ C) ◁ f ≫ (λ_ Y).hom = (λ_ X).hom ≫ f := by
-  simp
-
-@[reassoc]
-theorem leftUnitor_inv_naturality' {X Y : C} (f : X ⟶ Y) :
+theorem leftUnitor_inv_naturality {X Y : C} (f : X ⟶ Y) :
     f ≫ (λ_ Y).inv = (λ_ X).inv ≫ _ ◁ f := by simp
+#align category_theory.monoidal_category.left_unitor_inv_naturality CategoryTheory.MonoidalCategory.leftUnitor_inv_naturality
 
 @[reassoc]
 theorem id_whiskerLeft_symm {X X' : C} (f : X ⟶ X') :
@@ -506,13 +503,9 @@ theorem id_whiskerLeft_symm {X X' : C} (f : X ⟶ X') :
   simp only [id_whiskerLeft, assoc, inv_hom_id, comp_id, inv_hom_id_assoc]
 
 @[reassoc]
-theorem rightUnitor_naturality' {X Y : C} (f : X ⟶ Y) :
-    f ▷ (𝟙_ C) ≫ (ρ_ Y).hom = (ρ_ X).hom ≫ f := by
-  simp
-
-@[reassoc]
-theorem rightUnitor_inv_naturality' {X X' : C} (f : X ⟶ X') :
+theorem rightUnitor_inv_naturality {X X' : C} (f : X ⟶ X') :
     f ≫ (ρ_ X').inv = (ρ_ X).inv ≫ f ▷ _ := by simp
+#align category_theory.monoidal_category.right_unitor_inv_naturality CategoryTheory.MonoidalCategory.rightUnitor_inv_naturality
 
 @[reassoc]
 theorem whiskerRight_id_symm {X Y : C} (f : X ⟶ Y) :
@@ -529,16 +522,11 @@ but we prove them directly as they are used in proving the coherence theorem. -/
 section
 
 @[reassoc (attr := simp)]
-theorem pentagon' (W X Y Z : C) :
-    (α_ W X Y).hom ▷ Z ≫ (α_ W (X ⊗ Y) Z).hom ≫ W ◁ (α_ X Y Z).hom =
-      (α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom := by
-  simp [← id_tensorHom, ← tensorHom_id, pentagon]
-
-@[reassoc (attr := simp)]
-theorem pentagon_inv' :
+theorem pentagon_inv :
     W ◁ (α_ X Y Z).inv ≫ (α_ W (X ⊗ Y) Z).inv ≫ (α_ W X Y).inv ▷ Z =
       (α_ W X (Y ⊗ Z)).inv ≫ (α_ (W ⊗ X) Y Z).inv :=
   eq_of_inv_eq_inv (by simp)
+#align category_theory.monoidal_category.pentagon_inv CategoryTheory.MonoidalCategory.pentagon_inv
 
 @[reassoc (attr := simp)]
 theorem pentagon_inv_inv_hom_hom_inv :
@@ -591,24 +579,22 @@ theorem pentagon_inv_inv_hom_inv_inv :
   eq_of_inv_eq_inv (by simp)
 
 @[reassoc (attr := simp)]
-theorem triangle' (X Y : C) :
-    (α_ X (𝟙_ C) Y).hom ≫ X ◁ (λ_ Y).hom = (ρ_ X).hom ▷ Y := by
-  simp [← id_tensorHom, ← tensorHom_id, triangle]
-
-@[reassoc (attr := simp)]
-theorem triangle_assoc_comp_right' (X Y : C) :
+theorem triangle_assoc_comp_right (X Y : C) :
     (α_ X (𝟙_ C) Y).inv ≫ ((ρ_ X).hom ▷ Y) = X ◁ (λ_ Y).hom := by
-  rw [← triangle', Iso.inv_hom_id_assoc]
+  rw [← triangle, Iso.inv_hom_id_assoc]
+#align category_theory.monoidal_category.triangle_assoc_comp_right CategoryTheory.MonoidalCategory.triangle_assoc_comp_right
 
 @[reassoc (attr := simp)]
-theorem triangle_assoc_comp_right_inv' (X Y : C) :
+theorem triangle_assoc_comp_right_inv (X Y : C) :
     (ρ_ X).inv ▷ Y ≫ (α_ X (𝟙_ C) Y).hom = X ◁ (λ_ Y).inv := by
   simp [← cancel_mono (X ◁ (λ_ Y).hom)]
+#align category_theory.monoidal_category.triangle_assoc_comp_right_inv CategoryTheory.MonoidalCategory.triangle_assoc_comp_right_inv
 
 @[reassoc (attr := simp)]
-theorem triangle_assoc_comp_left_inv' (X Y : C) :
+theorem triangle_assoc_comp_left_inv (X Y : C) :
     (X ◁ (λ_ Y).inv) ≫ (α_ X (𝟙_ C) Y).inv = (ρ_ X).inv ▷ Y := by
   simp [← cancel_mono ((ρ_ X).hom ▷ Y)]
+#align category_theory.monoidal_category.triangle_assoc_comp_left_inv CategoryTheory.MonoidalCategory.triangle_assoc_comp_left_inv
 
 /-- We state it as a simp lemma, which is regarded as an involved version of
 `id_whiskerRight X Y : 𝟙 X ▷ Y = 𝟙 (X ⊗ Y)`.
@@ -617,8 +603,8 @@ theorem triangle_assoc_comp_left_inv' (X Y : C) :
 theorem leftUnitor_whiskerRight (X Y : C) :
     (λ_ X).hom ▷ Y = (α_ (𝟙_ C) X Y).hom ≫ (λ_ (X ⊗ Y)).hom := by
   rw [← whiskerLeft_iff, whiskerLeft_comp, ← cancel_epi (α_ _ _ _).hom, ←
-      cancel_epi ((α_ _ _ _).hom ▷ _), pentagon'_assoc, triangle', ← associator_naturality_middle, ←
-      comp_whiskerRight_assoc, triangle', associator_naturality_left]
+      cancel_epi ((α_ _ _ _).hom ▷ _), pentagon_assoc, triangle, ← associator_naturality_middle, ←
+      comp_whiskerRight_assoc, triangle, associator_naturality_left]
 
 @[reassoc, simp]
 theorem leftUnitor_inv_whiskerRight (X Y : C) :
@@ -629,8 +615,8 @@ theorem leftUnitor_inv_whiskerRight (X Y : C) :
 theorem whiskerLeft_rightUnitor (X Y : C) :
     X ◁ (ρ_ Y).hom = (α_ X Y (𝟙_ C)).inv ≫ (ρ_ (X ⊗ Y)).hom := by
   rw [← whiskerRight_iff, comp_whiskerRight, ← cancel_epi (α_ _ _ _).inv, ←
-      cancel_epi (X ◁ (α_ _ _ _).inv), pentagon_inv'_assoc, triangle_assoc_comp_right', ←
-      associator_inv_naturality_middle, ← whiskerLeft_comp_assoc, triangle_assoc_comp_right',
+      cancel_epi (X ◁ (α_ _ _ _).inv), pentagon_inv_assoc, triangle_assoc_comp_right, ←
+      associator_inv_naturality_middle, ← whiskerLeft_comp_assoc, triangle_assoc_comp_right,
       associator_inv_naturality_right]
 
 @[reassoc, simp]
@@ -639,20 +625,22 @@ theorem whiskerLeft_rightUnitor_inv (X Y : C) :
   eq_of_inv_eq_inv (by simp)
 
 @[reassoc]
-theorem leftUnitor_tensor' (X Y : C) :
+theorem leftUnitor_tensor (X Y : C) :
     (λ_ (X ⊗ Y)).hom = (α_ (𝟙_ C) X Y).inv ≫ (λ_ X).hom ▷ Y := by simp
 
 @[reassoc]
-theorem leftUnitor_tensor_inv' (X Y : C) :
+theorem leftUnitor_tensor_inv (X Y : C) :
     (λ_ (X ⊗ Y)).inv = (λ_ X).inv ▷ Y ≫ (α_ (𝟙_ C) X Y).hom := by simp
 
 @[reassoc]
-theorem rightUnitor_tensor' (X Y : C) :
+theorem rightUnitor_tensor (X Y : C) :
     (ρ_ (X ⊗ Y)).hom = (α_ X Y (𝟙_ C)).hom ≫ X ◁ (ρ_ Y).hom := by simp
+#align category_theory.monoidal_category.right_unitor_tensor CategoryTheory.MonoidalCategory.rightUnitor_tensor
 
 @[reassoc]
-theorem rightUnitor_tensor_inv' (X Y : C) :
+theorem rightUnitor_tensor_inv (X Y : C) :
     (ρ_ (X ⊗ Y)).inv = X ◁ (ρ_ Y).inv ≫ (α_ X Y (𝟙_ C)).inv := by simp
+#align category_theory.monoidal_category.right_unitor_tensor_inv CategoryTheory.MonoidalCategory.rightUnitor_tensor_inv
 
 end
 
@@ -782,22 +770,12 @@ abbrev ofTensorHom [MonoidalCategoryStruct C]
   pentagon := by intros; simp [← id_tensorHom, ← tensorHom_id, pentagon]
   triangle := by intros; simp [← id_tensorHom, ← tensorHom_id, triangle]
 
-section
-
-/- The lemmas of this section might be redundant because they should be stated in terms of the
-whiskering operators. We leave them in order not to break proofs that existed before we
-have the whiskering operators. -/
-
-/- TODO: The lemmas in this section are no longer simp lemmas after we set `id_tensorHom`
-and `tensorHom_id` as simp lemmas. -/
-attribute [local simp] id_tensorHom tensorHom_id
-
-@[reassoc, simp]
+@[reassoc]
 theorem comp_tensor_id (f : W ⟶ X) (g : X ⟶ Y) : f ≫ g ⊗ 𝟙 Z = (f ⊗ 𝟙 Z) ≫ (g ⊗ 𝟙 Z) := by
   simp
 #align category_theory.monoidal_category.comp_tensor_id CategoryTheory.MonoidalCategory.comp_tensor_id
 
-@[reassoc, simp]
+@[reassoc]
 theorem id_tensor_comp (f : W ⟶ X) (g : X ⟶ Y) : 𝟙 Z ⊗ f ≫ g = (𝟙 Z ⊗ f) ≫ (𝟙 Z ⊗ g) := by
   simp
 #align category_theory.monoidal_category.id_tensor_comp CategoryTheory.MonoidalCategory.id_tensor_comp
@@ -820,63 +798,6 @@ theorem tensor_left_iff {X Y : C} (f g : X ⟶ Y) : 𝟙 (𝟙_ C) ⊗ f = 𝟙
 theorem tensor_right_iff {X Y : C} (f g : X ⟶ Y) : f ⊗ 𝟙 (𝟙_ C) = g ⊗ 𝟙 (𝟙_ C) ↔ f = g := by simp
 #align category_theory.monoidal_category.tensor_right_iff CategoryTheory.MonoidalCategory.tensor_right_iff
 
-@[reassoc]
-theorem pentagon_inv (W X Y Z : C) :
-    (𝟙 W ⊗ (α_ X Y Z).inv) ≫ (α_ W (X ⊗ Y) Z).inv ≫ ((α_ W X Y).inv ⊗ 𝟙 Z) =
-      (α_ W X (Y ⊗ Z)).inv ≫ (α_ (W ⊗ X) Y Z).inv :=
-  CategoryTheory.eq_of_inv_eq_inv (by simp [pentagon])
-#align category_theory.monoidal_category.pentagon_inv CategoryTheory.MonoidalCategory.pentagon_inv
-
-@[reassoc]
-theorem rightUnitor_tensor (X Y : C) :
-    (ρ_ (X ⊗ Y)).hom = (α_ X Y (𝟙_ C)).hom ≫ (𝟙 X ⊗ (ρ_ Y).hom) := by
-  simp
-#align category_theory.monoidal_category.right_unitor_tensor CategoryTheory.MonoidalCategory.rightUnitor_tensor
-
-@[reassoc]
-theorem rightUnitor_tensor_inv (X Y : C) :
-    (ρ_ (X ⊗ Y)).inv = (𝟙 X ⊗ (ρ_ Y).inv) ≫ (α_ X Y (𝟙_ C)).inv :=
-  eq_of_inv_eq_inv (by simp)
-#align category_theory.monoidal_category.right_unitor_tensor_inv CategoryTheory.MonoidalCategory.rightUnitor_tensor_inv
-
-@[reassoc (attr := simp)]
-theorem triangle_assoc_comp_right (X Y : C) :
-    (α_ X (𝟙_ C) Y).inv ≫ ((ρ_ X).hom ⊗ 𝟙 Y) = 𝟙 X ⊗ (λ_ Y).hom := by
-  simp
-#align category_theory.monoidal_category.triangle_assoc_comp_right CategoryTheory.MonoidalCategory.triangle_assoc_comp_right
-
-@[reassoc (attr := simp)]
-theorem triangle_assoc_comp_left_inv (X Y : C) :
-    (𝟙 X ⊗ (λ_ Y).inv) ≫ (α_ X (𝟙_ C) Y).inv = (ρ_ X).inv ⊗ 𝟙 Y := by
-  simp
-#align category_theory.monoidal_category.triangle_assoc_comp_left_inv CategoryTheory.MonoidalCategory.triangle_assoc_comp_left_inv
-
-@[reassoc]
-theorem rightUnitor_conjugation {X Y : C} (f : X ⟶ Y) :
-    f ⊗ 𝟙 (𝟙_ C) = (ρ_ X).hom ≫ f ≫ (ρ_ Y).inv := by
-  simp
-#align category_theory.monoidal_category.right_unitor_conjugation CategoryTheory.MonoidalCategory.rightUnitor_conjugation
-
-@[reassoc]
-theorem leftUnitor_conjugation {X Y : C} (f : X ⟶ Y) :
-    𝟙 (𝟙_ C) ⊗ f = (λ_ X).hom ≫ f ≫ (λ_ Y).inv := by
-  simp
-#align category_theory.monoidal_category.left_unitor_conjugation CategoryTheory.MonoidalCategory.leftUnitor_conjugation
-
-@[reassoc]
-theorem leftUnitor_inv_naturality {X X' : C} (f : X ⟶ X') :
-    f ≫ (λ_ X').inv = (λ_ X).inv ≫ (𝟙 _ ⊗ f) := by
-  simp
-#align category_theory.monoidal_category.left_unitor_inv_naturality CategoryTheory.MonoidalCategory.leftUnitor_inv_naturality
-
-@[reassoc]
-theorem rightUnitor_inv_naturality {X X' : C} (f : X ⟶ X') :
-    f ≫ (ρ_ X').inv = (ρ_ X).inv ≫ (f ⊗ 𝟙 _) := by
-  simp
-#align category_theory.monoidal_category.right_unitor_inv_naturality CategoryTheory.MonoidalCategory.rightUnitor_inv_naturality
-
-end
-
 end
 
 section
@@ -961,7 +882,7 @@ def leftUnitorNatIso : tensorUnitLeft C ≅ 𝟭 C :=
       apply MonoidalCategory.leftUnitor)
     (by
       intros
-      apply MonoidalCategory.leftUnitor_naturality')
+      apply MonoidalCategory.leftUnitor_naturality)
 #align category_theory.monoidal_category.left_unitor_nat_iso CategoryTheory.MonoidalCategory.leftUnitorNatIso
 
 -- Porting Note: same as above
@@ -974,12 +895,12 @@ def rightUnitorNatIso : tensorUnitRight C ≅ 𝟭 C :=
       apply MonoidalCategory.rightUnitor)
     (by
       intros
-      apply MonoidalCategory.rightUnitor_naturality')
+      apply MonoidalCategory.rightUnitor_naturality)
 #align category_theory.monoidal_category.right_unitor_nat_iso CategoryTheory.MonoidalCategory.rightUnitorNatIso
 
 section
 
-attribute [local simp] id_tensorHom tensorHom_id whisker_exchange
+attribute [local simp] whisker_exchange
 
 -- Porting Note: This used to be `variable {C}` but it seems like Lean 4 parses that differently
 variable {C : Type u} [Category.{v} C] [MonoidalCategory.{v} C]
diff --git a/Mathlib/CategoryTheory/Monoidal/Center.lean b/Mathlib/CategoryTheory/Monoidal/Center.lean
index e3c033311bac54..fe7451784d68b9 100644
--- a/Mathlib/CategoryTheory/Monoidal/Center.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Center.lean
@@ -217,8 +217,6 @@ def tensorHom {X₁ Y₁ X₂ Y₂ : Center C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶
 
 section
 
-attribute [local simp] id_tensorHom tensorHom_id
-
 /-- Auxiliary definition for the `MonoidalCategory` instance on `Center C`. -/
 @[simps]
 def tensorUnit : Center C :=
diff --git a/Mathlib/CategoryTheory/Monoidal/CoherenceLemmas.lean b/Mathlib/CategoryTheory/Monoidal/CoherenceLemmas.lean
index 976570b1031bf5..0b0311b5706705 100644
--- a/Mathlib/CategoryTheory/Monoidal/CoherenceLemmas.lean
+++ b/Mathlib/CategoryTheory/Monoidal/CoherenceLemmas.lean
@@ -33,15 +33,15 @@ theorem leftUnitor_tensor'' (X Y : C) :
 #align category_theory.monoidal_category.left_unitor_tensor' CategoryTheory.MonoidalCategory.leftUnitor_tensor''
 
 @[reassoc]
-theorem leftUnitor_tensor (X Y : C) :
+theorem leftUnitor_tensor' (X Y : C) :
     (λ_ (X ⊗ Y)).hom = (α_ (𝟙_ C) X Y).inv ≫ ((λ_ X).hom ⊗ 𝟙 Y) := by
   coherence
-#align category_theory.monoidal_category.left_unitor_tensor CategoryTheory.MonoidalCategory.leftUnitor_tensor
+#align category_theory.monoidal_category.left_unitor_tensor CategoryTheory.MonoidalCategory.leftUnitor_tensor'
 
 @[reassoc]
-theorem leftUnitor_tensor_inv (X Y : C) :
+theorem leftUnitor_tensor_inv' (X Y : C) :
     (λ_ (X ⊗ Y)).inv = ((λ_ X).inv ⊗ 𝟙 Y) ≫ (α_ (𝟙_ C) X Y).hom := by coherence
-#align category_theory.monoidal_category.left_unitor_tensor_inv CategoryTheory.MonoidalCategory.leftUnitor_tensor_inv
+#align category_theory.monoidal_category.left_unitor_tensor_inv CategoryTheory.MonoidalCategory.leftUnitor_tensor_inv'
 
 @[reassoc]
 theorem id_tensor_rightUnitor_inv (X Y : C) : 𝟙 X ⊗ (ρ_ Y).inv = (ρ_ _).inv ≫ (α_ _ _ _).hom := by
@@ -60,12 +60,6 @@ theorem pentagon_inv_inv_hom (W X Y Z : C) :
   coherence
 #align category_theory.monoidal_category.pentagon_inv_inv_hom CategoryTheory.MonoidalCategory.pentagon_inv_inv_hom
 
-@[reassoc (attr := simp)]
-theorem triangle_assoc_comp_right_inv (X Y : C) :
-    ((ρ_ X).inv ⊗ 𝟙 Y) ≫ (α_ X (𝟙_ C) Y).hom = 𝟙 X ⊗ (λ_ Y).inv := by
-  coherence
-#align category_theory.monoidal_category.triangle_assoc_comp_right_inv CategoryTheory.MonoidalCategory.triangle_assoc_comp_right_inv
-
 theorem unitors_equal : (λ_ (𝟙_ C)).hom = (ρ_ (𝟙_ C)).hom := by
   coherence
 #align category_theory.monoidal_category.unitors_equal CategoryTheory.MonoidalCategory.unitors_equal
diff --git a/Mathlib/CategoryTheory/Monoidal/CommMon_.lean b/Mathlib/CategoryTheory/Monoidal/CommMon_.lean
index a28683acd4a959..c43d20b07abfb6 100644
--- a/Mathlib/CategoryTheory/Monoidal/CommMon_.lean
+++ b/Mathlib/CategoryTheory/Monoidal/CommMon_.lean
@@ -172,8 +172,6 @@ def laxBraidedToCommMon : LaxBraidedFunctor (Discrete PUnit.{u + 1}) C ⥤ CommM
 set_option linter.uppercaseLean3 false in
 #align CommMon_.equiv_lax_braided_functor_punit.lax_braided_to_CommMon CommMon_.EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon
 
-attribute [local simp] id_tensorHom tensorHom_id
-
 /-- Implementation of `CommMon_.equivLaxBraidedFunctorPunit`. -/
 @[simps]
 def commMonToLaxBraided : CommMon_ C ⥤ LaxBraidedFunctor (Discrete PUnit.{u + 1}) C where
diff --git a/Mathlib/CategoryTheory/Monoidal/End.lean b/Mathlib/CategoryTheory/Monoidal/End.lean
index 829147a0e031b8..0b7a7bdf0668c9 100644
--- a/Mathlib/CategoryTheory/Monoidal/End.lean
+++ b/Mathlib/CategoryTheory/Monoidal/End.lean
@@ -90,8 +90,6 @@ attribute [local instance] endofunctorMonoidalCategory
 -- porting note: used `dsimp [endofunctorMonoidalCategory]` when necessary instead
 -- attribute [local reducible] endofunctorMonoidalCategory
 
-attribute [local simp] id_tensorHom tensorHom_id in
-
 /-- Tensoring on the right gives a monoidal functor from `C` into endofunctors of `C`.
 -/
 @[simps!]
@@ -168,23 +166,23 @@ theorem μ_naturality₂ {m n m' n' : M} (f : m ⟶ m') (g : n ⟶ n') (X : C) :
 @[reassoc (attr := simp)]
 theorem μ_naturalityₗ {m n m' : M} (f : m ⟶ m') (X : C) :
     (F.obj n).map ((F.map f).app X) ≫ (F.μ m' n).app X =
-      (F.μ m n).app X ≫ (F.map (f ⊗ 𝟙 n)).app X := by
-  rw [← μ_naturality₂ F f (𝟙 n) X]
+      (F.μ m n).app X ≫ (F.map (f ▷ n)).app X := by
+  rw [← tensorHom_id, ← μ_naturality₂ F f (𝟙 n) X]
   simp
 #align category_theory.μ_naturalityₗ CategoryTheory.μ_naturalityₗ
 
 @[reassoc (attr := simp)]
 theorem μ_naturalityᵣ {m n n' : M} (g : n ⟶ n') (X : C) :
     (F.map g).app ((F.obj m).obj X) ≫ (F.μ m n').app X =
-      (F.μ m n).app X ≫ (F.map (𝟙 m ⊗ g)).app X := by
-  rw [← μ_naturality₂ F (𝟙 m) g X]
+      (F.μ m n).app X ≫ (F.map (m ◁ g)).app X := by
+  rw [← id_tensorHom, ← μ_naturality₂ F (𝟙 m) g X]
   simp
 #align category_theory.μ_naturalityᵣ CategoryTheory.μ_naturalityᵣ
 
 @[reassoc (attr := simp)]
 theorem μ_inv_naturalityₗ {m n m' : M} (f : m ⟶ m') (X : C) :
     (F.μIso m n).inv.app X ≫ (F.obj n).map ((F.map f).app X) =
-      (F.map (f ⊗ 𝟙 n)).app X ≫ (F.μIso m' n).inv.app X := by
+      (F.map (f ▷ n)).app X ≫ (F.μIso m' n).inv.app X := by
   rw [← IsIso.comp_inv_eq, Category.assoc, ← IsIso.eq_inv_comp]
   simp
 #align category_theory.μ_inv_naturalityₗ CategoryTheory.μ_inv_naturalityₗ
@@ -192,7 +190,7 @@ theorem μ_inv_naturalityₗ {m n m' : M} (f : m ⟶ m') (X : C) :
 @[reassoc (attr := simp)]
 theorem μ_inv_naturalityᵣ {m n n' : M} (g : n ⟶ n') (X : C) :
     (F.μIso m n).inv.app X ≫ (F.map g).app ((F.obj m).obj X) =
-      (F.map (𝟙 m ⊗ g)).app X ≫ (F.μIso m n').inv.app X := by
+      (F.map (m ◁ g)).app X ≫ (F.μIso m n').inv.app X := by
   rw [← IsIso.comp_inv_eq, Category.assoc, ← IsIso.eq_inv_comp]
   simp
 #align category_theory.μ_inv_naturalityᵣ CategoryTheory.μ_inv_naturalityᵣ
@@ -317,7 +315,7 @@ noncomputable def unitOfTensorIsoUnit (m n : M) (h : m ⊗ n ≅ 𝟙_ M) : F.ob
   then `F.obj m` and `F.obj n` forms a self-equivalence of `C`. -/
 @[simps]
 noncomputable def equivOfTensorIsoUnit (m n : M) (h₁ : m ⊗ n ≅ 𝟙_ M) (h₂ : n ⊗ m ≅ 𝟙_ M)
-    (H : (h₁.hom ⊗ 𝟙 m) ≫ (λ_ m).hom = (α_ m n m).hom ≫ (𝟙 m ⊗ h₂.hom) ≫ (ρ_ m).hom) : C ≌ C
+    (H : h₁.hom ▷ m ≫ (λ_ m).hom = (α_ m n m).hom ≫ m ◁ h₂.hom ≫ (ρ_ m).hom) : C ≌ C
     where
   functor := F.obj m
   inverse := F.obj n
diff --git a/Mathlib/CategoryTheory/Monoidal/Free/Basic.lean b/Mathlib/CategoryTheory/Monoidal/Free/Basic.lean
index 432c9356b3d345..a42bdd6f687ee9 100644
--- a/Mathlib/CategoryTheory/Monoidal/Free/Basic.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Free/Basic.lean
@@ -314,17 +314,21 @@ def projectMap (X Y : F C) : (X ⟶ Y) → (projectObj f X ⟶ projectObj f Y) :
     | ρ_hom_inv => dsimp only [projectMapAux]; rw [Iso.hom_inv_id]
     | ρ_inv_hom => dsimp only [projectMapAux]; rw [Iso.inv_hom_id]
     | ρ_naturality =>
-        dsimp only [projectMapAux, projectObj]; rw [MonoidalCategory.rightUnitor_naturality]
+        dsimp only [projectMapAux, projectObj]
+        rw [tensorHom_id, MonoidalCategory.rightUnitor_naturality]
     | l_hom_inv => dsimp only [projectMapAux]; rw [Iso.hom_inv_id]
     | l_inv_hom => dsimp only [projectMapAux]; rw [Iso.inv_hom_id]
     | l_naturality =>
         dsimp only [projectMapAux, projectObj]
+        rw [id_tensorHom]
         exact MonoidalCategory.leftUnitor_naturality _
     | pentagon =>
         dsimp only [projectMapAux]
+        simp only [tensorHom_id, id_tensorHom]
         exact MonoidalCategory.pentagon _ _ _ _
     | triangle =>
         dsimp only [projectMapAux]
+        simp only [tensorHom_id, id_tensorHom]
         exact MonoidalCategory.triangle _ _
 #align category_theory.free_monoidal_category.project_map CategoryTheory.FreeMonoidalCategory.projectMap
 
@@ -345,12 +349,14 @@ def project : MonoidalFunctor (F C) D where
     induction' f using Quotient.recOn
     · dsimp
       simp
+      rw [← tensorHom_id, ← tensorHom_id]
       rfl
     · rfl
   μ_natural_right := fun _ f => by
     induction' f using Quotient.recOn
     · dsimp
       simp
+      rw [← id_tensorHom, ← id_tensorHom]
       rfl
     · rfl
 #align category_theory.free_monoidal_category.project CategoryTheory.FreeMonoidalCategory.project
diff --git a/Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean b/Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean
index 3e58a9cc321eb8..e78af703e3fdd2 100644
--- a/Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean
@@ -163,7 +163,7 @@ def fullNormalize : F C ⥤ N C where
 @[simp]
 def tensorFunc : F C ⥤ N C ⥤ F C where
   obj X := Discrete.functor fun n => inclusion.obj ⟨n⟩ ⊗ X
-  map f := Discrete.natTrans (fun n => 𝟙 _ ⊗ f)
+  map f := Discrete.natTrans (fun n => _ ◁ f)
 #align category_theory.free_monoidal_category.tensor_func CategoryTheory.FreeMonoidalCategory.tensorFunc
 
 theorem tensorFunc_map_app {X Y : F C} (f : X ⟶ Y) (n) : ((tensorFunc C).map f).app n = 𝟙 _ ⊗ f :=
@@ -171,7 +171,7 @@ theorem tensorFunc_map_app {X Y : F C} (f : X ⟶ Y) (n) : ((tensorFunc C).map f
 #align category_theory.free_monoidal_category.tensor_func_map_app CategoryTheory.FreeMonoidalCategory.tensorFunc_map_app
 
 theorem tensorFunc_obj_map (Z : F C) {n n' : N C} (f : n ⟶ n') :
-    ((tensorFunc C).obj Z).map f = inclusion.map f ⊗ 𝟙 Z := by
+    ((tensorFunc C).obj Z).map f = inclusion.map f ▷ Z := by
   cases n
   cases n'
   rcases f with ⟨⟨h⟩⟩
@@ -251,42 +251,43 @@ def normalizeIso : tensorFunc C ≅ normalize' C :=
           Category.comp_id]
         simp only [← Category.assoc]
         congr 4
-        simp only [Category.assoc, ← cancel_epi (𝟙 (inclusionObj n.as) ⊗ (α_ X₁ X₂ X₃).inv),
-          tensor_inv_hom_id_assoc, tensor_id, Category.id_comp,
-          pentagon_inv_assoc (inclusionObj n.as) X₁ X₂ X₃, Iso.inv_hom_id, Category.comp_id]
+        rw [← cancel_epi ((inclusionObj n.as) ◁ (α_ X₁ X₂ X₃).inv)]
+        simp
       · ext n
         dsimp
         rw [mk_α_inv, NatTrans.comp_app, NatTrans.comp_app]
         dsimp [NatIso.ofComponents, normalizeMapAux, whiskeringRight, whiskerRight, Functor.comp]
-        simp only [Category.assoc, comp_tensor_id, tensor_id, Category.comp_id,
-          pentagon_inv_assoc, ← associator_inv_naturality_assoc]
-        rfl
+        simp [tensorHom_id, comp_whiskerRight, Category.assoc, pentagon_inv_assoc,
+          whiskerRight_tensor, Category.comp_id, Iso.cancel_iso_inv_left]
+        erw [Iso.hom_inv_id_assoc]
       · ext n
         dsimp [Functor.comp]
         rw [mk_l_hom, NatTrans.comp_app, NatTrans.comp_app]
         dsimp [NatIso.ofComponents, normalizeMapAux, whiskeringRight, whiskerRight, Functor.comp]
-        simp only [triangle_assoc_comp_right_assoc, Category.assoc, Category.comp_id]
+        simp only [tensorHom_id, triangle_assoc_comp_right_assoc, Category.comp_id]
         rfl
       · ext n
         dsimp [Functor.comp]
         rw [mk_l_inv, NatTrans.comp_app, NatTrans.comp_app]
         dsimp [NatIso.ofComponents, normalizeMapAux, whiskeringRight, whiskerRight, Functor.comp]
-        simp only [triangle_assoc_comp_right_assoc, tensor_inv_hom_id_assoc, tensor_id,
-          Category.id_comp, Category.comp_id]
+        simp only [tensorHom_id, triangle_assoc_comp_right_assoc, whiskerLeft_inv_hom_assoc,
+          Category.comp_id]
         rfl
       · ext n
         dsimp
         rw [mk_ρ_hom, NatTrans.comp_app, NatTrans.comp_app]
         dsimp [NatIso.ofComponents, normalizeMapAux, whiskeringRight, whiskerRight, Functor.comp]
-        simp only [← (Iso.inv_comp_eq _).2 (rightUnitor_tensor _ _), Category.assoc,
-          ← rightUnitor_naturality, Category.comp_id]; rfl
+        simp only [whiskerLeft_rightUnitor, Category.assoc, tensorHom_id,
+          MonoidalCategory.whiskerRight_id, Category.comp_id, Iso.cancel_iso_inv_left,
+          Iso.cancel_iso_hom_left]
+        erw [Iso.inv_hom_id, Category.comp_id]
       · ext n
         dsimp
         rw [mk_ρ_inv, NatTrans.comp_app, NatTrans.comp_app]
         dsimp [NatIso.ofComponents, normalizeMapAux, whiskeringRight, whiskerRight, Functor.comp]
-        simp only [← (Iso.eq_comp_inv _).1 (rightUnitor_tensor_inv _ _), rightUnitor_conjugation,
-          Category.assoc, Iso.hom_inv_id_assoc, Iso.inv_hom_id_assoc, Iso.inv_hom_id,
-          Discrete.functor, Category.comp_id, Function.comp]
+        simp only [whiskerLeft_rightUnitor_inv, tensorHom_id, MonoidalCategory.whiskerRight_id,
+          Category.assoc, Iso.hom_inv_id_assoc, Iso.inv_hom_id_assoc, Category.comp_id]
+        erw [Iso.inv_hom_id, Category.comp_id]
       · rw [mk_comp, Functor.map_comp, Functor.map_comp, Category.assoc, h₂, reassoc_of% h₁]
       · ext ⟨n⟩
         replace h₁ := NatTrans.congr_app h₁ ⟨n⟩
@@ -301,6 +302,7 @@ def normalizeIso : tensorFunc C ≅ normalize' C :=
         rw [NatTrans.comp_app, NatTrans.comp_app] at h₁ h₂ ⊢
         dsimp [NatIso.ofComponents, normalizeMapAux, whiskeringRight, whiskerRight,
           Functor.comp, Discrete.natTrans] at h₁ h₂ h₃ ⊢
+        simp only [← id_tensorHom, ← tensorHom_id] at h₁ ⊢
         rw [mk_tensor, associator_inv_naturality_assoc, ← tensor_comp_assoc, h₁,
           Category.assoc, Category.comp_id, ← @Category.id_comp (F C) _ _ _ (@Quotient.mk _ _ g),
           tensor_comp, Category.assoc, Category.assoc, Functor.map_comp]
diff --git a/Mathlib/CategoryTheory/Monoidal/Functor.lean b/Mathlib/CategoryTheory/Monoidal/Functor.lean
index 45c9319db18c14..3bd441d9404e74 100644
--- a/Mathlib/CategoryTheory/Monoidal/Functor.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Functor.lean
@@ -71,22 +71,22 @@ structure LaxMonoidalFunctor extends C ⥤ D where
   μ : ∀ X Y : C, obj X ⊗ obj Y ⟶ obj (X ⊗ Y)
   μ_natural_left :
     ∀ {X Y : C} (f : X ⟶ Y) (X' : C),
-      (map f ⊗ 𝟙 (obj X')) ≫ μ Y X' = μ X X' ≫ map (f ⊗ 𝟙 X') := by
+      map f ▷ obj X' ≫ μ Y X' = μ X X' ≫ map (f ▷ X') := by
     aesop_cat
   μ_natural_right :
     ∀ {X Y : C} (X' : C) (f : X ⟶ Y) ,
-      (𝟙 (obj X') ⊗ map f) ≫ μ X' Y = μ X' X ≫ map (𝟙 X' ⊗ f) := by
+      obj X' ◁ map f ≫ μ X' Y = μ X' X ≫ map (X' ◁ f) := by
     aesop_cat
   /-- associativity of the tensorator -/
   associativity :
     ∀ X Y Z : C,
-      (μ X Y ⊗ 𝟙 (obj Z)) ≫ μ (X ⊗ Y) Z ≫ map (α_ X Y Z).hom =
-        (α_ (obj X) (obj Y) (obj Z)).hom ≫ (𝟙 (obj X) ⊗ μ Y Z) ≫ μ X (Y ⊗ Z) := by
+      μ X Y ▷ obj Z ≫ μ (X ⊗ Y) Z ≫ map (α_ X Y Z).hom =
+        (α_ (obj X) (obj Y) (obj Z)).hom ≫ obj X ◁ μ Y Z ≫ μ X (Y ⊗ Z) := by
     aesop_cat
   -- unitality
-  left_unitality : ∀ X : C, (λ_ (obj X)).hom = (ε ⊗ 𝟙 (obj X)) ≫ μ (𝟙_ C) X ≫ map (λ_ X).hom :=
+  left_unitality : ∀ X : C, (λ_ (obj X)).hom = ε ▷ obj X ≫ μ (𝟙_ C) X ≫ map (λ_ X).hom :=
     by aesop_cat
-  right_unitality : ∀ X : C, (ρ_ (obj X)).hom = (𝟙 (obj X) ⊗ ε) ≫ μ X (𝟙_ C) ≫ map (ρ_ X).hom :=
+  right_unitality : ∀ X : C, (ρ_ (obj X)).hom = obj X ◁ ε ≫ μ X (𝟙_ C) ≫ map (ρ_ X).hom :=
     by aesop_cat
 #align category_theory.lax_monoidal_functor CategoryTheory.LaxMonoidalFunctor
 
@@ -118,37 +118,7 @@ variable {C D}
 theorem LaxMonoidalFunctor.μ_natural (F : LaxMonoidalFunctor C D) {X Y X' Y' : C}
     (f : X ⟶ Y) (g : X' ⟶ Y') :
       (F.map f ⊗ F.map g) ≫ F.μ Y Y' = F.μ X X' ≫ F.map (f ⊗ g) := by
-  rw [tensorHom_def, ← id_tensorHom, ← tensorHom_id]
-  simp only [assoc, μ_natural_right, μ_natural_left_assoc]
-  rw [← F.map_comp, tensor_id_comp_id_tensor]
-
-@[reassoc (attr := simp)]
-theorem  LaxMonoidalFunctor.associativity' (F : LaxMonoidalFunctor C D) (X Y Z : C) :
-    (F.μ X Y ▷ F.obj Z) ≫ F.μ (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom =
-        (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ ((F.obj X) ◁ F.μ Y Z) ≫ F.μ X (Y ⊗ Z) := by
-  simp [← id_tensorHom, ← tensorHom_id]
-
-@[reassoc]
-theorem  LaxMonoidalFunctor.left_unitality' (F : LaxMonoidalFunctor C D) (X : C) :
-    (λ_ (F.obj X)).hom = (F.ε ▷ F.obj X) ≫ F.μ (𝟙_ C) X ≫ F.map (λ_ X).hom := by
-  simp [← id_tensorHom, ← tensorHom_id]
-
-@[reassoc]
-theorem  LaxMonoidalFunctor.right_unitality' (F : LaxMonoidalFunctor C D) (X : C) :
-    (ρ_ (F.obj X)).hom = (F.obj X ◁ F.ε) ≫ F.μ X (𝟙_ C) ≫ F.map (ρ_ X).hom := by
-  simp [← id_tensorHom, ← tensorHom_id]
-
-@[reassoc (attr := simp)]
-theorem LaxMonoidalFunctor.μ_natural_left' (F : LaxMonoidalFunctor C D)
-    {X Y : C} (f : X ⟶ Y) (X' : C) :
-      F.map f ▷ F.obj X' ≫ F.μ Y X' = F.μ X X' ≫ F.map (f ▷ X') := by
-  simp [← id_tensorHom, ← tensorHom_id]
-
-@[reassoc (attr := simp)]
-theorem LaxMonoidalFunctor.μ_natural_right' (F : LaxMonoidalFunctor C D)
-    {X Y : C} (X' : C) (f : X ⟶ Y) :
-      F.obj X' ◁ F.map f ≫ F.μ X' Y = F.μ X' X ≫ F.map (X' ◁ f) := by
-  simp [← id_tensorHom, ← tensorHom_id]
+  simp [tensorHom_def]
 
 /--
 A constructor for lax monoidal functors whose axioms are described by `tensorHom` instead of
@@ -185,20 +155,20 @@ def LaxMonoidalFunctor.ofTensorHom (F : C ⥤ D)
   ε := ε
   μ := μ
   μ_natural_left := fun f X' => by
-    simp_rw [← F.map_id, μ_natural]
+    simp_rw [← tensorHom_id, ← F.map_id, μ_natural]
   μ_natural_right := fun X' f => by
-    simp_rw [← F.map_id, μ_natural]
+    simp_rw [← id_tensorHom, ← F.map_id, μ_natural]
   associativity := fun X Y Z => by
-    simp_rw [associativity]
+    simp_rw [← tensorHom_id, ← id_tensorHom, associativity]
   left_unitality := fun X => by
-    simp_rw [left_unitality]
+    simp_rw [← tensorHom_id, left_unitality]
   right_unitality := fun X => by
-    simp_rw [right_unitality]
+    simp_rw [← id_tensorHom, right_unitality]
 
 --Porting note: was `[simp, reassoc.1]`
 @[reassoc (attr := simp)]
 theorem LaxMonoidalFunctor.left_unitality_inv (F : LaxMonoidalFunctor C D) (X : C) :
-    (λ_ (F.obj X)).inv ≫ (F.ε ⊗ 𝟙 (F.obj X)) ≫ F.μ (𝟙_ C) X = F.map (λ_ X).inv := by
+    (λ_ (F.obj X)).inv ≫ F.ε ▷ F.obj X ≫ F.μ (𝟙_ C) X = F.map (λ_ X).inv := by
   rw [Iso.inv_comp_eq, F.left_unitality, Category.assoc, Category.assoc, ← F.toFunctor.map_comp,
     Iso.hom_inv_id, F.toFunctor.map_id, comp_id]
 #align category_theory.lax_monoidal_functor.left_unitality_inv CategoryTheory.LaxMonoidalFunctor.left_unitality_inv
@@ -206,7 +176,7 @@ theorem LaxMonoidalFunctor.left_unitality_inv (F : LaxMonoidalFunctor C D) (X :
 --Porting note: was `[simp, reassoc.1]`
 @[reassoc (attr := simp)]
 theorem LaxMonoidalFunctor.right_unitality_inv (F : LaxMonoidalFunctor C D) (X : C) :
-    (ρ_ (F.obj X)).inv ≫ (𝟙 (F.obj X) ⊗ F.ε) ≫ F.μ X (𝟙_ C) = F.map (ρ_ X).inv := by
+    (ρ_ (F.obj X)).inv ≫ F.obj X ◁ F.ε ≫ F.μ X (𝟙_ C) = F.map (ρ_ X).inv := by
   rw [Iso.inv_comp_eq, F.right_unitality, Category.assoc, Category.assoc, ← F.toFunctor.map_comp,
     Iso.hom_inv_id, F.toFunctor.map_id, comp_id]
 #align category_theory.lax_monoidal_functor.right_unitality_inv CategoryTheory.LaxMonoidalFunctor.right_unitality_inv
@@ -214,28 +184,12 @@ theorem LaxMonoidalFunctor.right_unitality_inv (F : LaxMonoidalFunctor C D) (X :
 --Porting note: was `[simp, reassoc.1]`
 @[reassoc (attr := simp)]
 theorem LaxMonoidalFunctor.associativity_inv (F : LaxMonoidalFunctor C D) (X Y Z : C) :
-    (𝟙 (F.obj X) ⊗ F.μ Y Z) ≫ F.μ X (Y ⊗ Z) ≫ F.map (α_ X Y Z).inv =
-      (α_ (F.obj X) (F.obj Y) (F.obj Z)).inv ≫ (F.μ X Y ⊗ 𝟙 (F.obj Z)) ≫ F.μ (X ⊗ Y) Z := by
+    F.obj X ◁ F.μ Y Z ≫ F.μ X (Y ⊗ Z) ≫ F.map (α_ X Y Z).inv =
+      (α_ (F.obj X) (F.obj Y) (F.obj Z)).inv ≫ F.μ X Y ▷ F.obj Z ≫ F.μ (X ⊗ Y) Z := by
   rw [Iso.eq_inv_comp, ← F.associativity_assoc, ← F.toFunctor.map_comp, Iso.hom_inv_id,
     F.toFunctor.map_id, comp_id]
 #align category_theory.lax_monoidal_functor.associativity_inv CategoryTheory.LaxMonoidalFunctor.associativity_inv
 
-@[reassoc (attr := simp)]
-theorem LaxMonoidalFunctor.left_unitality_inv' (F : LaxMonoidalFunctor C D) (X : C) :
-    (λ_ (F.obj X)).inv ≫ (F.ε ▷ F.obj X) ≫ F.μ (𝟙_ C) X = F.map (λ_ X).inv := by
-  simp [← id_tensorHom, ← tensorHom_id]
-
-@[reassoc (attr := simp)]
-theorem LaxMonoidalFunctor.right_unitality_inv' (F : LaxMonoidalFunctor C D) (X : C) :
-    (ρ_ (F.obj X)).inv ≫ (F.obj X ◁ F.ε) ≫ F.μ X (𝟙_ C) = F.map (ρ_ X).inv := by
-  simp [← id_tensorHom, ← tensorHom_id]
-
-@[reassoc (attr := simp)]
-theorem LaxMonoidalFunctor.associativity_inv' (F : LaxMonoidalFunctor C D) (X Y Z : C) :
-    (F.obj X ◁ F.μ Y Z) ≫ F.μ X (Y ⊗ Z) ≫ F.map (α_ X Y Z).inv =
-      (α_ (F.obj X) (F.obj Y) (F.obj Z)).inv ≫ (F.μ X Y ▷ F.obj Z) ≫ F.μ (X ⊗ Y) Z := by
-  simp [← id_tensorHom, ← tensorHom_id]
-
 end
 
 /--
@@ -300,38 +254,35 @@ variable {D : Type u₂} [Category.{v₂} D] [MonoidalCategory.{v₂} D]
 
 variable (F : MonoidalFunctor.{v₁, v₂} C D)
 
+@[reassoc]
 theorem map_tensor {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') :
     F.map (f ⊗ g) = inv (F.μ X X') ≫ (F.map f ⊗ F.map g) ≫ F.μ Y Y' := by simp
 #align category_theory.monoidal_functor.map_tensor CategoryTheory.MonoidalFunctor.map_tensor
 
--- Note: `𝟙 X ⊗ f` will be replaced by `X ◁ f` in #6307.
+@[reassoc]
 theorem map_whiskerLeft (X : C) {Y Z : C} (f : Y ⟶ Z) :
-    F.map (𝟙 X ⊗ f) = inv (F.μ X Y) ≫ (𝟙 (F.obj X) ⊗ F.map f) ≫ F.μ X Z := by simp
-
-theorem map_whiskerLeft' (X : C) {Y Z : C} (f : Y ⟶ Z) :
     F.map (X ◁ f) = inv (F.μ X Y) ≫ F.obj X ◁ F.map f ≫ F.μ X Z := by simp
 
--- Note: `f ⊗ 𝟙 Z` will be replaced by `f ▷ Z` in #6307.
+@[reassoc]
 theorem map_whiskerRight {X Y : C} (f : X ⟶ Y) (Z : C) :
-    F.map (f ⊗ 𝟙 Z) = inv (F.μ X Z) ≫ (F.map f ⊗ 𝟙 (F.obj Z)) ≫ F.μ Y Z := by simp
-
-theorem map_whiskerRight' {X Y : C} (f : X ⟶ Y) (Z : C) :
     F.map (f ▷ Z) = inv (F.μ X Z) ≫ F.map f ▷ F.obj Z ≫ F.μ Y Z := by simp
 
+@[reassoc]
 theorem map_leftUnitor (X : C) :
-    F.map (λ_ X).hom = inv (F.μ (𝟙_ C) X) ≫ (inv F.ε ⊗ 𝟙 (F.obj X)) ≫ (λ_ (F.obj X)).hom := by
+    F.map (λ_ X).hom = inv (F.μ (𝟙_ C) X) ≫ inv F.ε ▷ F.obj X ≫ (λ_ (F.obj X)).hom := by
   simp only [LaxMonoidalFunctor.left_unitality]
   slice_rhs 2 3 =>
-    rw [← comp_tensor_id]
+    rw [← comp_whiskerRight]
     simp
   simp
 #align category_theory.monoidal_functor.map_left_unitor CategoryTheory.MonoidalFunctor.map_leftUnitor
 
+@[reassoc]
 theorem map_rightUnitor (X : C) :
-    F.map (ρ_ X).hom = inv (F.μ X (𝟙_ C)) ≫ (𝟙 (F.obj X) ⊗ inv F.ε) ≫ (ρ_ (F.obj X)).hom := by
+    F.map (ρ_ X).hom = inv (F.μ X (𝟙_ C)) ≫ F.obj X ◁ inv F.ε ≫ (ρ_ (F.obj X)).hom := by
   simp only [LaxMonoidalFunctor.right_unitality]
   slice_rhs 2 3 =>
-    rw [← id_tensor_comp]
+    rw [← MonoidalCategory.whiskerLeft_comp]
     simp
   simp
 #align category_theory.monoidal_functor.map_right_unitor CategoryTheory.MonoidalFunctor.map_rightUnitor
@@ -384,14 +335,14 @@ theorem ε_hom_inv_id : F.ε ≫ F.εIso.inv = 𝟙 _ :=
 @[simps!]
 noncomputable def commTensorLeft (X : C) :
     F.toFunctor ⋙ tensorLeft (F.toFunctor.obj X) ≅ tensorLeft X ⋙ F.toFunctor :=
-  NatIso.ofComponents (fun Y => F.μIso X Y) fun f => F.μ_natural_right' X f
+  NatIso.ofComponents (fun Y => F.μIso X Y) fun f => F.μ_natural_right X f
 #align category_theory.monoidal_functor.comm_tensor_left CategoryTheory.MonoidalFunctor.commTensorLeft
 
 /-- Monoidal functors commute with right tensoring up to isomorphism -/
 @[simps!]
 noncomputable def commTensorRight (X : C) :
     F.toFunctor ⋙ tensorRight (F.toFunctor.obj X) ≅ tensorRight X ⋙ F.toFunctor :=
-  NatIso.ofComponents (fun Y => F.μIso Y X) fun f => F.μ_natural_left' f X
+  NatIso.ofComponents (fun Y => F.μIso Y X) fun f => F.μ_natural_left f X
 #align category_theory.monoidal_functor.comm_tensor_right CategoryTheory.MonoidalFunctor.commTensorRight
 
 end
@@ -440,14 +391,10 @@ def comp : LaxMonoidalFunctor.{v₁, v₃} C E :=
       simp_rw [comp_obj, F.comp_map, μ_natural_right_assoc, assoc, ← G.map_comp, μ_natural_right]
     associativity := fun X Y Z => by
       dsimp
-      rw [id_tensor_comp]
-      slice_rhs 3 4 => rw [← G.toFunctor.map_id, G.μ_natural]
+      simp only [comp_whiskerRight, assoc, μ_natural_left_assoc, MonoidalCategory.whiskerLeft_comp,
+        μ_natural_right_assoc]
       slice_rhs 1 3 => rw [← G.associativity]
-      rw [comp_tensor_id]
-      slice_lhs 2 3 => rw [← G.toFunctor.map_id, G.μ_natural]
-      rw [Category.assoc, Category.assoc, Category.assoc, Category.assoc, Category.assoc, ←
-        G.toFunctor.map_comp, ← G.toFunctor.map_comp, ← G.toFunctor.map_comp, ←
-        G.toFunctor.map_comp, F.associativity] }
+      simp_rw [Category.assoc, ← G.toFunctor.map_comp, F.associativity] }
 #align category_theory.lax_monoidal_functor.comp CategoryTheory.LaxMonoidalFunctor.comp
 
 @[inherit_doc]
@@ -586,43 +533,57 @@ structure as well.
 -/
 @[simp]
 noncomputable def monoidalAdjoint (F : MonoidalFunctor C D) {G : D ⥤ C} (h : F.toFunctor ⊣ G) :
-    LaxMonoidalFunctor D C := LaxMonoidalFunctor.ofTensorHom
-  (F := G)
-  (ε := h.homEquiv _ _ (inv F.ε))
-  (μ := fun X Y ↦
-    h.homEquiv _ (X ⊗ Y) (inv (F.μ (G.obj X) (G.obj Y)) ≫ (h.counit.app X ⊗ h.counit.app Y)))
-  (μ_natural := @fun X Y X' Y' f g => by
-    rw [← h.homEquiv_naturality_left, ← h.homEquiv_naturality_right, Equiv.apply_eq_iff_eq, assoc,
-      IsIso.eq_inv_comp, ← F.toLaxMonoidalFunctor.μ_natural_assoc, IsIso.hom_inv_id_assoc, ←
-      tensor_comp, Adjunction.counit_naturality, Adjunction.counit_naturality, tensor_comp])
-  (associativity := fun X Y Z ↦ by
+    LaxMonoidalFunctor D C where
+  toFunctor := G
+  ε := h.homEquiv _ _ (inv F.ε)
+  μ := fun X Y =>
+    h.homEquiv _ _ (inv (F.μ (G.obj X) (G.obj Y)) ≫ (h.counit.app X ⊗ h.counit.app Y))
+  μ_natural_left {X Y} f X' := by
+    rw [← h.homEquiv_naturality_left, ← h.homEquiv_naturality_right, Equiv.apply_eq_iff_eq,
+      assoc, IsIso.eq_inv_comp,
+      ← F.toLaxMonoidalFunctor.μ_natural_left_assoc, IsIso.hom_inv_id_assoc, tensorHom_def,
+      ← comp_whiskerRight_assoc, Adjunction.counit_naturality, comp_whiskerRight_assoc,
+      ← whisker_exchange, ← tensorHom_def_assoc]
+  μ_natural_right {X Y} X' f := by
+    rw [← h.homEquiv_naturality_left, ← h.homEquiv_naturality_right, Equiv.apply_eq_iff_eq,
+      assoc, IsIso.eq_inv_comp,
+      ← F.toLaxMonoidalFunctor.μ_natural_right_assoc, IsIso.hom_inv_id_assoc, tensorHom_def',
+      ← MonoidalCategory.whiskerLeft_comp_assoc, Adjunction.counit_naturality, whisker_exchange,
+      MonoidalCategory.whiskerLeft_comp, ← tensorHom_def_assoc]
+  associativity X Y Z := by
     dsimp only
-    rw [← h.homEquiv_naturality_right, ← h.homEquiv_naturality_left, ←
-      h.homEquiv_naturality_left, ← h.homEquiv_naturality_left, Equiv.apply_eq_iff_eq, ←
-      cancel_epi (F.toLaxMonoidalFunctor.μ (G.obj X ⊗ G.obj Y) (G.obj Z)), ←
-      cancel_epi (F.toLaxMonoidalFunctor.μ (G.obj X) (G.obj Y) ⊗ 𝟙 (F.obj (G.obj Z))),
-      F.toLaxMonoidalFunctor.associativity_assoc (G.obj X) (G.obj Y) (G.obj Z), ←
-      F.toLaxMonoidalFunctor.μ_natural_assoc, assoc, IsIso.hom_inv_id_assoc, ←
-      F.toLaxMonoidalFunctor.μ_natural_assoc, IsIso.hom_inv_id_assoc, ← tensor_comp, ←
-      tensor_comp, id_comp, Functor.map_id, Functor.map_id, id_comp, ← tensor_comp_assoc, ←
-      tensor_comp_assoc, id_comp, id_comp, h.homEquiv_unit, h.homEquiv_unit, Functor.map_comp,
-      assoc, assoc, h.counit_naturality, h.left_triangle_components_assoc, Functor.map_comp,
-      assoc, h.counit_naturality, h.left_triangle_components_assoc]
-    simp)
-  (left_unitality := fun X ↦ by
+    rw [← h.homEquiv_naturality_right, ← h.homEquiv_naturality_left, ← h.homEquiv_naturality_left,
+      ← h.homEquiv_naturality_left, Equiv.apply_eq_iff_eq,
+      ← cancel_epi (F.μ (G.obj X ⊗ G.obj Y) (G.obj Z)),
+      ← cancel_epi (F.μ (G.obj X) (G.obj Y) ▷ (F.obj (G.obj Z)))]
+    simp only [assoc]
+    calc
+      _ = (α_ _ _ _).hom ≫ (h.counit.app X ⊗ h.counit.app Y ⊗ h.counit.app Z) := by
+        rw [← F.μ_natural_left_assoc, IsIso.hom_inv_id_assoc, h.homEquiv_unit,
+          tensorHom_def_assoc (h.counit.app (X ⊗ Y)) (h.counit.app Z)]
+        dsimp only [comp_obj, id_obj]
+        simp_rw [← MonoidalCategory.comp_whiskerRight_assoc]
+        rw [F.map_comp_assoc, h.counit_naturality, h.left_triangle_components_assoc,
+          IsIso.hom_inv_id_assoc, ← tensorHom_def_assoc, associator_naturality]
+      _ = _ := by
+        rw [F.associativity_assoc, ← F.μ_natural_right_assoc, IsIso.hom_inv_id_assoc,
+          h.homEquiv_unit, tensorHom_def (h.counit.app X) (h.counit.app (Y ⊗ Z))]
+        dsimp only [id_obj, comp_obj]
+        rw [whisker_exchange_assoc, ← MonoidalCategory.whiskerLeft_comp, F.map_comp_assoc,
+          h.counit_naturality, h.left_triangle_components_assoc, whisker_exchange_assoc,
+          ← MonoidalCategory.whiskerLeft_comp, ← tensorHom_def, IsIso.hom_inv_id_assoc]
+  left_unitality X := by
     rw [← h.homEquiv_naturality_right, ← h.homEquiv_naturality_left, ← Equiv.symm_apply_eq,
-      h.homEquiv_counit, F.map_leftUnitor, h.homEquiv_unit, assoc, assoc, assoc, F.map_tensor,
-      assoc, assoc, IsIso.hom_inv_id_assoc, ← tensor_comp_assoc, Functor.map_id, id_comp,
-      Functor.map_comp, assoc, h.counit_naturality, h.left_triangle_components_assoc, ←
-      leftUnitor_naturality, ← tensor_comp_assoc, id_comp, comp_id]
-    simp)
-  (right_unitality := fun X ↦  by
+      h.homEquiv_counit, F.map_leftUnitor_assoc, h.homEquiv_unit, F.map_whiskerRight_assoc, assoc,
+      IsIso.hom_inv_id_assoc, tensorHom_def_assoc, ← MonoidalCategory.comp_whiskerRight_assoc,
+      F.map_comp_assoc, h.counit_naturality, h.left_triangle_components_assoc]
+    simp
+  right_unitality X := by
     rw [← h.homEquiv_naturality_right, ← h.homEquiv_naturality_left, ← Equiv.symm_apply_eq,
-      h.homEquiv_counit, F.map_rightUnitor, assoc, assoc, ← rightUnitor_naturality, ←
-      tensor_comp_assoc, comp_id, id_comp, h.homEquiv_unit, F.map_tensor, assoc, assoc, assoc,
-      IsIso.hom_inv_id_assoc, Functor.map_comp, Functor.map_id, ← tensor_comp_assoc, assoc,
-      h.counit_naturality, h.left_triangle_components_assoc, id_comp]
-    simp)
+      h.homEquiv_counit, F.map_rightUnitor_assoc, h.homEquiv_unit, F.map_whiskerLeft_assoc, assoc,
+      IsIso.hom_inv_id_assoc, tensorHom_def'_assoc, ← MonoidalCategory.whiskerLeft_comp_assoc,
+      F.map_comp_assoc, h.counit_naturality, h.left_triangle_components_assoc]
+    simp
 #align category_theory.monoidal_adjoint CategoryTheory.monoidalAdjoint
 
 /-- If a monoidal functor `F` is an equivalence of categories then its inverse is also monoidal. -/
diff --git a/Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean b/Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean
index 765730247e217c..c005ad6d3be94d 100644
--- a/Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean
+++ b/Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean
@@ -77,8 +77,6 @@ end FunctorCategory
 
 open CategoryTheory.Monoidal.FunctorCategory
 
-attribute [local simp] id_tensorHom tensorHom_id in
-
 /-- When `C` is any category, and `D` is a monoidal category,
 the functor category `C ⥤ D` has a natural pointwise monoidal structure,
 where `(F ⊗ G).obj X = F.obj X ⊗ G.obj X`.
@@ -165,8 +163,6 @@ theorem associator_inv_app {F G H : C ⥤ D} {X} :
   rfl
 #align category_theory.monoidal.associator_inv_app CategoryTheory.Monoidal.associator_inv_app
 
-attribute [local simp] id_tensorHom tensorHom_id in
-
 /-- When `C` is any category, and `D` is a monoidal category,
 the functor category `C ⥤ D` has a natural pointwise monoidal structure,
 where `(F ⊗ G).obj X = F.obj X ⊗ G.obj X`.
diff --git a/Mathlib/CategoryTheory/Monoidal/Functorial.lean b/Mathlib/CategoryTheory/Monoidal/Functorial.lean
index 06c35998619725..22fa6acc8f6bbf 100644
--- a/Mathlib/CategoryTheory/Monoidal/Functorial.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Functorial.lean
@@ -57,24 +57,24 @@ class LaxMonoidal (F : C → D) [Functorial.{v₁, v₂} F] where
   μ : ∀ X Y : C, F X ⊗ F Y ⟶ F (X ⊗ Y)
   μ_natural_left :
     ∀ {X Y : C} (f : X ⟶ Y) (X' : C),
-      (map F f ⊗ 𝟙 (F X')) ≫ μ Y X' = μ X X' ≫ map F (f ⊗ 𝟙 X') := by
+      map F f ▷ F X' ≫ μ Y X' = μ X X' ≫ map F (f ▷ X') := by
     aesop_cat
   μ_natural_right :
     ∀ {X Y : C} (X' : C) (f : X ⟶ Y) ,
-      (𝟙 (F X') ⊗ map F f) ≫ μ X' Y = μ X' X ≫ map F (𝟙 X' ⊗ f) := by
+      F X' ◁ map F f ≫ μ X' Y = μ X' X ≫ map F (X' ◁ f) := by
     aesop_cat
   /-- associativity of the tensorator -/
   associativity :
     ∀ X Y Z : C,
-      (μ X Y ⊗ 𝟙 (F Z)) ≫ μ (X ⊗ Y) Z ≫ map F (α_ X Y Z).hom =
-        (α_ (F X) (F Y) (F Z)).hom ≫ (𝟙 (F X) ⊗ μ Y Z) ≫ μ X (Y ⊗ Z) := by
+      μ X Y ▷ F Z ≫ μ (X ⊗ Y) Z ≫ map F (α_ X Y Z).hom =
+        (α_ (F X) (F Y) (F Z)).hom ≫ F X ◁ μ Y Z ≫ μ X (Y ⊗ Z) := by
     aesop_cat
   /-- left unitality -/
-  left_unitality : ∀ X : C, (λ_ (F X)).hom = (ε ⊗ 𝟙 (F X)) ≫ μ (𝟙_ C) X ≫ map F (λ_ X).hom := by
-    aesop_cat
+  left_unitality : ∀ X : C, (λ_ (F X)).hom = ε ▷ F X ≫ μ (𝟙_ C) X ≫ map F (λ_ X).hom :=
+    by aesop_cat
   /-- right unitality -/
-  right_unitality : ∀ X : C, (ρ_ (F X)).hom = (𝟙 (F X) ⊗ ε) ≫ μ X (𝟙_ C) ≫ map F (ρ_ X).hom := by
-    aesop_cat
+  right_unitality : ∀ X : C, (ρ_ (F X)).hom = F X ◁ ε ≫ μ X (𝟙_ C) ≫ map F (ρ_ X).hom :=
+    by aesop_cat
 #align category_theory.lax_monoidal CategoryTheory.LaxMonoidal
 
 /-- An unbundled description of lax monoidal functors. -/
diff --git a/Mathlib/CategoryTheory/Monoidal/Limits.lean b/Mathlib/CategoryTheory/Monoidal/Limits.lean
index 813036093795ab..75e207ce03b60b 100644
--- a/Mathlib/CategoryTheory/Monoidal/Limits.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Limits.lean
@@ -89,7 +89,7 @@ instance limitLaxMonoidal : LaxMonoidal fun F : J ⥤ C => limit F := .ofTensorH
       rw [← comp_tensor_id]
       erw [limit.lift_π]
       dsimp
-    slice_rhs 2 3 => rw [leftUnitor_naturality]
+    slice_rhs 2 3 => rw [id_tensorHom, leftUnitor_naturality]
     simp)
   (right_unitality := fun X => by
     ext j; dsimp
@@ -101,7 +101,7 @@ instance limitLaxMonoidal : LaxMonoidal fun F : J ⥤ C => limit F := .ofTensorH
       rw [← id_tensor_comp]
       erw [limit.lift_π]
       dsimp
-    slice_rhs 2 3 => rw [rightUnitor_naturality]
+    slice_rhs 2 3 => rw [tensorHom_id, rightUnitor_naturality]
     simp)
 #align category_theory.limits.limit_lax_monoidal CategoryTheory.Limits.limitLaxMonoidal
 
diff --git a/Mathlib/CategoryTheory/Monoidal/Linear.lean b/Mathlib/CategoryTheory/Monoidal/Linear.lean
index 20051ab717df89..c8a2e24043adbf 100644
--- a/Mathlib/CategoryTheory/Monoidal/Linear.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Linear.lean
@@ -63,12 +63,12 @@ theorem monoidalLinearOfFaithful {D : Type*} [Category D] [Preadditive D] [Linea
   { whiskerLeft_smul := by
       intros X Y Z r f
       apply F.toFunctor.map_injective
-      rw [F.map_whiskerLeft']
+      rw [F.map_whiskerLeft]
       simp
     smul_whiskerRight := by
       intros r X Y f Z
       apply F.toFunctor.map_injective
-      rw [F.map_whiskerRight']
+      rw [F.map_whiskerRight]
       simp }
 #align category_theory.monoidal_linear_of_faithful CategoryTheory.monoidalLinearOfFaithful
 
diff --git a/Mathlib/CategoryTheory/Monoidal/Mon_.lean b/Mathlib/CategoryTheory/Monoidal/Mon_.lean
index bf7107c14a3b93..3cd885689d61e8 100644
--- a/Mathlib/CategoryTheory/Monoidal/Mon_.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Mon_.lean
@@ -73,12 +73,12 @@ variable {M : Mon_ C}
 
 @[simp]
 theorem one_mul_hom {Z : C} (f : Z ⟶ M.X) : (M.one ⊗ f) ≫ M.mul = (λ_ Z).hom ≫ f := by
-  rw [tensorHom_def'_assoc, M.one_mul, leftUnitor_naturality']
+  rw [tensorHom_def'_assoc, M.one_mul, leftUnitor_naturality]
 #align Mon_.one_mul_hom Mon_.one_mul_hom
 
 @[simp]
 theorem mul_one_hom {Z : C} (f : Z ⟶ M.X) : (f ⊗ M.one) ≫ M.mul = (ρ_ Z).hom ≫ f := by
-  rw [tensorHom_def_assoc, M.mul_one, rightUnitor_naturality']
+  rw [tensorHom_def_assoc, M.mul_one, rightUnitor_naturality]
 #align Mon_.mul_one_hom Mon_.mul_one_hom
 
 theorem assoc_flip :
@@ -163,6 +163,7 @@ instance : ReflectsIsomorphisms (forget C) where
 /-- Construct an isomorphism of monoids by giving an isomorphism between the underlying objects
 and checking compatibility with unit and multiplication only in the forward direction.
 -/
+@[simps]
 def isoOfIso {M N : Mon_ C} (f : M.X ≅ N.X) (one_f : M.one ≫ f.hom = N.one)
     (mul_f : M.mul ≫ f.hom = (f.hom ⊗ f.hom) ≫ N.mul) : M ≅ N where
   hom :=
@@ -212,15 +213,15 @@ def mapMon (F : LaxMonoidalFunctor C D) : Mon_ C ⥤ Mon_ D where
       one := F.ε ≫ F.map A.one
       mul := F.μ _ _ ≫ F.map A.mul
       one_mul := by
-        simp only [comp_whiskerRight, Category.assoc, μ_natural_left'_assoc, left_unitality']
+        simp only [comp_whiskerRight, Category.assoc, μ_natural_left_assoc, left_unitality]
         slice_lhs 3 4 => rw [← F.toFunctor.map_comp, A.one_mul]
       mul_one := by
-        simp only [MonoidalCategory.whiskerLeft_comp, Category.assoc, μ_natural_right'_assoc,
-          right_unitality']
+        simp only [MonoidalCategory.whiskerLeft_comp, Category.assoc, μ_natural_right_assoc,
+          right_unitality]
         slice_lhs 3 4 => rw [← F.toFunctor.map_comp, A.mul_one]
       mul_assoc := by
-        simp only [comp_whiskerRight, Category.assoc, μ_natural_left'_assoc,
-          MonoidalCategory.whiskerLeft_comp, μ_natural_right'_assoc]
+        simp only [comp_whiskerRight, Category.assoc, μ_natural_left_assoc,
+          MonoidalCategory.whiskerLeft_comp, μ_natural_right_assoc]
         slice_lhs 3 4 => rw [← F.toFunctor.map_comp, A.mul_assoc]
         simp }
   map f :=
@@ -258,8 +259,6 @@ def laxMonoidalToMon : LaxMonoidalFunctor (Discrete PUnit.{u + 1}) C ⥤ Mon_ C
   map α := ((mapMonFunctor (Discrete PUnit) C).map α).app _
 #align Mon_.equiv_lax_monoidal_functor_punit.lax_monoidal_to_Mon Mon_.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon
 
-attribute [local simp] id_tensorHom tensorHom_id
-
 /-- Implementation of `Mon_.equivLaxMonoidalFunctorPUnit`. -/
 @[simps]
 def monToLaxMonoidal : Mon_ C ⥤ LaxMonoidalFunctor (Discrete PUnit.{u + 1}) C where
@@ -377,14 +376,12 @@ theorem one_associator {M N P : Mon_ C} :
   slice_lhs 1 3 => rw [← Category.id_comp P.one, tensor_comp]
   slice_lhs 2 3 => rw [associator_naturality]
   slice_rhs 1 2 => rw [← Category.id_comp M.one, tensor_comp]
-  slice_lhs 1 2 => rw [← leftUnitor_tensor_inv]
+  slice_lhs 1 2 => rw [tensorHom_id, ← leftUnitor_tensor_inv]
   rw [← cancel_epi (λ_ (𝟙_ C)).inv]
   slice_lhs 1 2 => rw [leftUnitor_inv_naturality]
   simp
 #align Mon_.one_associator Mon_.one_associator
 
-attribute [local simp] id_tensorHom tensorHom_id
-
 theorem one_leftUnitor {M : Mon_ C} :
     ((λ_ (𝟙_ C)).inv ≫ (𝟙 (𝟙_ C) ⊗ M.one)) ≫ (λ_ M.X).hom = M.one := by
   simp
@@ -454,7 +451,7 @@ theorem mul_leftUnitor {M : Mon_ C} :
       ((λ_ M.X).hom ⊗ (λ_ M.X).hom) ≫ M.mul := by
   rw [← Category.comp_id (λ_ (𝟙_ C)).hom, ← Category.id_comp M.mul, tensor_comp]
   simp only [tensorHom_id, id_tensorHom]
-  slice_lhs 3 4 => rw [leftUnitor_naturality']
+  slice_lhs 3 4 => rw [leftUnitor_naturality]
   slice_lhs 1 3 => rw [← leftUnitor_monoidal]
   simp only [Category.assoc, Category.id_comp]
 #align Mon_.mul_left_unitor Mon_.mul_leftUnitor
@@ -464,7 +461,7 @@ theorem mul_rightUnitor {M : Mon_ C} :
       ((ρ_ M.X).hom ⊗ (ρ_ M.X).hom) ≫ M.mul := by
   rw [← Category.id_comp M.mul, ← Category.comp_id (λ_ (𝟙_ C)).hom, tensor_comp]
   simp only [tensorHom_id, id_tensorHom]
-  slice_lhs 3 4 => rw [rightUnitor_naturality']
+  slice_lhs 3 4 => rw [rightUnitor_naturality]
   slice_lhs 1 3 => rw [← rightUnitor_monoidal]
   simp only [Category.assoc, Category.id_comp]
 #align Mon_.mul_right_unitor Mon_.mul_rightUnitor
diff --git a/Mathlib/CategoryTheory/Monoidal/Opposite.lean b/Mathlib/CategoryTheory/Monoidal/Opposite.lean
index 82c1f70f0a4424..16da27d6e31a89 100644
--- a/Mathlib/CategoryTheory/Monoidal/Opposite.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Opposite.lean
@@ -175,8 +175,6 @@ variable [MonoidalCategory.{v₁} C]
 
 open Opposite MonoidalCategory
 
-attribute [local simp] id_tensorHom tensorHom_id
-
 instance monoidalCategoryOp : MonoidalCategory Cᵒᵖ where
   tensorObj X Y := op (unop X ⊗ unop Y)
   whiskerLeft X _ _ f := (X.unop ◁ f.unop).op
diff --git a/Mathlib/CategoryTheory/Monoidal/Preadditive.lean b/Mathlib/CategoryTheory/Monoidal/Preadditive.lean
index 443b27d7b1ca6a..3edf5c5f7b015c 100644
--- a/Mathlib/CategoryTheory/Monoidal/Preadditive.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Preadditive.lean
@@ -85,20 +85,20 @@ theorem monoidalPreadditive_of_faithful {D} [Category D] [Preadditive D] [Monoid
   { whiskerLeft_zero := by
       intros
       apply F.toFunctor.map_injective
-      simp [F.map_whiskerLeft']
+      simp [F.map_whiskerLeft]
     zero_whiskerRight := by
       intros
       apply F.toFunctor.map_injective
-      simp [F.map_whiskerRight']
+      simp [F.map_whiskerRight]
     whiskerLeft_add := by
       intros
       apply F.toFunctor.map_injective
-      simp only [F.map_whiskerLeft', Functor.map_add, Preadditive.comp_add, Preadditive.add_comp,
+      simp only [F.map_whiskerLeft, Functor.map_add, Preadditive.comp_add, Preadditive.add_comp,
         MonoidalPreadditive.whiskerLeft_add]
     add_whiskerRight := by
       intros
       apply F.toFunctor.map_injective
-      simp only [F.map_whiskerRight', Functor.map_add, Preadditive.comp_add, Preadditive.add_comp,
+      simp only [F.map_whiskerRight, Functor.map_add, Preadditive.comp_add, Preadditive.add_comp,
         MonoidalPreadditive.add_whiskerRight] }
 #align category_theory.monoidal_preadditive_of_faithful CategoryTheory.monoidalPreadditive_of_faithful
 
diff --git a/Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean b/Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean
index 0d26c763b98d58..d1a1a28af4e9ff 100644
--- a/Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean
@@ -331,8 +331,6 @@ def tensorRightHomEquiv (X Y Y' Z : C) [ExactPairing Y Y'] : (X ⊗ Y ⟶ Z) ≃
         rw [coevaluation_evaluation'']; coherence
 #align category_theory.tensor_right_hom_equiv CategoryTheory.tensorRightHomEquiv
 
-attribute [local simp] id_tensorHom tensorHom_id
-
 theorem tensorLeftHomEquiv_naturality {X Y Y' Z Z' : C} [ExactPairing Y Y'] (f : Y' ⊗ X ⟶ Z)
     (g : Z ⟶ Z') :
     (tensorLeftHomEquiv X Y Y' Z') (f ≫ g) = (tensorLeftHomEquiv X Y Y' Z) f ≫ Y ◁ g := by
@@ -402,8 +400,6 @@ theorem tensorLeftHomEquiv_tensor {X X' Y Y' Z Z' : C} [ExactPairing Y Y'] (f :
   simp [tensorLeftHomEquiv, tensorHom_def']
 #align category_theory.tensor_left_hom_equiv_tensor CategoryTheory.tensorLeftHomEquiv_tensor
 
-attribute [local simp] id_tensorHom tensorHom_id
-
 /-- `tensorRightHomEquiv` commutes with tensoring on the left -/
 theorem tensorRightHomEquiv_tensor {X X' Y Y' Z Z' : C} [ExactPairing Y Y'] (f : X ⟶ Z ⊗ Y')
     (g : X' ⟶ Z') :
diff --git a/Mathlib/CategoryTheory/Monoidal/Rigid/OfEquivalence.lean b/Mathlib/CategoryTheory/Monoidal/Rigid/OfEquivalence.lean
index b718cce09d78cd..cad8f813ab111a 100644
--- a/Mathlib/CategoryTheory/Monoidal/Rigid/OfEquivalence.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Rigid/OfEquivalence.lean
@@ -22,8 +22,6 @@ variable {C D : Type*} [Category C] [Category D] [MonoidalCategory C] [MonoidalC
 
 variable (F : MonoidalFunctor C D)
 
-attribute [local simp] id_tensorHom tensorHom_id
-
 /-- Given candidate data for an exact pairing,
 which is sent by a faithful monoidal functor to an exact pairing,
 the equations holds automatically. -/
@@ -36,11 +34,11 @@ def exactPairingOfFaithful [Faithful F.toFunctor] {X Y : C} (eval : Y ⊗ X ⟶
   evaluation_coevaluation' :=
     F.toFunctor.map_injective <| by
       simp [map_eval, map_coeval,
-        MonoidalFunctor.map_whiskerLeft', MonoidalFunctor.map_whiskerRight']
+        MonoidalFunctor.map_whiskerLeft, MonoidalFunctor.map_whiskerRight]
   coevaluation_evaluation' :=
     F.toFunctor.map_injective <| by
       simp [map_eval, map_coeval,
-        MonoidalFunctor.map_whiskerLeft', MonoidalFunctor.map_whiskerRight']
+        MonoidalFunctor.map_whiskerLeft, MonoidalFunctor.map_whiskerRight]
 #align category_theory.exact_pairing_of_faithful CategoryTheory.exactPairingOfFaithful
 
 /-- Given a pair of objects which are sent by a fully faithful functor to a pair of objects
diff --git a/Mathlib/CategoryTheory/Monoidal/Transport.lean b/Mathlib/CategoryTheory/Monoidal/Transport.lean
index e9e66fdc336025..45cb26fa843c1a 100644
--- a/Mathlib/CategoryTheory/Monoidal/Transport.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Transport.lean
@@ -102,21 +102,19 @@ abbrev induced [MonoidalCategoryStruct D] (F : D ⥤ C) [Faithful F]
   id_whiskerRight X Y := F.map_injective <| by simp [fData.whiskerRight_eq]
   triangle X Y := F.map_injective <| by cases fData; aesop_cat
   pentagon W X Y Z := F.map_injective <| by
-    simp only [Functor.map_comp, fData.tensorHom_eq, fData.associator_eq, Iso.trans_assoc,
+    simp only [Functor.map_comp, fData.whiskerRight_eq, fData.associator_eq, Iso.trans_assoc,
       Iso.trans_hom, Iso.symm_hom, tensorIso_hom, Iso.refl_hom, tensorHom_id, id_tensorHom,
-      Functor.map_id, comp_whiskerRight, whisker_assoc, assoc, MonoidalCategory.whiskerLeft_comp,
-      Iso.hom_inv_id_assoc, whiskerLeft_hom_inv_assoc, hom_inv_whiskerRight_assoc,
-      Iso.inv_hom_id_assoc, Iso.cancel_iso_inv_left]
+      comp_whiskerRight, whisker_assoc, assoc, fData.whiskerLeft_eq,
+      MonoidalCategory.whiskerLeft_comp, Iso.hom_inv_id_assoc, whiskerLeft_hom_inv_assoc,
+      hom_inv_whiskerRight_assoc, Iso.inv_hom_id_assoc, Iso.cancel_iso_inv_left]
     slice_lhs 5 6 =>
       rw [← MonoidalCategory.whiskerLeft_comp, hom_inv_whiskerRight]
     rw [whisker_exchange_assoc]
     simp
   leftUnitor_naturality {X Y : D} f := F.map_injective <| by
-    simp [fData.leftUnitor_eq, fData.tensorHom_eq, whisker_exchange_assoc,
-      id_tensorHom, tensorHom_id]
+    simp [fData.leftUnitor_eq, fData.whiskerLeft_eq, whisker_exchange_assoc]
   rightUnitor_naturality {X Y : D} f := F.map_injective <| by
-    simp [fData.rightUnitor_eq, fData.tensorHom_eq, ← whisker_exchange_assoc,
-      id_tensorHom, tensorHom_id]
+    simp [fData.rightUnitor_eq, fData.whiskerRight_eq, ← whisker_exchange_assoc]
   associator_naturality {X₁ X₂ X₃ Y₁ Y₂ Y₃} f₁ f₂ f₃ := F.map_injective <| by
     simp [fData.tensorHom_eq, fData.associator_eq, tensorHom_def, whisker_exchange_assoc]
 
diff --git a/Mathlib/CategoryTheory/Monoidal/Types/Coyoneda.lean b/Mathlib/CategoryTheory/Monoidal/Types/Coyoneda.lean
index 215e05af141cad..223ebae8b70ff0 100644
--- a/Mathlib/CategoryTheory/Monoidal/Types/Coyoneda.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Types/Coyoneda.lean
@@ -33,8 +33,6 @@ open MonoidalCategory
 -- I don't know if that is a problem, might need to change it back in the future, but
 -- if so it might be better to fix then instead of at the moment of porting.
 
-attribute [local simp] id_tensorHom tensorHom_id
-
 /-- `(𝟙_ C ⟶ -)` is a lax monoidal functor to `Type`. -/
 noncomputable
 def coyonedaTensorUnit (C : Type u) [Category.{v} C] [MonoidalCategory C] :
@@ -48,13 +46,18 @@ def coyonedaTensorUnit (C : Type u) [Category.{v} C] [MonoidalCategory C] :
       dsimp; simp only [Iso.cancel_iso_inv_left, Category.assoc]
       conv_lhs =>
         rw [← Category.id_comp h, tensor_comp, Category.assoc, associator_naturality, ←
-          Category.assoc, unitors_inv_equal, triangle_assoc_comp_right_inv]
-      conv_rhs => rw [← Category.id_comp f, tensor_comp])
-    (left_unitality := by aesop_cat)
+          Category.assoc, unitors_inv_equal, tensorHom_id, triangle_assoc_comp_right_inv]
+      conv_rhs => rw [← Category.id_comp f, tensor_comp]
+      simp)
+    (left_unitality := by
+      intros
+      ext ⟨⟨⟩, f⟩; dsimp at f
+      dsimp
+      simp)
     (right_unitality := fun X => by
       ext ⟨f, ⟨⟩⟩; dsimp at f
-      dsimp; simp only [Category.assoc]
-      rw [rightUnitor_naturality, unitors_inv_equal, Iso.inv_hom_id_assoc])
+      dsimp
+      simp [unitors_inv_equal])
 #align category_theory.coyoneda_tensor_unit CategoryTheory.coyonedaTensorUnit
 
 end CategoryTheory
diff --git a/Mathlib/RepresentationTheory/Action/Monoidal.lean b/Mathlib/RepresentationTheory/Action/Monoidal.lean
index df738c059cf518..9fd3db06d67713 100644
--- a/Mathlib/RepresentationTheory/Action/Monoidal.lean
+++ b/Mathlib/RepresentationTheory/Action/Monoidal.lean
@@ -176,7 +176,7 @@ section
 
 variable [Preadditive V] [MonoidalPreadditive V]
 
-attribute [local simp] MonoidalPreadditive.tensor_add MonoidalPreadditive.add_tensor
+attribute [local simp] MonoidalPreadditive.whiskerLeft_add MonoidalPreadditive.add_whiskerRight
 
 instance : MonoidalPreadditive (Action V G) where
 
@@ -399,17 +399,10 @@ def mapActionLax (F : LaxMonoidalFunctor V W) (G : MonCat.{u}) :
   (μ := fun X Y =>
     { hom := F.μ X.V Y.V
       comm := fun g => F.μ_natural (X.ρ g) (Y.ρ g) })
-  -- using `dsimp` before `simp` speeds these up
-  (μ_natural := @fun {X Y X' Y'} f g ↦ by ext; dsimp; simp)
-  (associativity := fun X Y Z ↦ by ext; dsimp; simp)
-  (left_unitality := fun X ↦ by ext; dsimp; simp)
-  (right_unitality := fun X ↦ by
-    ext
-    dsimp
-    simp only [MonoidalCategory.rightUnitor_conjugation,
-      LaxMonoidalFunctor.right_unitality, Category.id_comp, Category.assoc,
-      LaxMonoidalFunctor.right_unitality_inv_assoc, Category.comp_id, Iso.hom_inv_id]
-    rw [← F.map_comp, Iso.inv_hom_id, F.map_id, Category.comp_id])
+  (μ_natural := by intros; ext; simp)
+  (associativity := by intros; ext; simp)
+  (left_unitality := by intros; ext; simp)
+  (right_unitality := by intros; ext; simp)
 
 variable (F : MonoidalFunctor V W) (G : MonCat.{u})