diff --git a/Mathlib/CategoryTheory/Monad/EquivMon.lean b/Mathlib/CategoryTheory/Monad/EquivMon.lean
index 74a46af127c22..b24fe287b95c6 100644
--- a/Mathlib/CategoryTheory/Monad/EquivMon.lean
+++ b/Mathlib/CategoryTheory/Monad/EquivMon.lean
@@ -66,14 +66,14 @@ def ofMon (M : Mon_ (C ⥤ C)) : Monad C where
   μ' := M.mul
   left_unit' := fun X => by
     -- Porting note: now using `erw`
-    erw [← NatTrans.id_hcomp_app M.one, ← NatTrans.comp_app, M.mul_one]
+    erw [← whiskerLeft_app, ← NatTrans.comp_app, M.mul_one]
     rfl
   right_unit' := fun X => by
     -- Porting note: now using `erw`
-    erw [← NatTrans.hcomp_id_app M.one, ← NatTrans.comp_app, M.one_mul]
+    erw [← whiskerRight_app, ← NatTrans.comp_app, M.one_mul]
     rfl
   assoc' := fun X => by
-    rw [← NatTrans.hcomp_id_app, ← NatTrans.comp_app]
+    rw [← whiskerLeft_app, ← whiskerRight_app, ← NatTrans.comp_app]
     -- Porting note: had to add this step:
     erw [M.mul_assoc]
     simp
diff --git a/Mathlib/CategoryTheory/Monoidal/Bimod.lean b/Mathlib/CategoryTheory/Monoidal/Bimod.lean
index deb4b6049ec25..700a2748622e5 100644
--- a/Mathlib/CategoryTheory/Monoidal/Bimod.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Bimod.lean
@@ -180,6 +180,8 @@ set_option linter.uppercaseLean3 false in
 
 variable (A)
 
+attribute [local simp] id_tensorHom tensorHom_id
+
 /-- A monoid object as a bimodule over itself. -/
 @[simps]
 def regular : Bimod A A where
@@ -663,7 +665,7 @@ theorem hom_inv_id : hom P ≫ inv P = 𝟙 _ := by
   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]
   slice_lhs 2 3 => rw [← MonoidalCategory.tensor_id, associator_inv_naturality]
-  slice_lhs 3 4 => rw [← comp_tensor_id, Mon_.one_mul]
+  slice_lhs 3 4 => rw [← comp_tensor_id, tensorHom_id, tensorHom_id, Mon_.one_mul]
   slice_rhs 1 2 => rw [Category.comp_id]
   coherence
 set_option linter.uppercaseLean3 false in
@@ -730,7 +732,7 @@ theorem hom_inv_id : hom P ≫ inv P = 𝟙 _ := by
   slice_lhs 2 3 => rw [tensor_id_comp_id_tensor, ← id_tensor_comp_tensor_id]
   slice_lhs 3 4 => rw [coequalizer.condition]
   slice_lhs 2 3 => rw [← MonoidalCategory.tensor_id, associator_naturality]
-  slice_lhs 3 4 => rw [← id_tensor_comp, Mon_.mul_one]
+  slice_lhs 3 4 => rw [← id_tensor_comp, id_tensorHom, id_tensorHom, Mon_.mul_one]
   slice_rhs 1 2 => rw [Category.comp_id]
   coherence
 set_option linter.uppercaseLean3 false in
@@ -833,10 +835,10 @@ theorem id_whisker_left_bimod {X Y : Mon_ C} {M N : Bimod X Y} (f : M ⟶ N) :
   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]
   slice_rhs 3 4 => rw [← MonoidalCategory.tensor_id, associator_inv_naturality]
-  slice_rhs 4 5 => rw [← comp_tensor_id, Mon_.one_mul]
+  slice_rhs 4 5 => rw [← comp_tensor_id, tensorHom_id, tensorHom_id, Mon_.one_mul]
   have : (λ_ (X.X ⊗ N.X)).inv ≫ (α_ (𝟙_ C) X.X N.X).inv ≫ ((λ_ X.X).hom ⊗ 𝟙 N.X) = 𝟙 _ := by
     pure_coherence
-  slice_rhs 2 4 => rw [this]
+  slice_rhs 2 4 => rw [← tensorHom_id, this]
   slice_rhs 1 2 => rw [Category.comp_id]
 set_option linter.uppercaseLean3 false in
 #align Bimod.id_whisker_left_Bimod Bimod.id_whisker_left_bimod
@@ -890,10 +892,10 @@ theorem whisker_right_id_bimod {X Y : Mon_ C} {M N : Bimod X Y} (f : M ⟶ N) :
   slice_rhs 3 4 => rw [tensor_id_comp_id_tensor, ← id_tensor_comp_tensor_id]
   slice_rhs 4 5 => rw [coequalizer.condition]
   slice_rhs 3 4 => rw [← MonoidalCategory.tensor_id, associator_naturality]
-  slice_rhs 4 5 => rw [← id_tensor_comp, Mon_.mul_one]
+  slice_rhs 4 5 => rw [← id_tensor_comp, id_tensorHom, id_tensorHom, Mon_.mul_one]
   have : (ρ_ (N.X ⊗ Y.X)).inv ≫ (α_ N.X Y.X (𝟙_ C)).hom ≫ (𝟙 N.X ⊗ (ρ_ Y.X).hom) = 𝟙 _ := by
     pure_coherence
-  slice_rhs 2 4 => rw [this]
+  slice_rhs 2 4 => rw [← id_tensorHom, this]
   slice_rhs 1 2 => rw [Category.comp_id]
 set_option linter.uppercaseLean3 false in
 #align Bimod.whisker_right_id_Bimod Bimod.whisker_right_id_bimod
diff --git a/Mathlib/CategoryTheory/Monoidal/Braided.lean b/Mathlib/CategoryTheory/Monoidal/Braided.lean
index 248b50ffa9f57..d4120883df0bf 100644
--- a/Mathlib/CategoryTheory/Monoidal/Braided.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Braided.lean
@@ -42,26 +42,25 @@ and also satisfies the two hexagon identities.
 class BraidedCategory (C : Type u) [Category.{v} C] [MonoidalCategory.{v} C] where
   /-- The braiding natural isomorphism. -/
   braiding : ∀ X Y : C, X ⊗ Y ≅ Y ⊗ X
-  -- Note: `𝟙 X ⊗ f` will be replaced by `X ◁ f` (and similarly for `f ⊗ 𝟙 Z`) in #6307.
   braiding_naturality_right :
     ∀ (X : C) {Y Z : C} (f : Y ⟶ Z),
-      (𝟙 X ⊗ f) ≫ (braiding X Z).hom = (braiding X Y).hom ≫ (f ⊗ 𝟙 X) := by
+      X ◁ f ≫ (braiding X Z).hom = (braiding X Y).hom ≫ f ▷ X := by
     aesop_cat
   braiding_naturality_left :
     ∀ {X Y : C} (f : X ⟶ Y) (Z : C),
-      (f ⊗ 𝟙 Z) ≫ (braiding Y Z).hom = (braiding X Z).hom ≫ (𝟙 Z ⊗ f) := by
+      f ▷ Z ≫ (braiding Y Z).hom = (braiding X Z).hom ≫ Z ◁ f := by
     aesop_cat
   /-- The first hexagon identity. -/
   hexagon_forward :
     ∀ X Y Z : C,
       (α_ X Y Z).hom ≫ (braiding X (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom =
-        ((braiding X Y).hom ⊗ 𝟙 Z) ≫ (α_ Y X Z).hom ≫ (𝟙 Y ⊗ (braiding X Z).hom) := by
+        ((braiding X Y).hom ▷ Z) ≫ (α_ Y X Z).hom ≫ (Y ◁ (braiding X Z).hom) := by
     aesop_cat
   /-- The second hexagon identity. -/
   hexagon_reverse :
     ∀ X Y Z : C,
       (α_ X Y Z).inv ≫ (braiding (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv =
-        (𝟙 X ⊗ (braiding Y Z).hom) ≫ (α_ X Z Y).inv ≫ ((braiding X Z).hom ⊗ 𝟙 Y) := by
+        (X ◁ (braiding Y Z).hom) ≫ (α_ X Z Y).inv ≫ ((braiding X Z).hom ▷ Y) := by
     aesop_cat
 #align category_theory.braided_category CategoryTheory.BraidedCategory
 
@@ -86,8 +85,8 @@ variable {C : Type u} [Category.{v} C] [MonoidalCategory.{v} C] [BraidedCategory
 @[simp]
 theorem braiding_tensor_left (X Y Z : C) :
     (β_ (X ⊗ Y) Z).hom  =
-      (α_ X Y Z).hom ≫ (𝟙 X ⊗ (β_ Y Z).hom) ≫ (α_ X Z Y).inv ≫
-        ((β_ X Z).hom ⊗ 𝟙 Y) ≫ (α_ Z X Y).hom := by
+      (α_ X Y Z).hom ≫ X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫
+        (β_ X Z).hom ▷ Y ≫ (α_ Z X Y).hom := by
   intros
   apply (cancel_epi (α_ X Y Z).inv).1
   apply (cancel_mono (α_ Z X Y).inv).1
@@ -96,8 +95,8 @@ theorem braiding_tensor_left (X Y Z : C) :
 @[simp]
 theorem braiding_tensor_right (X Y Z : C) :
     (β_ X (Y ⊗ Z)).hom  =
-      (α_ X Y Z).inv ≫ ((β_ X Y).hom ⊗ 𝟙 Z) ≫ (α_ Y X Z).hom ≫
-        (𝟙 Y ⊗ (β_ X Z).hom) ≫ (α_ Y Z X).inv := by
+      (α_ X Y Z).inv ≫ (β_ X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫
+        Y ◁ (β_ X Z).hom ≫ (α_ Y Z X).inv := by
   intros
   apply (cancel_epi (α_ X Y Z).hom).1
   apply (cancel_mono (α_ Y Z X).hom).1
@@ -106,22 +105,21 @@ theorem braiding_tensor_right (X Y Z : C) :
 @[simp]
 theorem braiding_inv_tensor_left (X Y Z : C) :
     (β_ (X ⊗ Y) Z).inv  =
-      (α_ Z X Y).inv ≫ ((β_ X Z).inv ⊗ 𝟙 Y) ≫ (α_ X Z Y).hom ≫
-        (𝟙 X ⊗ (β_ Y Z).inv) ≫ (α_ X Y Z).inv :=
+      (α_ Z X Y).inv ≫ (β_ X Z).inv ▷ Y ≫ (α_ X Z Y).hom ≫
+        X ◁ (β_ Y Z).inv ≫ (α_ X Y Z).inv :=
   eq_of_inv_eq_inv (by simp)
 
 @[simp]
 theorem braiding_inv_tensor_right (X Y Z : C) :
     (β_ X (Y ⊗ Z)).inv  =
-      (α_ Y Z X).hom ≫ (𝟙 Y ⊗ (β_ X Z).inv) ≫ (α_ Y X Z).inv ≫
-        ((β_ X Y).inv ⊗ 𝟙 Z) ≫ (α_ X Y Z).hom :=
+      (α_ Y Z X).hom ≫ Y ◁ (β_ X Z).inv ≫ (α_ Y X Z).inv ≫
+        (β_ X Y).inv ▷ Z ≫ (α_ X Y Z).hom :=
   eq_of_inv_eq_inv (by simp)
 
--- The priority setting will not be needed when we replace `𝟙 X ⊗ f` by `X ◁ f`.
-@[reassoc (attr := simp (low))]
+@[reassoc (attr := simp)]
 theorem braiding_naturality {X X' Y Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') :
     (f ⊗ g) ≫ (braiding Y Y').hom = (braiding X X').hom ≫ (g ⊗ f) := by
-  rw [← tensor_id_comp_id_tensor f g, ← id_tensor_comp_tensor_id g f]
+  rw [tensorHom_def' f g, tensorHom_def g f]
   simp_rw [Category.assoc, braiding_naturality_left, braiding_naturality_right_assoc]
 
 end BraidedCategory
@@ -139,36 +137,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 ?_
+    refine (cancel_epi (F.μ _ _ ▷ _)).1 ?_
     rw [Functor.map_comp, Functor.map_comp, Functor.map_comp, Functor.map_comp, ←
-      LaxMonoidalFunctor.μ_natural_assoc, Functor.map_id, ← comp_tensor_id_assoc, w,
-      comp_tensor_id, assoc, LaxMonoidalFunctor.associativity_assoc,
-      LaxMonoidalFunctor.associativity_assoc, ← LaxMonoidalFunctor.μ_natural, Functor.map_id, ←
-      id_tensor_comp_assoc, w, id_tensor_comp_assoc, reassoc_of% w, braiding_naturality_assoc,
-      LaxMonoidalFunctor.associativity, hexagon_forward_assoc]
+      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]
   hexagon_reverse := by
     intros
     apply F.toFunctor.map_injective
     refine (cancel_epi (F.μ _ _)).1 ?_
-    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_assoc, Functor.map_id, ← id_tensor_comp_assoc, w,
-      id_tensor_comp_assoc, LaxMonoidalFunctor.associativity_inv_assoc,
-      LaxMonoidalFunctor.associativity_inv_assoc, ← LaxMonoidalFunctor.μ_natural,
-      Functor.map_id, ← comp_tensor_id_assoc, w, comp_tensor_id_assoc, reassoc_of% w,
-      braiding_naturality_assoc, LaxMonoidalFunctor.associativity_inv, hexagon_reverse_assoc]
+      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]
 #align category_theory.braided_category_of_faithful CategoryTheory.braidedCategoryOfFaithful
 
 /-- Pull back a braiding along a fully faithful monoidal functor. -/
@@ -200,82 +199,89 @@ variable (C : Type u₁) [Category.{v₁} C] [MonoidalCategory C] [BraidedCatego
 
 theorem braiding_leftUnitor_aux₁ (X : C) :
     (α_ (𝟙_ C) (𝟙_ C) X).hom ≫
-        (𝟙 (𝟙_ C) ⊗ (β_ X (𝟙_ C)).inv) ≫ (α_ _ X _).inv ≫ ((λ_ X).hom ⊗ 𝟙 _) =
-      ((λ_ _).hom ⊗ 𝟙 X) ≫ (β_ X (𝟙_ C)).inv :=
-  by rw [← leftUnitor_tensor, leftUnitor_naturality]; simp [id_tensorHom, tensorHom_id]
+        (𝟙_ C ◁ (β_ X (𝟙_ C)).inv) ≫ (α_ _ X _).inv ≫ ((λ_ X).hom ▷ _) =
+      ((λ_ _).hom ▷ X) ≫ (β_ X (𝟙_ C)).inv := by
+  coherence
 #align category_theory.braiding_left_unitor_aux₁ CategoryTheory.braiding_leftUnitor_aux₁
 
 theorem braiding_leftUnitor_aux₂ (X : C) :
-    ((β_ X (𝟙_ C)).hom ⊗ 𝟙 (𝟙_ C)) ≫ ((λ_ X).hom ⊗ 𝟙 (𝟙_ C)) = (ρ_ X).hom ⊗ 𝟙 (𝟙_ C) :=
+    ((β_ X (𝟙_ C)).hom ▷ 𝟙_ C) ≫ ((λ_ X).hom ▷ 𝟙_ C) = (ρ_ X).hom ▷ 𝟙_ C :=
   calc
-    ((β_ X (𝟙_ C)).hom ⊗ 𝟙 (𝟙_ C)) ≫ ((λ_ X).hom ⊗ 𝟙 (𝟙_ C)) =
-      ((β_ X (𝟙_ C)).hom ⊗ 𝟙 (𝟙_ C)) ≫ (α_ _ _ _).hom ≫ (α_ _ _ _).inv ≫ ((λ_ X).hom ⊗ 𝟙 (𝟙_ C)) :=
+    ((β_ X (𝟙_ C)).hom ▷ 𝟙_ C) ≫ ((λ_ X).hom ▷ 𝟙_ C) =
+      ((β_ X (𝟙_ C)).hom ▷ 𝟙_ C) ≫ (α_ _ _ _).hom ≫ (α_ _ _ _).inv ≫ ((λ_ X).hom ▷ 𝟙_ C) :=
       by coherence
-    _ = ((β_ X (𝟙_ C)).hom ⊗ 𝟙 (𝟙_ C)) ≫ (α_ _ _ _).hom ≫ (𝟙 _ ⊗ (β_ X _).hom) ≫
-          (𝟙 _ ⊗ (β_ X _).inv) ≫ (α_ _ _ _).inv ≫ ((λ_ X).hom ⊗ 𝟙 (𝟙_ C)) :=
-      by (slice_rhs 3 4 => rw [← id_tensor_comp, Iso.hom_inv_id, tensor_id]); rw [id_comp]
-    _ = (α_ _ _ _).hom ≫ (β_ _ _).hom ≫ (α_ _ _ _).hom ≫ (𝟙 _ ⊗ (β_ X _).inv) ≫ (α_ _ _ _).inv ≫
-          ((λ_ X).hom ⊗ 𝟙 (𝟙_ C)) :=
+    _ = ((β_ X (𝟙_ C)).hom ▷ 𝟙_ C) ≫ (α_ _ _ _).hom ≫ (_ ◁ (β_ X _).hom) ≫
+          (_ ◁ (β_ X _).inv) ≫ (α_ _ _ _).inv ≫ ((λ_ X).hom ▷ 𝟙_ C) :=
+      by simp
+    _ = (α_ _ _ _).hom ≫ (β_ _ _).hom ≫ (α_ _ _ _).hom ≫ (_ ◁ (β_ X _).inv) ≫ (α_ _ _ _).inv ≫
+          ((λ_ X).hom ▷ 𝟙_ C) :=
       by (slice_lhs 1 3 => rw [← hexagon_forward]); simp only [assoc]
-    _ = (α_ _ _ _).hom ≫ (β_ _ _).hom ≫ ((λ_ _).hom ⊗ 𝟙 X) ≫ (β_ X _).inv :=
+    _ = (α_ _ _ _).hom ≫ (β_ _ _).hom ≫ ((λ_ _).hom ▷ X) ≫ (β_ X _).inv :=
       by rw [braiding_leftUnitor_aux₁]
-    _ = (α_ _ _ _).hom ≫ (𝟙 _ ⊗ (λ_ _).hom) ≫ (β_ _ _).hom ≫ (β_ X _).inv :=
-      by (slice_lhs 2 3 => rw [← braiding_naturality]); simp only [assoc]
-    _ = (α_ _ _ _).hom ≫ (𝟙 _ ⊗ (λ_ _).hom) := by rw [Iso.hom_inv_id, comp_id]
-    _ = (ρ_ X).hom ⊗ 𝟙 (𝟙_ C) := by rw [triangle]
+    _ = (α_ _ _ _).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']
 
 #align category_theory.braiding_left_unitor_aux₂ CategoryTheory.braiding_leftUnitor_aux₂
 
-@[simp]
+@[reassoc]
 theorem braiding_leftUnitor (X : C) : (β_ X (𝟙_ C)).hom ≫ (λ_ X).hom = (ρ_ X).hom := by
-  rw [← tensor_right_iff, comp_tensor_id, braiding_leftUnitor_aux₂]
+  rw [← whiskerRight_iff, comp_whiskerRight, braiding_leftUnitor_aux₂]
 #align category_theory.braiding_left_unitor CategoryTheory.braiding_leftUnitor
 
 theorem braiding_rightUnitor_aux₁ (X : C) :
     (α_ X (𝟙_ C) (𝟙_ C)).inv ≫
-        ((β_ (𝟙_ C) X).inv ⊗ 𝟙 (𝟙_ C)) ≫ (α_ _ X _).hom ≫ (𝟙 _ ⊗ (ρ_ X).hom) =
-      (𝟙 X ⊗ (ρ_ _).hom) ≫ (β_ (𝟙_ C) X).inv :=
-  by rw [← rightUnitor_tensor, rightUnitor_naturality]; simp [id_tensorHom, tensorHom_id]
+        ((β_ (𝟙_ C) X).inv ▷ 𝟙_ C) ≫ (α_ _ X _).hom ≫ (_ ◁ (ρ_ X).hom) =
+      (X ◁ (ρ_ _).hom) ≫ (β_ (𝟙_ C) X).inv := by
+  coherence
 #align category_theory.braiding_right_unitor_aux₁ CategoryTheory.braiding_rightUnitor_aux₁
 
 theorem braiding_rightUnitor_aux₂ (X : C) :
-    (𝟙 (𝟙_ C) ⊗ (β_ (𝟙_ C) X).hom) ≫ (𝟙 (𝟙_ C) ⊗ (ρ_ X).hom) = 𝟙 (𝟙_ C) ⊗ (λ_ X).hom :=
+    (𝟙_ C ◁ (β_ (𝟙_ C) X).hom) ≫ (𝟙_ C ◁ (ρ_ X).hom) = 𝟙_ C ◁ (λ_ X).hom :=
   calc
-    (𝟙 (𝟙_ C) ⊗ (β_ (𝟙_ C) X).hom) ≫ (𝟙 (𝟙_ C) ⊗ (ρ_ X).hom) =
-      (𝟙 (𝟙_ C) ⊗ (β_ (𝟙_ C) X).hom) ≫ (α_ _ _ _).inv ≫ (α_ _ _ _).hom ≫ (𝟙 (𝟙_ C) ⊗ (ρ_ X).hom) :=
+    (𝟙_ C ◁ (β_ (𝟙_ C) X).hom) ≫ (𝟙_ C ◁ (ρ_ X).hom) =
+      (𝟙_ C ◁ (β_ (𝟙_ C) X).hom) ≫ (α_ _ _ _).inv ≫ (α_ _ _ _).hom ≫ (𝟙_ C ◁ (ρ_ X).hom) :=
       by coherence
-    _ = (𝟙 (𝟙_ C) ⊗ (β_ (𝟙_ C) X).hom) ≫ (α_ _ _ _).inv ≫ ((β_ _ X).hom ⊗ 𝟙 _) ≫
-          ((β_ _ X).inv ⊗ 𝟙 _) ≫ (α_ _ _ _).hom ≫ (𝟙 (𝟙_ C) ⊗ (ρ_ X).hom) :=
-      by (slice_rhs 3 4 => rw [← comp_tensor_id, Iso.hom_inv_id, tensor_id]); rw [id_comp]
-    _ = (α_ _ _ _).inv ≫ (β_ _ _).hom ≫ (α_ _ _ _).inv ≫ ((β_ _ X).inv ⊗ 𝟙 _) ≫ (α_ _ _ _).hom ≫
-          (𝟙 (𝟙_ C) ⊗ (ρ_ X).hom) :=
+    _ = (𝟙_ C ◁ (β_ (𝟙_ C) X).hom) ≫ (α_ _ _ _).inv ≫ ((β_ _ X).hom ▷ _) ≫
+          ((β_ _ X).inv ▷ _) ≫ (α_ _ _ _).hom ≫ (𝟙_ C ◁ (ρ_ X).hom) :=
+      by simp
+    _ = (α_ _ _ _).inv ≫ (β_ _ _).hom ≫ (α_ _ _ _).inv ≫ ((β_ _ X).inv ▷ _) ≫ (α_ _ _ _).hom ≫
+          (𝟙_ C ◁ (ρ_ X).hom) :=
       by (slice_lhs 1 3 => rw [← hexagon_reverse]); simp only [assoc]
-    _ = (α_ _ _ _).inv ≫ (β_ _ _).hom ≫ (𝟙 X ⊗ (ρ_ _).hom) ≫ (β_ _ X).inv :=
+    _ = (α_ _ _ _).inv ≫ (β_ _ _).hom ≫ (X ◁ (ρ_ _).hom) ≫ (β_ _ X).inv :=
       by rw [braiding_rightUnitor_aux₁]
-    _ = (α_ _ _ _).inv ≫ ((ρ_ _).hom ⊗ 𝟙 _) ≫ (β_ _ X).hom ≫ (β_ _ _).inv :=
-      by (slice_lhs 2 3 => rw [← braiding_naturality]); simp only [assoc]
-    _ = (α_ _ _ _).inv ≫ ((ρ_ _).hom ⊗ 𝟙 _) := by rw [Iso.hom_inv_id, comp_id]
-    _ = 𝟙 (𝟙_ C) ⊗ (λ_ X).hom := by rw [triangle_assoc_comp_right]
+    _ = (α_ _ _ _).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']
 
 #align category_theory.braiding_right_unitor_aux₂ CategoryTheory.braiding_rightUnitor_aux₂
 
-@[simp]
+@[reassoc]
 theorem braiding_rightUnitor (X : C) : (β_ (𝟙_ C) X).hom ≫ (ρ_ X).hom = (λ_ X).hom := by
-  rw [← tensor_left_iff, id_tensor_comp, braiding_rightUnitor_aux₂]
+  rw [← whiskerLeft_iff, MonoidalCategory.whiskerLeft_comp, braiding_rightUnitor_aux₂]
 #align category_theory.braiding_right_unitor CategoryTheory.braiding_rightUnitor
 
-@[simp]
+@[reassoc, simp]
+theorem braiding_tensorUnit_left (X : C) : (β_ (𝟙_ C) X).hom = (λ_ X).hom ≫ (ρ_ X).inv := by
+  simp [← braiding_rightUnitor]
+
+@[reassoc]
 theorem leftUnitor_inv_braiding (X : C) : (λ_ X).inv ≫ (β_ (𝟙_ C) X).hom = (ρ_ X).inv := by
-  apply (cancel_mono (ρ_ X).hom).1
-  simp only [assoc, braiding_rightUnitor, Iso.inv_hom_id]
+  simp
 #align category_theory.left_unitor_inv_braiding CategoryTheory.leftUnitor_inv_braiding
 
-@[simp]
+@[reassoc]
 theorem rightUnitor_inv_braiding (X : C) : (ρ_ X).inv ≫ (β_ X (𝟙_ C)).hom = (λ_ X).inv := by
   apply (cancel_mono (λ_ X).hom).1
   simp only [assoc, braiding_leftUnitor, Iso.inv_hom_id]
 #align category_theory.right_unitor_inv_braiding CategoryTheory.rightUnitor_inv_braiding
 
+@[reassoc, simp]
+theorem braiding_tensorUnit_right (X : C) : (β_ X (𝟙_ C)).hom = (ρ_ X).hom ≫ (λ_ X).inv := by
+  simp [← rightUnitor_inv_braiding]
+
 end
 
 /--
@@ -448,30 +454,20 @@ end CommMonoid
 section Tensor
 
 /-- The strength of the tensor product functor from `C × C` to `C`. -/
-def tensor_μ (X Y : C × C) : (tensor C).obj X ⊗ (tensor C).obj Y ⟶ (tensor C).obj (X ⊗ Y) :=
+def tensor_μ (X Y : C × C) : (X.1 ⊗ X.2) ⊗ Y.1 ⊗ Y.2 ⟶ (X.1 ⊗ Y.1) ⊗ X.2 ⊗ Y.2 :=
   (α_ X.1 X.2 (Y.1 ⊗ Y.2)).hom ≫
-    (𝟙 X.1 ⊗ (α_ X.2 Y.1 Y.2).inv) ≫
-      (𝟙 X.1 ⊗ (β_ X.2 Y.1).hom ⊗ 𝟙 Y.2) ≫
-        (𝟙 X.1 ⊗ (α_ Y.1 X.2 Y.2).hom) ≫ (α_ X.1 Y.1 (X.2 ⊗ Y.2)).inv
+    (X.1 ◁ (α_ X.2 Y.1 Y.2).inv) ≫
+      (X.1 ◁ (β_ X.2 Y.1).hom ▷ Y.2) ≫
+        (X.1 ◁ (α_ Y.1 X.2 Y.2).hom) ≫ (α_ X.1 Y.1 (X.2 ⊗ Y.2)).inv
 #align category_theory.tensor_μ CategoryTheory.tensor_μ
 
-theorem tensor_μ_def₁ (X₁ X₂ Y₁ Y₂ : C) :
-    tensor_μ C (X₁, X₂) (Y₁, Y₂) ≫ (α_ X₁ Y₁ (X₂ ⊗ Y₂)).hom ≫ (𝟙 X₁ ⊗ (α_ Y₁ X₂ Y₂).inv) =
-      (α_ X₁ X₂ (Y₁ ⊗ Y₂)).hom ≫ (𝟙 X₁ ⊗ (α_ X₂ Y₁ Y₂).inv) ≫ (𝟙 X₁ ⊗ (β_ X₂ Y₁).hom ⊗ 𝟙 Y₂) :=
-  by dsimp [tensor_μ]; simp
-#align category_theory.tensor_μ_def₁ CategoryTheory.tensor_μ_def₁
-
-theorem tensor_μ_def₂ (X₁ X₂ Y₁ Y₂ : C) :
-    (𝟙 X₁ ⊗ (α_ X₂ Y₁ Y₂).hom) ≫ (α_ X₁ X₂ (Y₁ ⊗ Y₂)).inv ≫ tensor_μ C (X₁, X₂) (Y₁, Y₂) =
-      (𝟙 X₁ ⊗ (β_ X₂ Y₁).hom ⊗ 𝟙 Y₂) ≫ (𝟙 X₁ ⊗ (α_ Y₁ X₂ Y₂).hom) ≫ (α_ X₁ Y₁ (X₂ ⊗ Y₂)).inv :=
-  by dsimp [tensor_μ]; simp
-#align category_theory.tensor_μ_def₂ CategoryTheory.tensor_μ_def₂
-
+@[reassoc]
 theorem tensor_μ_natural {X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : U₁ ⟶ V₁)
     (g₂ : U₂ ⟶ V₂) :
     ((f₁ ⊗ f₂) ⊗ g₁ ⊗ g₂) ≫ tensor_μ C (Y₁, Y₂) (V₁, V₂) =
       tensor_μ C (X₁, X₂) (U₁, U₂) ≫ ((f₁ ⊗ g₁) ⊗ f₂ ⊗ g₂) := by
-  dsimp [tensor_μ]
+  dsimp only [tensor_μ]
+  simp_rw [← id_tensorHom, ← tensorHom_id]
   slice_lhs 1 2 => rw [associator_naturality]
   slice_lhs 2 3 =>
     rw [← tensor_comp, comp_id f₁, ← id_comp f₁, associator_inv_naturality, tensor_comp]
@@ -483,301 +479,142 @@ 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₂) =
-      tensor_μ C (X₁, X₂) (Z₁, Z₂) ≫ ((f₁ ⊗ 𝟙 Z₁) ⊗ (f₂ ⊗ 𝟙 Z₂)) := by
-  convert tensor_μ_natural C f₁ f₂ (𝟙 Z₁) (𝟙 Z₂) using 1; simp
+    (f₁ ⊗ f₂) ▷ (Z₁ ⊗ Z₂) ≫ tensor_μ C (Y₁, Y₂) (Z₁, Z₂) =
+      tensor_μ C (X₁, X₂) (Z₁, Z₂) ≫ (f₁ ▷ Z₁ ⊗ f₂ ▷ Z₂) := by
+  convert tensor_μ_natural C f₁ f₂ (𝟙 Z₁) (𝟙 Z₂) using 1 <;> simp
 
 @[reassoc]
 theorem tensor_μ_natural_right (Z₁ Z₂ : C) {X₁ X₂ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) :
-    (𝟙 (Z₁ ⊗ Z₂) ⊗ (f₁ ⊗ f₂)) ≫ tensor_μ C (Z₁, Z₂) (Y₁, Y₂) =
-      tensor_μ C (Z₁, Z₂) (X₁, X₂) ≫ ((𝟙 Z₁ ⊗ f₁) ⊗ (𝟙 Z₂ ⊗ f₂)) := by
-  convert tensor_μ_natural C (𝟙 Z₁) (𝟙 Z₂) f₁ f₂ using 1; simp
+    (Z₁ ⊗ Z₂) ◁ (f₁ ⊗ f₂) ≫ tensor_μ C (Z₁, Z₂) (Y₁, Y₂) =
+      tensor_μ C (Z₁, Z₂) (X₁, X₂) ≫ (Z₁ ◁ f₁ ⊗ Z₂ ◁ f₂) := by
+  convert tensor_μ_natural C (𝟙 Z₁) (𝟙 Z₂) f₁ f₂ using 1 <;> simp
 
+@[reassoc]
 theorem tensor_left_unitality (X₁ X₂ : C) :
     (λ_ (X₁ ⊗ X₂)).hom =
-      ((λ_ (𝟙_ C)).inv ⊗ 𝟙 (X₁ ⊗ X₂)) ≫
+      ((λ_ (𝟙_ C)).inv ▷ (X₁ ⊗ X₂)) ≫
         tensor_μ C (𝟙_ C, 𝟙_ C) (X₁, X₂) ≫ ((λ_ X₁).hom ⊗ (λ_ X₂).hom) := by
-  dsimp [tensor_μ]
+  dsimp only [tensor_μ]
   have :
-    ((λ_ (𝟙_ C)).inv ⊗ 𝟙 (X₁ ⊗ X₂)) ≫
-        (α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).hom ≫ (𝟙 (𝟙_ C) ⊗ (α_ (𝟙_ C) X₁ X₂).inv) =
-      𝟙 (𝟙_ C) ⊗ (λ_ X₁).inv ⊗ 𝟙 X₂ :=
-    by pure_coherence
+    ((λ_ (𝟙_ C)).inv ▷ (X₁ ⊗ X₂)) ≫
+        (α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).hom ≫ (𝟙_ C ◁ (α_ (𝟙_ C) X₁ X₂).inv) =
+      𝟙_ C ◁ (λ_ X₁).inv ▷ X₂ :=
+    by coherence
   slice_rhs 1 3 => rw [this]
   clear this
-  slice_rhs 1 2 => rw [← tensor_comp, ← tensor_comp, comp_id, comp_id, leftUnitor_inv_braiding]
-  simp only [assoc]
-  coherence
+  slice_rhs 1 2 => rw [← MonoidalCategory.whiskerLeft_comp, ← comp_whiskerRight,
+    leftUnitor_inv_braiding]
+  simp [tensorHom_id, id_tensorHom, tensorHom_def]
 #align category_theory.tensor_left_unitality CategoryTheory.tensor_left_unitality
 
+@[reassoc]
 theorem tensor_right_unitality (X₁ X₂ : C) :
     (ρ_ (X₁ ⊗ X₂)).hom =
-      (𝟙 (X₁ ⊗ X₂) ⊗ (λ_ (𝟙_ C)).inv) ≫
+      ((X₁ ⊗ X₂) ◁ (λ_ (𝟙_ C)).inv) ≫
         tensor_μ C (X₁, X₂) (𝟙_ C, 𝟙_ C) ≫ ((ρ_ X₁).hom ⊗ (ρ_ X₂).hom) := by
-  dsimp [tensor_μ]
+  dsimp only [tensor_μ]
   have :
-    (𝟙 (X₁ ⊗ X₂) ⊗ (λ_ (𝟙_ C)).inv) ≫
-        (α_ X₁ X₂ (𝟙_ C ⊗ 𝟙_ C)).hom ≫ (𝟙 X₁ ⊗ (α_ X₂ (𝟙_ C) (𝟙_ C)).inv) =
-      (α_ X₁ X₂ (𝟙_ C)).hom ≫ (𝟙 X₁ ⊗ (ρ_ X₂).inv ⊗ 𝟙 (𝟙_ C)) :=
-    by pure_coherence
+    ((X₁ ⊗ X₂) ◁ (λ_ (𝟙_ C)).inv) ≫
+        (α_ X₁ X₂ (𝟙_ C ⊗ 𝟙_ C)).hom ≫ (X₁ ◁ (α_ X₂ (𝟙_ C) (𝟙_ C)).inv) =
+      (α_ X₁ X₂ (𝟙_ C)).hom ≫ (X₁ ◁ (ρ_ X₂).inv ▷ 𝟙_ C) :=
+    by coherence
   slice_rhs 1 3 => rw [this]
   clear this
-  slice_rhs 2 3 => rw [← tensor_comp, ← tensor_comp, comp_id, comp_id, rightUnitor_inv_braiding]
-  simp only [assoc]
-  coherence
+  slice_rhs 2 3 => rw [← MonoidalCategory.whiskerLeft_comp, ← comp_whiskerRight,
+    rightUnitor_inv_braiding]
+  simp [tensorHom_id, id_tensorHom, tensorHom_def]
 #align category_theory.tensor_right_unitality CategoryTheory.tensor_right_unitality
 
-/-
-Diagram B6 from Proposition 1 of [Joyal and Street, *Braided monoidal categories*][Joyal_Street].
--/
-theorem tensor_associativity_aux (W X Y Z : C) :
-    ((β_ W X).hom ⊗ 𝟙 (Y ⊗ Z)) ≫
-        (α_ X W (Y ⊗ Z)).hom ≫
-          (𝟙 X ⊗ (α_ W Y Z).inv) ≫ (𝟙 X ⊗ (β_ (W ⊗ Y) Z).hom) ≫ (𝟙 X ⊗ (α_ Z W Y).inv) =
-      (𝟙 (W ⊗ X) ⊗ (β_ Y Z).hom) ≫
-        (α_ (W ⊗ X) Z Y).inv ≫
-          ((α_ W X Z).hom ⊗ 𝟙 Y) ≫
-            ((β_ W (X ⊗ Z)).hom ⊗ 𝟙 Y) ≫ ((α_ X Z W).hom ⊗ 𝟙 Y) ≫ (α_ X (Z ⊗ W) Y).hom := by
-  slice_rhs 3 5 => rw [← tensor_comp, ← tensor_comp, hexagon_forward, tensor_comp, tensor_comp]
-  slice_rhs 5 6 => rw [associator_naturality]
-  slice_rhs 2 3 => rw [← associator_inv_naturality]
-  slice_rhs 3 5 => rw [← pentagon_hom_inv]
-  slice_rhs 1 2 => rw [tensor_id, id_tensor_comp_tensor_id, ← tensor_id_comp_id_tensor]
-  slice_rhs 2 3 => rw [← tensor_id, associator_naturality]
-  slice_rhs 3 5 => rw [← tensor_comp, ← tensor_comp, ← hexagon_reverse, tensor_comp, tensor_comp]
-#align category_theory.tensor_associativity_aux CategoryTheory.tensor_associativity_aux
-
-set_option maxHeartbeats 400000 in
 theorem tensor_associativity (X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C) :
-    (tensor_μ C (X₁, X₂) (Y₁, Y₂) ⊗ 𝟙 (Z₁ ⊗ Z₂)) ≫
+    (tensor_μ C (X₁, X₂) (Y₁, Y₂) ▷ (Z₁ ⊗ Z₂)) ≫
         tensor_μ C (X₁ ⊗ Y₁, X₂ ⊗ Y₂) (Z₁, Z₂) ≫ ((α_ X₁ Y₁ Z₁).hom ⊗ (α_ X₂ Y₂ Z₂).hom) =
       (α_ (X₁ ⊗ X₂) (Y₁ ⊗ Y₂) (Z₁ ⊗ Z₂)).hom ≫
-        (𝟙 (X₁ ⊗ X₂) ⊗ tensor_μ C (Y₁, Y₂) (Z₁, Z₂)) ≫ tensor_μ C (X₁, X₂) (Y₁ ⊗ Z₁, Y₂ ⊗ Z₂) := by
-  have :
-    (α_ X₁ Y₁ Z₁).hom ⊗ (α_ X₂ Y₂ Z₂).hom =
-      (α_ (X₁ ⊗ Y₁) Z₁ ((X₂ ⊗ Y₂) ⊗ Z₂)).hom ≫
-        (𝟙 (X₁ ⊗ Y₁) ⊗ (α_ Z₁ (X₂ ⊗ Y₂) Z₂).inv) ≫
-          (α_ X₁ Y₁ ((Z₁ ⊗ X₂ ⊗ Y₂) ⊗ Z₂)).hom ≫
-            (𝟙 X₁ ⊗ (α_ Y₁ (Z₁ ⊗ X₂ ⊗ Y₂) Z₂).inv) ≫
-              (α_ X₁ (Y₁ ⊗ Z₁ ⊗ X₂ ⊗ Y₂) Z₂).inv ≫
-                ((𝟙 X₁ ⊗ 𝟙 Y₁ ⊗ (α_ Z₁ X₂ Y₂).inv) ⊗ 𝟙 Z₂) ≫
-                  ((𝟙 X₁ ⊗ (α_ Y₁ (Z₁ ⊗ X₂) Y₂).inv) ⊗ 𝟙 Z₂) ≫
-                    ((𝟙 X₁ ⊗ (α_ Y₁ Z₁ X₂).inv ⊗ 𝟙 Y₂) ⊗ 𝟙 Z₂) ≫
-                      (α_ X₁ (((Y₁ ⊗ Z₁) ⊗ X₂) ⊗ Y₂) Z₂).hom ≫
-                        (𝟙 X₁ ⊗ (α_ ((Y₁ ⊗ Z₁) ⊗ X₂) Y₂ Z₂).hom) ≫
-                          (𝟙 X₁ ⊗ (α_ (Y₁ ⊗ Z₁) X₂ (Y₂ ⊗ Z₂)).hom) ≫
-                            (α_ X₁ (Y₁ ⊗ Z₁) (X₂ ⊗ Y₂ ⊗ Z₂)).inv :=
-    by pure_coherence
-  rw [this]; clear this
-  slice_lhs 2 4 => rw [tensor_μ_def₁]
-  slice_lhs 4 5 => rw [← tensor_id, associator_naturality]
-  slice_lhs 5 6 => rw [← tensor_comp, associator_inv_naturality, tensor_comp]
-  slice_lhs 6 7 => rw [associator_inv_naturality]
-  have :
-    (α_ (X₁ ⊗ Y₁) (X₂ ⊗ Y₂) (Z₁ ⊗ Z₂)).hom ≫
-        (𝟙 (X₁ ⊗ Y₁) ⊗ (α_ (X₂ ⊗ Y₂) Z₁ Z₂).inv) ≫
-          (α_ X₁ Y₁ (((X₂ ⊗ Y₂) ⊗ Z₁) ⊗ Z₂)).hom ≫
-            (𝟙 X₁ ⊗ (α_ Y₁ ((X₂ ⊗ Y₂) ⊗ Z₁) Z₂).inv) ≫ (α_ X₁ (Y₁ ⊗ (X₂ ⊗ Y₂) ⊗ Z₁) Z₂).inv =
-      ((α_ X₁ Y₁ (X₂ ⊗ Y₂)).hom ⊗ 𝟙 (Z₁ ⊗ Z₂)) ≫
-        ((𝟙 X₁ ⊗ (α_ Y₁ X₂ Y₂).inv) ⊗ 𝟙 (Z₁ ⊗ Z₂)) ≫
-          (α_ (X₁ ⊗ (Y₁ ⊗ X₂) ⊗ Y₂) Z₁ Z₂).inv ≫
-            ((α_ X₁ ((Y₁ ⊗ X₂) ⊗ Y₂) Z₁).hom ⊗ 𝟙 Z₂) ≫
-              ((𝟙 X₁ ⊗ (α_ (Y₁ ⊗ X₂) Y₂ Z₁).hom) ⊗ 𝟙 Z₂) ≫
-                ((𝟙 X₁ ⊗ (α_ Y₁ X₂ (Y₂ ⊗ Z₁)).hom) ⊗ 𝟙 Z₂) ≫
-                  ((𝟙 X₁ ⊗ 𝟙 Y₁ ⊗ (α_ X₂ Y₂ Z₁).inv) ⊗ 𝟙 Z₂) :=
-    by pure_coherence
-  slice_lhs 2 6 => rw [this]
-  clear this
-  slice_lhs 1 3 => rw [← tensor_comp, ← tensor_comp, tensor_μ_def₁, tensor_comp, tensor_comp]
-  slice_lhs 3 4 => rw [← tensor_id, associator_inv_naturality]
-  slice_lhs 4 5 => rw [← tensor_comp, associator_naturality, tensor_comp]
-  slice_lhs 5 6 =>
-    rw [← tensor_comp, ← tensor_comp, associator_naturality, tensor_comp, tensor_comp]
-  slice_lhs 6 10 =>
-    rw [← tensor_comp, ← tensor_comp, ← tensor_comp, ← tensor_comp, ← tensor_comp, ← tensor_comp, ←
-      tensor_comp, ← tensor_comp, tensor_id, tensor_associativity_aux, ← tensor_id, ←
-      id_comp (𝟙 X₁ ≫ 𝟙 X₁ ≫ 𝟙 X₁ ≫ 𝟙 X₁ ≫ 𝟙 X₁), ← id_comp (𝟙 Z₂ ≫ 𝟙 Z₂ ≫ 𝟙 Z₂ ≫ 𝟙 Z₂ ≫ 𝟙 Z₂),
-      tensor_comp, tensor_comp, tensor_comp, tensor_comp, tensor_comp, tensor_comp, tensor_comp,
-      tensor_comp, tensor_comp, tensor_comp]
-  slice_lhs 11 12 =>
-    rw [← tensor_comp, ← tensor_comp, Iso.hom_inv_id]
-    simp
-  simp only [assoc, id_comp]
-  slice_lhs 10 11 =>
-    rw [← tensor_comp, ← tensor_comp, ← tensor_comp, Iso.hom_inv_id]
-    simp
-  simp only [assoc, id_comp]
-  slice_lhs 9 10 => rw [associator_naturality]
-  slice_lhs 10 11 => rw [← tensor_comp, associator_naturality, tensor_comp]
-  slice_lhs 11 13 => rw [tensor_id, ← tensor_μ_def₂]
-  have :
-    ((𝟙 X₁ ⊗ (α_ (X₂ ⊗ Y₁) Z₁ Y₂).inv) ⊗ 𝟙 Z₂) ≫
-        ((𝟙 X₁ ⊗ (α_ X₂ Y₁ Z₁).hom ⊗ 𝟙 Y₂) ⊗ 𝟙 Z₂) ≫
-          (α_ X₁ ((X₂ ⊗ Y₁ ⊗ Z₁) ⊗ Y₂) Z₂).hom ≫
-            (𝟙 X₁ ⊗ (α_ (X₂ ⊗ Y₁ ⊗ Z₁) Y₂ Z₂).hom) ≫
-              (𝟙 X₁ ⊗ (α_ X₂ (Y₁ ⊗ Z₁) (Y₂ ⊗ Z₂)).hom) ≫ (α_ X₁ X₂ ((Y₁ ⊗ Z₁) ⊗ Y₂ ⊗ Z₂)).inv =
-      (α_ X₁ ((X₂ ⊗ Y₁) ⊗ Z₁ ⊗ Y₂) Z₂).hom ≫
-        (𝟙 X₁ ⊗ (α_ (X₂ ⊗ Y₁) (Z₁ ⊗ Y₂) Z₂).hom) ≫
-          (𝟙 X₁ ⊗ (α_ X₂ Y₁ ((Z₁ ⊗ Y₂) ⊗ Z₂)).hom) ≫
-            (α_ X₁ X₂ (Y₁ ⊗ (Z₁ ⊗ Y₂) ⊗ Z₂)).inv ≫
-              (𝟙 (X₁ ⊗ X₂) ⊗ 𝟙 Y₁ ⊗ (α_ Z₁ Y₂ Z₂).hom) ≫ (𝟙 (X₁ ⊗ X₂) ⊗ (α_ Y₁ Z₁ (Y₂ ⊗ Z₂)).inv) :=
-    by pure_coherence
-  slice_lhs 7 12 => rw [this]
-  clear this
-  slice_lhs 6 7 => rw [associator_naturality]
-  slice_lhs 7 8 => rw [← tensor_comp, associator_naturality, tensor_comp]
-  slice_lhs 8 9 => rw [← tensor_comp, associator_naturality, tensor_comp]
-  slice_lhs 9 10 => rw [associator_inv_naturality]
-  slice_lhs 10 12 => rw [← tensor_comp, ← tensor_comp, ← tensor_μ_def₂, tensor_comp, tensor_comp]
-  dsimp
-  coherence
+        ((X₁ ⊗ X₂) ◁ tensor_μ C (Y₁, Y₂) (Z₁, Z₂)) ≫ tensor_μ C (X₁, X₂) (Y₁ ⊗ Z₁, Y₂ ⊗ Z₂) := by
+  dsimp only [tensor_obj, prodMonoidal_tensorObj, tensor_μ]
+  simp only [whiskerRight_tensor, comp_whiskerRight, whisker_assoc, assoc, Iso.inv_hom_id_assoc,
+    tensor_whiskerLeft, braiding_tensor_left, MonoidalCategory.whiskerLeft_comp,
+    braiding_tensor_right]
+  calc
+    _ = 𝟙 _ ⊗≫
+      X₁ ◁ ((β_ X₂ Y₁).hom ▷ (Y₂ ⊗ Z₁) ≫ (Y₁ ⊗ X₂) ◁ (β_ Y₂ Z₁).hom) ▷ Z₂ ⊗≫
+        X₁ ◁ Y₁ ◁ (β_ X₂ Z₁).hom ▷ Y₂ ▷ Z₂ ⊗≫ 𝟙 _ := by coherence
+    _ = _ := by rw [← whisker_exchange]; coherence
 #align category_theory.tensor_associativity CategoryTheory.tensor_associativity
 
+-- We got a timeout if `reassoc` was at the declaration, so we put it here instead.
+attribute [reassoc] tensor_associativity
+
 /-- The tensor product functor from `C × C` to `C` as a monoidal functor. -/
 @[simps!]
 def tensorMonoidal : MonoidalFunctor (C × C) C :=
   { tensor C with
     ε := (λ_ (𝟙_ C)).inv
     μ := tensor_μ C
-    μ_natural_left := fun f Z => tensor_μ_natural_left C f.1 f.2 Z.1 Z.2
-    μ_natural_right := fun Z f => tensor_μ_natural_right C Z.1 Z.2 f.1 f.2
-    associativity := fun X Y Z => tensor_associativity C X.1 X.2 Y.1 Y.2 Z.1 Z.2
-    left_unitality := fun ⟨X₁, X₂⟩ => tensor_left_unitality C X₁ X₂
-    right_unitality := fun ⟨X₁, X₂⟩ => tensor_right_unitality C X₁ X₂
+    μ_natural_left := fun f Z => by
+      -- `simpa` will be not needed when we define `μ_natural_left` in terms of the whiskerings.
+      simpa using tensor_μ_natural_left C f.1 f.2 Z.1 Z.2
+    μ_natural_right := fun Z f => by
+      simpa using tensor_μ_natural_right C Z.1 Z.2 f.1 f.2
+    associativity := fun X Y Z => by
+      simpa using tensor_associativity C X.1 X.2 Y.1 Y.2 Z.1 Z.2
+    left_unitality := fun ⟨X₁, X₂⟩ => by
+      simpa using tensor_left_unitality C X₁ X₂
+    right_unitality := fun ⟨X₁, X₂⟩ => by
+      simpa using tensor_right_unitality C X₁ X₂
     μ_isIso := by dsimp [tensor_μ]; infer_instance }
-#align category_theory.tensor_monoidal CategoryTheory.tensorMonoidal
 
+@[reassoc]
 theorem leftUnitor_monoidal (X₁ X₂ : C) :
     (λ_ X₁).hom ⊗ (λ_ X₂).hom =
-      tensor_μ C (𝟙_ C, X₁) (𝟙_ C, X₂) ≫ ((λ_ (𝟙_ C)).hom ⊗ 𝟙 (X₁ ⊗ X₂)) ≫ (λ_ (X₁ ⊗ X₂)).hom := by
-  dsimp [tensor_μ]
+      tensor_μ C (𝟙_ C, X₁) (𝟙_ C, X₂) ≫ ((λ_ (𝟙_ C)).hom ▷ (X₁ ⊗ X₂)) ≫ (λ_ (X₁ ⊗ X₂)).hom := by
+  dsimp only [tensor_μ]
   have :
     (λ_ X₁).hom ⊗ (λ_ X₂).hom =
       (α_ (𝟙_ C) X₁ (𝟙_ C ⊗ X₂)).hom ≫
-        (𝟙 (𝟙_ C) ⊗ (α_ X₁ (𝟙_ C) X₂).inv) ≫ (λ_ ((X₁ ⊗ 𝟙_ C) ⊗ X₂)).hom ≫ ((ρ_ X₁).hom ⊗ 𝟙 X₂) :=
-    by pure_coherence
+        (𝟙_ C ◁ (α_ X₁ (𝟙_ C) X₂).inv) ≫ (λ_ ((X₁ ⊗ 𝟙_ C) ⊗ X₂)).hom ≫ ((ρ_ X₁).hom ▷ X₂) :=
+    by coherence
   rw [this]; clear this
   rw [← braiding_leftUnitor]
-  slice_lhs 3 4 => rw [← id_comp (𝟙 X₂), tensor_comp]
-  slice_lhs 3 4 => rw [← leftUnitor_naturality]
+  dsimp only [tensor_obj, prodMonoidal_tensorObj]
   coherence
 #align category_theory.left_unitor_monoidal CategoryTheory.leftUnitor_monoidal
 
+@[reassoc]
 theorem rightUnitor_monoidal (X₁ X₂ : C) :
     (ρ_ X₁).hom ⊗ (ρ_ X₂).hom =
-      tensor_μ C (X₁, 𝟙_ C) (X₂, 𝟙_ C) ≫ (𝟙 (X₁ ⊗ X₂) ⊗ (λ_ (𝟙_ C)).hom) ≫ (ρ_ (X₁ ⊗ X₂)).hom := by
-  dsimp [tensor_μ]
+      tensor_μ C (X₁, 𝟙_ C) (X₂, 𝟙_ C) ≫ ((X₁ ⊗ X₂) ◁ (λ_ (𝟙_ C)).hom) ≫ (ρ_ (X₁ ⊗ X₂)).hom := by
+  dsimp only [tensor_μ]
   have :
     (ρ_ X₁).hom ⊗ (ρ_ X₂).hom =
       (α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).hom ≫
-        (𝟙 X₁ ⊗ (α_ (𝟙_ C) X₂ (𝟙_ C)).inv) ≫ (𝟙 X₁ ⊗ (ρ_ (𝟙_ C ⊗ X₂)).hom) ≫ (𝟙 X₁ ⊗ (λ_ X₂).hom) :=
-    by pure_coherence
+        (X₁ ◁ (α_ (𝟙_ C) X₂ (𝟙_ C)).inv) ≫ (X₁ ◁ (ρ_ (𝟙_ C ⊗ X₂)).hom) ≫ (X₁ ◁ (λ_ X₂).hom) :=
+    by coherence
   rw [this]; clear this
   rw [← braiding_rightUnitor]
-  slice_lhs 3 4 => rw [← id_comp (𝟙 X₁), tensor_comp, id_comp]
-  slice_lhs 3 4 => rw [← tensor_comp, ← rightUnitor_naturality, tensor_comp]
+  dsimp only [tensor_obj, prodMonoidal_tensorObj]
   coherence
 #align category_theory.right_unitor_monoidal CategoryTheory.rightUnitor_monoidal
 
-theorem associator_monoidal_aux (W X Y Z : C) :
-    (𝟙 W ⊗ (β_ X (Y ⊗ Z)).hom) ≫
-        (𝟙 W ⊗ (α_ Y Z X).hom) ≫ (α_ W Y (Z ⊗ X)).inv ≫ ((β_ W Y).hom ⊗ 𝟙 (Z ⊗ X)) =
-      (α_ W X (Y ⊗ Z)).inv ≫
-        (α_ (W ⊗ X) Y Z).inv ≫
-          ((β_ (W ⊗ X) Y).hom ⊗ 𝟙 Z) ≫
-            ((α_ Y W X).inv ⊗ 𝟙 Z) ≫ (α_ (Y ⊗ W) X Z).hom ≫ (𝟙 (Y ⊗ W) ⊗ (β_ X Z).hom) := by
-  slice_rhs 1 2 => rw [← pentagon_inv]
-  slice_rhs 3 5 => rw [← tensor_comp, ← tensor_comp, hexagon_reverse, tensor_comp, tensor_comp]
-  slice_rhs 5 6 => rw [associator_naturality]
-  slice_rhs 6 7 => rw [tensor_id, tensor_id_comp_id_tensor, ← id_tensor_comp_tensor_id]
-  slice_rhs 2 3 => rw [← associator_inv_naturality]
-  slice_rhs 3 5 => rw [pentagon_inv_inv_hom]
-  slice_rhs 4 5 => rw [← tensor_id, ← associator_inv_naturality]
-  slice_rhs 2 4 => rw [← tensor_comp, ← tensor_comp, ← hexagon_forward, tensor_comp, tensor_comp]
-  simp
-#align category_theory.associator_monoidal_aux CategoryTheory.associator_monoidal_aux
-
-set_option maxHeartbeats 400000 in
 theorem associator_monoidal (X₁ X₂ X₃ Y₁ Y₂ Y₃ : C) :
     tensor_μ C (X₁ ⊗ X₂, X₃) (Y₁ ⊗ Y₂, Y₃) ≫
-        (tensor_μ C (X₁, X₂) (Y₁, Y₂) ⊗ 𝟙 (X₃ ⊗ Y₃)) ≫ (α_ (X₁ ⊗ Y₁) (X₂ ⊗ Y₂) (X₃ ⊗ Y₃)).hom =
+        (tensor_μ C (X₁, X₂) (Y₁, Y₂) ▷ (X₃ ⊗ Y₃)) ≫ (α_ (X₁ ⊗ Y₁) (X₂ ⊗ Y₂) (X₃ ⊗ Y₃)).hom =
       ((α_ X₁ X₂ X₃).hom ⊗ (α_ Y₁ Y₂ Y₃).hom) ≫
-        tensor_μ C (X₁, X₂ ⊗ X₃) (Y₁, Y₂ ⊗ Y₃) ≫ (𝟙 (X₁ ⊗ Y₁) ⊗ tensor_μ C (X₂, X₃) (Y₂, Y₃)) := by
-  have :
-    (α_ (X₁ ⊗ Y₁) (X₂ ⊗ Y₂) (X₃ ⊗ Y₃)).hom =
-      ((α_ X₁ Y₁ (X₂ ⊗ Y₂)).hom ⊗ 𝟙 (X₃ ⊗ Y₃)) ≫
-        ((𝟙 X₁ ⊗ (α_ Y₁ X₂ Y₂).inv) ⊗ 𝟙 (X₃ ⊗ Y₃)) ≫
-          (α_ (X₁ ⊗ (Y₁ ⊗ X₂) ⊗ Y₂) X₃ Y₃).inv ≫
-            ((α_ X₁ ((Y₁ ⊗ X₂) ⊗ Y₂) X₃).hom ⊗ 𝟙 Y₃) ≫
-              ((𝟙 X₁ ⊗ (α_ (Y₁ ⊗ X₂) Y₂ X₃).hom) ⊗ 𝟙 Y₃) ≫
-                (α_ X₁ ((Y₁ ⊗ X₂) ⊗ Y₂ ⊗ X₃) Y₃).hom ≫
-                  (𝟙 X₁ ⊗ (α_ (Y₁ ⊗ X₂) (Y₂ ⊗ X₃) Y₃).hom) ≫
-                    (𝟙 X₁ ⊗ (α_ Y₁ X₂ ((Y₂ ⊗ X₃) ⊗ Y₃)).hom) ≫
-                      (α_ X₁ Y₁ (X₂ ⊗ (Y₂ ⊗ X₃) ⊗ Y₃)).inv ≫
-                        (𝟙 (X₁ ⊗ Y₁) ⊗ 𝟙 X₂ ⊗ (α_ Y₂ X₃ Y₃).hom) ≫
-                          (𝟙 (X₁ ⊗ Y₁) ⊗ (α_ X₂ Y₂ (X₃ ⊗ Y₃)).inv) :=
-    by pure_coherence
-  rw [this]; clear this
-  slice_lhs 2 4 => rw [← tensor_comp, ← tensor_comp, tensor_μ_def₁, tensor_comp, tensor_comp]
-  slice_lhs 4 5 => rw [← tensor_id, associator_inv_naturality]
-  slice_lhs 5 6 => rw [← tensor_comp, associator_naturality, tensor_comp]
-  slice_lhs 6 7 =>
-    rw [← tensor_comp, ← tensor_comp, associator_naturality, tensor_comp, tensor_comp]
-  have :
-    ((α_ X₁ X₂ (Y₁ ⊗ Y₂)).hom ⊗ 𝟙 (X₃ ⊗ Y₃)) ≫
-        ((𝟙 X₁ ⊗ (α_ X₂ Y₁ Y₂).inv) ⊗ 𝟙 (X₃ ⊗ Y₃)) ≫
-          (α_ (X₁ ⊗ (X₂ ⊗ Y₁) ⊗ Y₂) X₃ Y₃).inv ≫
-            ((α_ X₁ ((X₂ ⊗ Y₁) ⊗ Y₂) X₃).hom ⊗ 𝟙 Y₃) ≫ ((𝟙 X₁ ⊗ (α_ (X₂ ⊗ Y₁) Y₂ X₃).hom) ⊗ 𝟙 Y₃) =
-      (α_ (X₁ ⊗ X₂) (Y₁ ⊗ Y₂) (X₃ ⊗ Y₃)).hom ≫
-        (𝟙 (X₁ ⊗ X₂) ⊗ (α_ (Y₁ ⊗ Y₂) X₃ Y₃).inv) ≫
-          (α_ X₁ X₂ (((Y₁ ⊗ Y₂) ⊗ X₃) ⊗ Y₃)).hom ≫
-            (𝟙 X₁ ⊗ (α_ X₂ ((Y₁ ⊗ Y₂) ⊗ X₃) Y₃).inv) ≫
-              (α_ X₁ (X₂ ⊗ (Y₁ ⊗ Y₂) ⊗ X₃) Y₃).inv ≫
-                ((𝟙 X₁ ⊗ 𝟙 X₂ ⊗ (α_ Y₁ Y₂ X₃).hom) ⊗ 𝟙 Y₃) ≫
-                  ((𝟙 X₁ ⊗ (α_ X₂ Y₁ (Y₂ ⊗ X₃)).inv) ⊗ 𝟙 Y₃) :=
-    by pure_coherence
-  slice_lhs 2 6 => rw [this]
-  clear this
-  slice_lhs 1 3 => rw [tensor_μ_def₁]
-  slice_lhs 3 4 => rw [← tensor_id, associator_naturality]
-  slice_lhs 4 5 => rw [← tensor_comp, associator_inv_naturality, tensor_comp]
-  slice_lhs 5 6 => rw [associator_inv_naturality]
-  slice_lhs 6 9 =>
-    rw [← tensor_comp, ← tensor_comp, ← tensor_comp, ← tensor_comp, ← tensor_comp, ← tensor_comp,
-      tensor_id, associator_monoidal_aux, ← id_comp (𝟙 X₁ ≫ 𝟙 X₁ ≫ 𝟙 X₁ ≫ 𝟙 X₁), ←
-      id_comp (𝟙 X₁ ≫ 𝟙 X₁ ≫ 𝟙 X₁ ≫ 𝟙 X₁ ≫ 𝟙 X₁), ← id_comp (𝟙 Y₃ ≫ 𝟙 Y₃ ≫ 𝟙 Y₃ ≫ 𝟙 Y₃), ←
-      id_comp (𝟙 Y₃ ≫ 𝟙 Y₃ ≫ 𝟙 Y₃ ≫ 𝟙 Y₃ ≫ 𝟙 Y₃), tensor_comp, tensor_comp, tensor_comp,
-      tensor_comp, tensor_comp, tensor_comp, tensor_comp, tensor_comp, tensor_comp, tensor_comp]
-  slice_lhs 11 12 => rw [associator_naturality]
-  slice_lhs 12 13 => rw [← tensor_comp, associator_naturality, tensor_comp]
-  slice_lhs 13 14 => rw [← tensor_comp, ← tensor_id, associator_naturality, tensor_comp]
-  slice_lhs 14 15 => rw [associator_inv_naturality]
-  slice_lhs 15 17 =>
-    rw [tensor_id, ← tensor_comp, ← tensor_comp, ← tensor_μ_def₂, tensor_comp, tensor_comp]
-  have :
-    ((𝟙 X₁ ⊗ (α_ Y₁ X₂ X₃).inv ⊗ 𝟙 Y₂) ⊗ 𝟙 Y₃) ≫
-        ((𝟙 X₁ ⊗ (α_ (Y₁ ⊗ X₂) X₃ Y₂).hom) ⊗ 𝟙 Y₃) ≫
-          (α_ X₁ ((Y₁ ⊗ X₂) ⊗ X₃ ⊗ Y₂) Y₃).hom ≫
-            (𝟙 X₁ ⊗ (α_ (Y₁ ⊗ X₂) (X₃ ⊗ Y₂) Y₃).hom) ≫
-              (𝟙 X₁ ⊗ (α_ Y₁ X₂ ((X₃ ⊗ Y₂) ⊗ Y₃)).hom) ≫
-                (α_ X₁ Y₁ (X₂ ⊗ (X₃ ⊗ Y₂) ⊗ Y₃)).inv ≫
-                  (𝟙 (X₁ ⊗ Y₁) ⊗ 𝟙 X₂ ⊗ (α_ X₃ Y₂ Y₃).hom) ≫
-                    (𝟙 (X₁ ⊗ Y₁) ⊗ (α_ X₂ X₃ (Y₂ ⊗ Y₃)).inv) =
-      (α_ X₁ ((Y₁ ⊗ X₂ ⊗ X₃) ⊗ Y₂) Y₃).hom ≫
-        (𝟙 X₁ ⊗ (α_ (Y₁ ⊗ X₂ ⊗ X₃) Y₂ Y₃).hom) ≫
-          (𝟙 X₁ ⊗ (α_ Y₁ (X₂ ⊗ X₃) (Y₂ ⊗ Y₃)).hom) ≫ (α_ X₁ Y₁ ((X₂ ⊗ X₃) ⊗ Y₂ ⊗ Y₃)).inv :=
-    by pure_coherence
-  slice_lhs 9 16 => rw [this]
-  clear this
-  slice_lhs 8 9 => rw [associator_naturality]
-  slice_lhs 9 10 => rw [← tensor_comp, associator_naturality, tensor_comp]
-  slice_lhs 10 12 => rw [tensor_id, ← tensor_μ_def₂]
-  dsimp
-  coherence
+        tensor_μ C (X₁, X₂ ⊗ X₃) (Y₁, Y₂ ⊗ Y₃) ≫ ((X₁ ⊗ Y₁) ◁ tensor_μ C (X₂, X₃) (Y₂, Y₃)) := by
+  dsimp only [tensor_μ]
+  calc
+    _ = 𝟙 _ ⊗≫ X₁ ◁ X₂ ◁ (β_ X₃ Y₁).hom ▷ Y₂ ▷ Y₃ ⊗≫
+      X₁ ◁ ((X₂ ⊗ Y₁) ◁ (β_ X₃ Y₂).hom ≫
+        (β_ X₂ Y₁).hom ▷ (Y₂ ⊗ X₃)) ▷ Y₃ ⊗≫ 𝟙 _ := by simp; coherence
+    _ = _ := by rw [whisker_exchange]; simp; coherence
 #align category_theory.associator_monoidal CategoryTheory.associator_monoidal
 
+-- We got a timeout if `reassoc` was at the declaration, so we put it here instead.
+attribute [reassoc] associator_monoidal
+
 end Tensor
 
 end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Monoidal/Category.lean b/Mathlib/CategoryTheory/Monoidal/Category.lean
index 7ffcd258802f9..291e3bc93eb1b 100644
--- a/Mathlib/CategoryTheory/Monoidal/Category.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Category.lean
@@ -463,18 +463,30 @@ theorem associator_inv_naturality_right (X Y : C) {Z Z' : C} (f : Z ⟶ Z') :
 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) :
-    f ≫ (λ_ Y).inv = (λ_ X).inv ≫ (_ ◁ f) := by simp
+    f ≫ (λ_ Y).inv = (λ_ X).inv ≫ _ ◁ f := by simp
 
+@[reassoc]
 theorem id_whiskerLeft_symm {X X' : C} (f : X ⟶ X') :
     f = (λ_ X).inv ≫ 𝟙_ C ◁ f ≫ (λ_ X').hom := by
   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') :
-    f ≫ (ρ_ X').inv = (ρ_ X).inv ≫ (f ▷ _) := by simp
+    f ≫ (ρ_ X').inv = (ρ_ X).inv ≫ f ▷ _ := by simp
 
+@[reassoc]
 theorem whiskerRight_id_symm {X Y : C} (f : X ⟶ Y) :
     f = (ρ_ X).inv ≫ f ▷ 𝟙_ C ≫ (ρ_ Y).hom := by
   simp
@@ -823,16 +835,6 @@ theorem leftUnitor_conjugation {X Y : C} (f : X ⟶ Y) :
   simp
 #align category_theory.monoidal_category.left_unitor_conjugation CategoryTheory.MonoidalCategory.leftUnitor_conjugation
 
-@[reassoc]
-theorem leftUnitor_naturality' {X Y : C} (f : X ⟶ Y) :
-    (𝟙 (𝟙_ C) ⊗ f) ≫ (λ_ Y).hom = (λ_ X).hom ≫ f :=
-  by simp
-
-@[reassoc]
-theorem rightUnitor_naturality' {X Y : C} (f : X ⟶ Y) :
-    (f ⊗ 𝟙 (𝟙_ C)) ≫ (ρ_ Y).hom = (ρ_ X).hom ≫ f := by
-  simp
-
 @[reassoc]
 theorem leftUnitor_inv_naturality {X X' : C} (f : X ⟶ X') :
     f ≫ (λ_ X').inv = (λ_ X).inv ≫ (𝟙 _ ⊗ f) := by
diff --git a/Mathlib/CategoryTheory/Monoidal/Center.lean b/Mathlib/CategoryTheory/Monoidal/Center.lean
index 19d7d10a0f7e6..e4d5f001d43b8 100644
--- a/Mathlib/CategoryTheory/Monoidal/Center.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Center.lean
@@ -17,18 +17,19 @@ We define `Center C` to be pairs `⟨X, b⟩`, where `X : C` and `b` is a half-b
 We show that `Center C` is braided monoidal,
 and provide the monoidal functor `Center.forget` from `Center C` back to `C`.
 
-## Future work
+## Implementation notes
 
-Verifying the various axioms here is done by tedious rewriting.
+Verifying the various axioms directly requires tedious rewriting.
 Using the `slice` tactic may make the proofs marginally more readable.
 
 More exciting, however, would be to make possible one of the following options:
 1. Integration with homotopy.io / globular to give "picture proofs".
 2. The monoidal coherence theorem, so we can ignore associators
-   (after which most of these proofs are trivial;
-   I'm unsure if the monoidal coherence theorem is even usable in dependent type theory).
+   (after which most of these proofs are trivial).
 3. Automating these proofs using `rewrite_search` or some relative.
 
+In this file, we take the second approach using the monoidal composition `⊗≫` and the
+`coherence` tactic.
 -/
 
 
@@ -56,9 +57,9 @@ structure HalfBraiding (X : C) where
   β : ∀ U, X ⊗ U ≅ U ⊗ X
   monoidal : ∀ U U', (β (U ⊗ U')).hom =
       (α_ _ _ _).inv ≫
-        ((β U).hom ⊗ 𝟙 U') ≫ (α_ _ _ _).hom ≫ (𝟙 U ⊗ (β U').hom) ≫ (α_ _ _ _).inv := by
+        ((β U).hom ▷ U') ≫ (α_ _ _ _).hom ≫ (U ◁ (β U').hom) ≫ (α_ _ _ _).inv := by
     aesop_cat
-  naturality : ∀ {U U'} (f : U ⟶ U'), (𝟙 X ⊗ f) ≫ (β U').hom = (β U).hom ≫ (f ⊗ 𝟙 X) := by
+  naturality : ∀ {U U'} (f : U ⟶ U'), (X ◁ f) ≫ (β U').hom = (β U).hom ≫ (f ▷ X) := by
     aesop_cat
 #align category_theory.half_braiding CategoryTheory.HalfBraiding
 
@@ -84,7 +85,7 @@ variable {C}
 @[ext] -- @[nolint has_nonempty_instance] -- Porting note: This linter does not exist yet.
 structure Hom (X Y : Center C) where
   f : X.1 ⟶ Y.1
-  comm : ∀ U, (f ⊗ 𝟙 U) ≫ (Y.2.β U).hom = (X.2.β U).hom ≫ (𝟙 U ⊗ f) := by aesop_cat
+  comm : ∀ U, (f ▷ U) ≫ (Y.2.β U).hom = (X.2.β U).hom ≫ (U ◁ f) := by aesop_cat
 #align category_theory.center.hom CategoryTheory.Center.Hom
 
 attribute [reassoc (attr := simp)] Hom.comm
@@ -118,7 +119,8 @@ a morphism whose underlying morphism is an isomorphism.
 def isoMk {X Y : Center C} (f : X ⟶ Y) [IsIso f.f] : X ≅ Y where
   hom := f
   inv := ⟨inv f.f,
-    fun U => by simp [← cancel_epi (f.f ⊗ 𝟙 U), ← comp_tensor_id_assoc, ← id_tensor_comp]⟩
+    fun U => by simp [← cancel_epi (f.f ▷ U), ← comp_whiskerRight_assoc,
+      ← MonoidalCategory.whiskerLeft_comp] ⟩
 #align category_theory.center.iso_mk CategoryTheory.Center.isoMk
 
 instance isIso_of_f_isIso {X Y : Center C} (f : X ⟶ Y) [IsIso f.f] : IsIso f := by
@@ -132,48 +134,86 @@ def tensorObj (X Y : Center C) : Center C :=
   ⟨X.1 ⊗ Y.1,
     { β := fun U =>
         α_ _ _ _ ≪≫
-          (Iso.refl X.1 ⊗ Y.2.β U) ≪≫ (α_ _ _ _).symm ≪≫ (X.2.β U ⊗ Iso.refl Y.1) ≪≫ α_ _ _ _
+          (whiskerLeftIso X.1 (Y.2.β U)) ≪≫ (α_ _ _ _).symm ≪≫
+            (whiskerRightIso (X.2.β U) Y.1) ≪≫ α_ _ _ _
       monoidal := fun U U' => by
-        dsimp
-        simp only [comp_tensor_id, id_tensor_comp, Category.assoc, HalfBraiding.monoidal]
-        -- On the RHS, we'd like to commute `((X.snd.β U).hom ⊗ 𝟙 Y.fst) ⊗ 𝟙 U'`
-        -- and `𝟙 U ⊗ 𝟙 X.fst ⊗ (Y.snd.β U').hom` past each other,
-        -- but there are some associators we need to get out of the way first.
-        slice_rhs 6 8 => rw [pentagon]
-        slice_rhs 5 6 => rw [associator_naturality]
-        slice_rhs 7 8 => rw [← associator_naturality]
-        slice_rhs 6 7 =>
-          rw [tensor_id, tensor_id, tensor_id_comp_id_tensor, ← id_tensor_comp_tensor_id,
-            ← tensor_id, ← tensor_id]
-        -- Now insert associators as needed to make the four half-braidings look identical
-        slice_rhs 10 10 => rw [associator_inv_conjugation]
-        slice_rhs 7 7 => rw [associator_inv_conjugation]
-        slice_rhs 6 6 => rw [associator_conjugation]
-        slice_rhs 3 3 => rw [associator_conjugation]
-        -- Finish with an application of the coherence theorem.
-        coherence
-      naturality := fun f => by
-        dsimp
-        rw [Category.assoc, Category.assoc, Category.assoc, Category.assoc,
-          id_tensor_associator_naturality_assoc, ← id_tensor_comp_assoc, HalfBraiding.naturality,
-          id_tensor_comp_assoc, associator_inv_naturality_assoc, ← comp_tensor_id_assoc,
-          HalfBraiding.naturality, comp_tensor_id_assoc, associator_naturality, ← tensor_id] }⟩
+        dsimp only [Iso.trans_hom, whiskerLeftIso_hom, Iso.symm_hom, whiskerRightIso_hom]
+        simp only [HalfBraiding.monoidal]
+        -- We'd like to commute `X.1 ◁ U ◁ (HalfBraiding.β Y.2 U').hom`
+        -- and `((HalfBraiding.β X.2 U).hom ▷ U' ▷ Y.1)` past each other.
+        -- We do this with the help of the monoidal composition `⊗≫` and the `coherence` tactic.
+        calc
+          _ = 𝟙 _ ⊗≫
+            X.1 ◁ (HalfBraiding.β Y.2 U).hom ▷ U' ⊗≫
+              (_ ◁ (HalfBraiding.β Y.2 U').hom ≫
+                (HalfBraiding.β X.2 U).hom ▷ _) ⊗≫
+                  U ◁ (HalfBraiding.β X.2 U').hom ▷ Y.1 ⊗≫ 𝟙 _ := by coherence
+          _ = _ := by rw [whisker_exchange]; coherence
+      naturality := fun {U U'} f => by
+        dsimp only [Iso.trans_hom, whiskerLeftIso_hom, Iso.symm_hom, whiskerRightIso_hom]
+        calc
+          _ = 𝟙 _ ⊗≫
+            (X.1 ◁ (Y.1 ◁ f ≫ (HalfBraiding.β Y.2 U').hom)) ⊗≫
+              (HalfBraiding.β X.2 U').hom ▷ Y.1 ⊗≫ 𝟙 _ := by coherence
+          _ = 𝟙 _ ⊗≫
+            X.1 ◁ (HalfBraiding.β Y.2 U).hom ⊗≫
+              (X.1 ◁ f ≫ (HalfBraiding.β X.2 U').hom) ▷ Y.1 ⊗≫ 𝟙 _ := by
+            rw [HalfBraiding.naturality]; coherence
+          _ = _ := by rw [HalfBraiding.naturality]; coherence }⟩
 #align category_theory.center.tensor_obj CategoryTheory.Center.tensorObj
 
+@[reassoc]
+theorem whiskerLeft_comm (X : Center C) {Y₁ Y₂ : Center C} (f : Y₁ ⟶ Y₂) (U : C) :
+    (X.1 ◁ f.f) ▷ U ≫ ((tensorObj X Y₂).2.β U).hom =
+      ((tensorObj X Y₁).2.β U).hom ≫ U ◁ X.1 ◁ f.f := by
+  dsimp only [tensorObj_fst, tensorObj_snd_β, Iso.trans_hom, whiskerLeftIso_hom,
+    Iso.symm_hom, whiskerRightIso_hom]
+  calc
+    _ = 𝟙 _ ⊗≫
+      X.fst ◁ (f.f ▷ U ≫ (HalfBraiding.β Y₂.snd U).hom) ⊗≫
+        (HalfBraiding.β X.snd U).hom ▷ Y₂.fst ⊗≫ 𝟙 _ := by coherence
+    _ = 𝟙 _ ⊗≫
+      X.fst ◁ (HalfBraiding.β Y₁.snd U).hom ⊗≫
+        ((X.fst ⊗ U) ◁ f.f ≫ (HalfBraiding.β X.snd U).hom ▷ Y₂.fst) ⊗≫ 𝟙 _ := by
+      rw [f.comm]; coherence
+    _ = _ := by rw [whisker_exchange]; coherence
+
+/-- Auxiliary definition for the `MonoidalCategory` instance on `Center C`. -/
+def whiskerLeft (X : Center C) {Y₁ Y₂ : Center C} (f : Y₁ ⟶ Y₂) :
+    tensorObj X Y₁ ⟶ tensorObj X Y₂ where
+  f := X.1 ◁ f.f
+  comm U := whiskerLeft_comm X f U
+
+@[reassoc]
+theorem whiskerRight_comm {X₁ X₂: Center C} (f : X₁ ⟶ X₂) (Y : Center C) (U : C) :
+    f.f ▷ Y.1 ▷ U ≫ ((tensorObj X₂ Y).2.β U).hom =
+      ((tensorObj X₁ Y).2.β U).hom ≫ U ◁ f.f ▷ Y.1 := by
+  dsimp only [tensorObj_fst, tensorObj_snd_β, Iso.trans_hom, whiskerLeftIso_hom,
+    Iso.symm_hom, whiskerRightIso_hom]
+  calc
+    _ = 𝟙 _ ⊗≫
+      (f.f ▷ (Y.fst ⊗ U) ≫ X₂.fst ◁ (HalfBraiding.β Y.snd U).hom) ⊗≫
+        (HalfBraiding.β X₂.snd U).hom ▷ Y.fst ⊗≫ 𝟙 _ := by coherence
+    _ = 𝟙 _ ⊗≫
+      X₁.fst ◁ (HalfBraiding.β Y.snd U).hom ⊗≫
+        (f.f ▷ U ≫ (HalfBraiding.β X₂.snd U).hom) ▷ Y.fst ⊗≫ 𝟙 _ := by
+      rw [← whisker_exchange]; coherence
+    _ = _ := by rw [f.comm]; coherence
+
+/-- Auxiliary definition for the `MonoidalCategory` instance on `Center C`. -/
+def whiskerRight {X₁ X₂ : Center C} (f : X₁ ⟶ X₂) (Y : Center C) :
+    tensorObj X₁ Y ⟶ tensorObj X₂ Y where
+  f := f.f ▷ Y.1
+  comm U := whiskerRight_comm f Y U
+
 /-- Auxiliary definition for the `MonoidalCategory` instance on `Center C`. -/
 @[simps]
 def tensorHom {X₁ Y₁ X₂ Y₂ : Center C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) :
     tensorObj X₁ X₂ ⟶ tensorObj Y₁ Y₂ where
   f := f.f ⊗ g.f
   comm U := by
-    dsimp
-    rw [Category.assoc, Category.assoc, Category.assoc, Category.assoc, associator_naturality_assoc,
-      ← tensor_id_comp_id_tensor, Category.assoc, ← id_tensor_comp_assoc, g.comm,
-      id_tensor_comp_assoc, tensor_id_comp_id_tensor_assoc, ← id_tensor_comp_tensor_id,
-      Category.assoc, associator_inv_naturality_assoc, id_tensor_associator_inv_naturality_assoc,
-      tensor_id, id_tensor_comp_tensor_id_assoc, ← tensor_id_comp_id_tensor g.f, Category.assoc,
-      ← comp_tensor_id_assoc, f.comm, comp_tensor_id_assoc, id_tensor_associator_naturality,
-      associator_naturality_assoc, ← id_tensor_comp, tensor_id_comp_id_tensor]
+    rw [tensorHom_def, comp_whiskerRight_assoc, whiskerLeft_comm, whiskerRight_comm_assoc,
+      MonoidalCategory.whiskerLeft_comp]
 #align category_theory.center.tensor_hom CategoryTheory.Center.tensorHom
 
 section
@@ -209,14 +249,14 @@ attribute [local simp] associator_naturality leftUnitor_naturality rightUnitor_n
 
 attribute [local simp] Center.associator Center.leftUnitor Center.rightUnitor
 
+attribute [local simp] Center.whiskerLeft Center.whiskerRight Center.tensorHom
+
 instance : MonoidalCategory (Center C) where
   tensorObj X Y := tensorObj X Y
   tensorHom f g := tensorHom f g
   tensorHom_def := by intros; ext; simp [tensorHom_def]
-  -- Todo: replace it by `X.1 ◁ f.f`
-  whiskerLeft X _ _ f := tensorHom (𝟙 X) f
-  -- Todo: replace it by `f.f ▷ Y.1`
-  whiskerRight f Y := tensorHom f (𝟙 Y)
+  whiskerLeft X _ _ f := whiskerLeft X f
+  whiskerRight f Y := whiskerRight f Y
   tensorUnit := tensorUnit
   associator := associator
   leftUnitor := leftUnitor
@@ -231,17 +271,18 @@ theorem tensor_fst (X Y : Center C) : (X ⊗ Y).1 = X.1 ⊗ Y.1 :=
 theorem tensor_β (X Y : Center C) (U : C) :
     (X ⊗ Y).2.β U =
       α_ _ _ _ ≪≫
-        (Iso.refl X.1 ⊗ Y.2.β U) ≪≫ (α_ _ _ _).symm ≪≫ (X.2.β U ⊗ Iso.refl Y.1) ≪≫ α_ _ _ _ :=
+        (whiskerLeftIso X.1 (Y.2.β U)) ≪≫ (α_ _ _ _).symm ≪≫
+          (whiskerRightIso (X.2.β U) Y.1) ≪≫ α_ _ _ _ :=
   rfl
 #align category_theory.center.tensor_β CategoryTheory.Center.tensor_β
 
 @[simp]
 theorem whiskerLeft_f (X : Center C) {Y₁ Y₂ : Center C} (f : Y₁ ⟶ Y₂) : (X ◁ f).f = X.1 ◁ f.f :=
-  id_tensorHom X.1 f.f
+  rfl
 
 @[simp]
 theorem whiskerRight_f {X₁ X₂ : Center C} (f : X₁ ⟶ X₂) (Y : Center C) : (f ▷ Y).f = f.f ▷ Y.1 :=
-  tensorHom_id f.f Y.1
+  rfl
 
 @[simp]
 theorem tensor_f {X₁ Y₁ X₂ Y₂ : Center C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : (f ⊗ g).f = f.f ⊗ g.f :=
@@ -344,20 +385,9 @@ def ofBraided : MonoidalFunctor C (Center C) where
   obj := ofBraidedObj
   map f :=
     { f
-      comm := fun U => braiding_naturality _ _ }
-  ε :=
-    { f := 𝟙 _
-      comm := fun U => by
-        dsimp
-        rw [tensor_id, Category.id_comp, tensor_id, Category.comp_id, ← braiding_rightUnitor,
-          Category.assoc, Iso.hom_inv_id, Category.comp_id] }
-  μ X Y :=
-    { f := 𝟙 _
-      comm := fun U => by
-        dsimp
-        rw [tensor_id, tensor_id, Category.id_comp, Category.comp_id, ← Iso.inv_comp_eq,
-          ← Category.assoc, ← Category.assoc, ← Iso.comp_inv_eq, Category.assoc, hexagon_reverse,
-          Category.assoc] }
+      comm := fun U => braiding_naturality_left f U }
+  ε := { f := 𝟙 _ }
+  μ X Y := { f := 𝟙 _ }
 #align category_theory.center.of_braided CategoryTheory.Center.ofBraided
 
 end
diff --git a/Mathlib/CategoryTheory/Monoidal/CommMon_.lean b/Mathlib/CategoryTheory/Monoidal/CommMon_.lean
index e4a0f20b6a6f4..4abc94fdb8686 100644
--- a/Mathlib/CategoryTheory/Monoidal/CommMon_.lean
+++ b/Mathlib/CategoryTheory/Monoidal/CommMon_.lean
@@ -171,7 +171,9 @@ 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
 
-/-- Implementation of `CommMon_.equivLaxBraidedFunctorPUnit`. -/
+attribute [local simp] id_tensorHom tensorHom_id
+
+/-- Implementation of `CommMon_.equivLaxBraidedFunctorPunit`. -/
 @[simps]
 def commMonToLaxBraided : CommMon_ C ⥤ LaxBraidedFunctor (Discrete PUnit.{u + 1}) C where
   obj A :=
diff --git a/Mathlib/CategoryTheory/Monoidal/Functor.lean b/Mathlib/CategoryTheory/Monoidal/Functor.lean
index e899d4b4ece1e..7a875c0cebc08 100644
--- a/Mathlib/CategoryTheory/Monoidal/Functor.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Functor.lean
@@ -122,6 +122,34 @@ theorem LaxMonoidalFunctor.μ_natural (F : LaxMonoidalFunctor C D) {X Y X' Y' :
   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]
+
 /--
 A constructor for lax monoidal functors whose axioms are described by `tensorHom` instead of
 `whiskerLeft` and `whiskerRight`.
@@ -192,6 +220,22 @@ theorem LaxMonoidalFunctor.associativity_inv (F : LaxMonoidalFunctor C D) (X Y Z
     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
 
 /--
diff --git a/Mathlib/CategoryTheory/Monoidal/Internal/Module.lean b/Mathlib/CategoryTheory/Monoidal/Internal/Module.lean
index ea7536e625e26..e66bd2c9ec1e3 100644
--- a/Mathlib/CategoryTheory/Monoidal/Internal/Module.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Internal/Module.lean
@@ -124,7 +124,7 @@ def inverseObj (A : AlgebraCat.{u} R) : Mon_ (ModuleCat.{u} R) where
     --   ModuleCat.MonoidalCategory.leftUnitor_hom_apply]
     -- Porting note : because `dsimp` is not effective, `rw` needs to be changed to `erw`
     erw [LinearMap.mul'_apply, MonoidalCategory.leftUnitor_hom_apply, ← Algebra.smul_def]
-    rw [id_apply]
+    erw [id_apply]
   mul_one := by
     -- Porting note : `ext` did not pick up `TensorProduct.ext`
     refine TensorProduct.ext <| LinearMap.ext fun x => LinearMap.ext_ring ?_
@@ -138,7 +138,7 @@ def inverseObj (A : AlgebraCat.{u} R) : Mon_ (ModuleCat.{u} R) where
     erw [CategoryTheory.comp_apply]
     erw [LinearMap.mul'_apply, ModuleCat.MonoidalCategory.rightUnitor_hom_apply, ← Algebra.commutes,
       ← Algebra.smul_def]
-    rw [id_apply]
+    erw [id_apply]
   mul_assoc := by
     -- Porting note : `ext` did not pick up `TensorProduct.ext`
     refine TensorProduct.ext <| TensorProduct.ext <| LinearMap.ext fun x => LinearMap.ext fun y =>
@@ -151,7 +151,7 @@ def inverseObj (A : AlgebraCat.{u} R) : Mon_ (ModuleCat.{u} R) where
     erw [CategoryTheory.comp_apply,
       CategoryTheory.comp_apply, CategoryTheory.comp_apply]
     erw [LinearMap.mul'_apply, LinearMap.mul'_apply]
-    rw [id_apply]
+    erw [id_apply]
     erw [TensorProduct.mk_apply, TensorProduct.mk_apply, id_apply, LinearMap.mul'_apply,
       LinearMap.mul'_apply]
     simp only [LinearMap.mul'_apply, mul_assoc]
diff --git a/Mathlib/CategoryTheory/Monoidal/Mod_.lean b/Mathlib/CategoryTheory/Monoidal/Mod_.lean
index 1e23e1bccecdb..676dac683e395 100644
--- a/Mathlib/CategoryTheory/Monoidal/Mod_.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Mod_.lean
@@ -24,8 +24,8 @@ variable {C}
 structure Mod_ (A : Mon_ C) where
   X : C
   act : A.X ⊗ X ⟶ X
-  one_act : (A.one ⊗ 𝟙 X) ≫ act = (λ_ X).hom := by aesop_cat
-  assoc : (A.mul ⊗ 𝟙 X) ≫ act = (α_ A.X A.X X).hom ≫ (𝟙 A.X ⊗ act) ≫ act := by aesop_cat
+  one_act : (A.one ▷ X) ≫ act = (λ_ X).hom := by aesop_cat
+  assoc : (A.mul ▷ X) ≫ act = (α_ A.X A.X X).hom ≫ (A.X ◁ act) ≫ act := by aesop_cat
 set_option linter.uppercaseLean3 false in
 #align Mod_ Mod_
 
@@ -36,7 +36,7 @@ namespace Mod_
 variable {A : Mon_ C} (M : Mod_ A)
 
 theorem assoc_flip :
-    (𝟙 A.X ⊗ M.act) ≫ M.act = (α_ A.X A.X M.X).inv ≫ (A.mul ⊗ 𝟙 M.X) ≫ M.act := by simp
+    (A.X ◁ M.act) ≫ M.act = (α_ A.X A.X M.X).inv ≫ (A.mul ▷ M.X) ≫ M.act := by simp
 set_option linter.uppercaseLean3 false in
 #align Mod_.assoc_flip Mod_.assoc_flip
 
@@ -45,7 +45,7 @@ set_option linter.uppercaseLean3 false in
 @[ext]
 structure Hom (M N : Mod_ A) where
   hom : M.X ⟶ N.X
-  act_hom : M.act ≫ hom = (𝟙 A.X ⊗ hom) ≫ N.act := by aesop_cat
+  act_hom : M.act ≫ hom = (A.X ◁ hom) ≫ N.act := by aesop_cat
 set_option linter.uppercaseLean3 false in
 #align Mod_.hom Mod_.Hom
 
@@ -121,26 +121,26 @@ between the categories of module objects.
 def comap {A B : Mon_ C} (f : A ⟶ B) : Mod_ B ⥤ Mod_ A where
   obj M :=
     { X := M.X
-      act := (f.hom ⊗ 𝟙 M.X) ≫ M.act
+      act := (f.hom ▷ M.X) ≫ M.act
       one_act := by
-        slice_lhs 1 2 => rw [← comp_tensor_id]
+        slice_lhs 1 2 => rw [← comp_whiskerRight]
         rw [f.one_hom, one_act]
       assoc := by
         -- oh, for homotopy.io in a widget!
-        slice_rhs 2 3 => rw [id_tensor_comp_tensor_id, ← tensor_id_comp_id_tensor]
-        rw [id_tensor_comp]
+        slice_rhs 2 3 => rw [whisker_exchange]
+        simp only [whiskerRight_tensor, MonoidalCategory.whiskerLeft_comp, Category.assoc,
+          Iso.hom_inv_id_assoc]
         slice_rhs 4 5 => rw [Mod_.assoc_flip]
-        slice_rhs 3 4 => rw [associator_inv_naturality]
-        slice_rhs 2 3 => rw [← tensor_id, associator_inv_naturality]
-        slice_rhs 1 3 => rw [Iso.hom_inv_id_assoc]
-        slice_rhs 1 2 => rw [← comp_tensor_id, tensor_id_comp_id_tensor]
-        slice_rhs 1 2 => rw [← comp_tensor_id, ← f.mul_hom]
-        rw [comp_tensor_id, Category.assoc] }
+        slice_rhs 3 4 => rw [associator_inv_naturality_middle]
+        slice_rhs 2 4 => rw [Iso.hom_inv_id_assoc]
+        slice_rhs 1 2 => rw [← MonoidalCategory.comp_whiskerRight, ← whisker_exchange]
+        slice_rhs 1 2 => rw [← MonoidalCategory.comp_whiskerRight, ← tensorHom_def', ← f.mul_hom]
+        rw [comp_whiskerRight, Category.assoc] }
   map g :=
     { hom := g.hom
       act_hom := by
         dsimp
-        slice_rhs 1 2 => rw [id_tensor_comp_tensor_id, ← tensor_id_comp_id_tensor]
+        slice_rhs 1 2 => rw [whisker_exchange]
         slice_rhs 2 3 => rw [← g.act_hom]
         rw [Category.assoc] }
 set_option linter.uppercaseLean3 false in
diff --git a/Mathlib/CategoryTheory/Monoidal/Mon_.lean b/Mathlib/CategoryTheory/Monoidal/Mon_.lean
index 222916e3e2602..66f3cd8f2aed6 100644
--- a/Mathlib/CategoryTheory/Monoidal/Mon_.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Mon_.lean
@@ -36,17 +36,19 @@ structure Mon_ where
   X : C
   one : 𝟙_ C ⟶ X
   mul : X ⊗ X ⟶ X
-  one_mul : (one ⊗ 𝟙 X) ≫ mul = (λ_ X).hom := by aesop_cat
-  mul_one : (𝟙 X ⊗ one) ≫ mul = (ρ_ X).hom := by aesop_cat
+  one_mul : (one ▷ X) ≫ mul = (λ_ X).hom := by aesop_cat
+  mul_one : (X ◁ one) ≫ mul = (ρ_ X).hom := by aesop_cat
   -- Obviously there is some flexibility stating this axiom.
   -- This one has left- and right-hand sides matching the statement of `Monoid.mul_assoc`,
   -- and chooses to place the associator on the right-hand side.
   -- The heuristic is that unitors and associators "don't have much weight".
-  mul_assoc : (mul ⊗ 𝟙 X) ≫ mul = (α_ X X X).hom ≫ (𝟙 X ⊗ mul) ≫ mul := by aesop_cat
+  mul_assoc : (mul ▷ X) ≫ mul = (α_ X X X).hom ≫ (X ◁ mul) ≫ mul := by aesop_cat
 #align Mon_ Mon_
 
 attribute [reassoc] Mon_.one_mul Mon_.mul_one
 
+attribute [simp] Mon_.one_mul Mon_.mul_one
+
 -- We prove a more general `@[simp]` lemma below.
 attribute [reassoc (attr := simp)] Mon_.mul_assoc
 
@@ -71,16 +73,16 @@ 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 [← id_tensor_comp_tensor_id, Category.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 [← tensor_id_comp_id_tensor, Category.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 :
-    (𝟙 M.X ⊗ M.mul) ≫ M.mul = (α_ M.X M.X M.X).inv ≫ (M.mul ⊗ 𝟙 M.X) ≫ M.mul := by simp
+    (M.X ◁ M.mul) ≫ M.mul = (α_ M.X M.X M.X).inv ≫ (M.mul ▷ M.X) ≫ M.mul := by simp
 #align Mon_.assoc_flip Mon_.assoc_flip
 
 /-- A morphism of monoid objects. -/
@@ -210,28 +212,17 @@ 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
-        conv_lhs => rw [comp_tensor_id, ← F.toFunctor.map_id]
-        slice_lhs 2 3 => rw [F.μ_natural]
+        simp only [comp_whiskerRight, Category.assoc, μ_natural_left'_assoc, left_unitality']
         slice_lhs 3 4 => rw [← F.toFunctor.map_comp, A.one_mul]
-        rw [F.toFunctor.map_id]
-        rw [F.left_unitality]
       mul_one := by
-        conv_lhs => rw [id_tensor_comp, ← F.toFunctor.map_id]
-        slice_lhs 2 3 => rw [F.μ_natural]
+        simp only [MonoidalCategory.whiskerLeft_comp, Category.assoc, μ_natural_right'_assoc,
+          right_unitality']
         slice_lhs 3 4 => rw [← F.toFunctor.map_comp, A.mul_one]
-        rw [F.toFunctor.map_id]
-        rw [F.right_unitality]
       mul_assoc := by
-        conv_lhs => rw [comp_tensor_id, ← F.toFunctor.map_id]
-        slice_lhs 2 3 => rw [F.μ_natural]
+        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]
-        conv_lhs => rw [F.toFunctor.map_id]
-        conv_lhs => rw [F.toFunctor.map_comp, F.toFunctor.map_comp]
-        conv_rhs => rw [id_tensor_comp, ← F.toFunctor.map_id]
-        slice_rhs 3 4 => rw [F.μ_natural]
-        conv_rhs => rw [F.toFunctor.map_id]
-        slice_rhs 1 3 => rw [← F.associativity]
-        simp only [Category.assoc] }
+        simp }
   map f :=
     { hom := F.map f.hom
       one_hom := by dsimp; rw [Category.assoc, ← F.toFunctor.map_comp, f.one_hom]
@@ -267,6 +258,8 @@ 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
@@ -387,59 +380,57 @@ theorem one_associator {M N P : Mon_ C} :
   slice_lhs 1 2 => rw [← leftUnitor_tensor_inv]
   rw [← cancel_epi (λ_ (𝟙_ C)).inv]
   slice_lhs 1 2 => rw [leftUnitor_inv_naturality]
-  simp only [Category.assoc]
+  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
-  slice_lhs 2 3 => rw [leftUnitor_naturality]
   simp
 #align Mon_.one_left_unitor Mon_.one_leftUnitor
 
 theorem one_rightUnitor {M : Mon_ C} :
     ((λ_ (𝟙_ C)).inv ≫ (M.one ⊗ 𝟙 (𝟙_ C))) ≫ (ρ_ M.X).hom = M.one := by
-  slice_lhs 2 3 => rw [rightUnitor_naturality, ← unitors_equal]
-  simp
+  simp [← unitors_equal]
 #align Mon_.one_right_unitor Mon_.one_rightUnitor
 
 variable [BraidedCategory C]
 
 theorem Mon_tensor_one_mul (M N : Mon_ C) :
-    ((λ_ (𝟙_ C)).inv ≫ (M.one ⊗ N.one) ⊗ 𝟙 (M.X ⊗ N.X)) ≫
+    (((λ_ (𝟙_ C)).inv ≫ (M.one ⊗ N.one)) ▷ (M.X ⊗ N.X)) ≫
         tensor_μ C (M.X, N.X) (M.X, N.X) ≫ (M.mul ⊗ N.mul) =
       (λ_ (M.X ⊗ N.X)).hom := by
-  rw [← Category.id_comp (𝟙 (M.X ⊗ N.X)), tensor_comp]
-  slice_lhs 2 3 => rw [← tensor_id, tensor_μ_natural]
+  simp only [comp_whiskerRight_assoc]
+  slice_lhs 2 3 => rw [tensor_μ_natural_left]
   slice_lhs 3 4 => rw [← tensor_comp, one_mul M, one_mul N]
   symm
   exact tensor_left_unitality C M.X N.X
 #align Mon_.Mon_tensor_one_mul Mon_.Mon_tensor_one_mul
 
 theorem Mon_tensor_mul_one (M N : Mon_ C) :
-    (𝟙 (M.X ⊗ N.X) ⊗ (λ_ (𝟙_ C)).inv ≫ (M.one ⊗ N.one)) ≫
+    (M.X ⊗ N.X) ◁ ((λ_ (𝟙_ C)).inv ≫ (M.one ⊗ N.one)) ≫
         tensor_μ C (M.X, N.X) (M.X, N.X) ≫ (M.mul ⊗ N.mul) =
       (ρ_ (M.X ⊗ N.X)).hom := by
-  rw [← Category.id_comp (𝟙 (M.X ⊗ N.X)), tensor_comp]
-  slice_lhs 2 3 => rw [← tensor_id, tensor_μ_natural]
+  simp only [whiskerLeft_comp_assoc]
+  slice_lhs 2 3 => rw [tensor_μ_natural_right]
   slice_lhs 3 4 => rw [← tensor_comp, mul_one M, mul_one N]
   symm
   exact tensor_right_unitality C M.X N.X
 #align Mon_.Mon_tensor_mul_one Mon_.Mon_tensor_mul_one
 
 theorem Mon_tensor_mul_assoc (M N : Mon_ C) :
-    (tensor_μ C (M.X, N.X) (M.X, N.X) ≫ (M.mul ⊗ N.mul) ⊗ 𝟙 (M.X ⊗ N.X)) ≫
+    ((tensor_μ C (M.X, N.X) (M.X, N.X) ≫ (M.mul ⊗ N.mul)) ▷ (M.X ⊗ N.X)) ≫
         tensor_μ C (M.X, N.X) (M.X, N.X) ≫ (M.mul ⊗ N.mul) =
       (α_ (M.X ⊗ N.X) (M.X ⊗ N.X) (M.X ⊗ N.X)).hom ≫
-        (𝟙 (M.X ⊗ N.X) ⊗ tensor_μ C (M.X, N.X) (M.X, N.X) ≫ (M.mul ⊗ N.mul)) ≫
+        ((M.X ⊗ N.X) ◁ (tensor_μ C (M.X, N.X) (M.X, N.X) ≫ (M.mul ⊗ N.mul))) ≫
           tensor_μ C (M.X, N.X) (M.X, N.X) ≫ (M.mul ⊗ N.mul) := by
-  rw [← Category.id_comp (𝟙 (M.X ⊗ N.X)), tensor_comp]
-  slice_lhs 2 3 => rw [← tensor_id, tensor_μ_natural]
+  simp only [comp_whiskerRight_assoc, whiskerLeft_comp_assoc]
+  slice_lhs 2 3 => rw [tensor_μ_natural_left]
   slice_lhs 3 4 => rw [← tensor_comp, mul_assoc M, mul_assoc N, tensor_comp, tensor_comp]
-  -- Porting note: needed to add `dsimp` here.
-  slice_lhs 1 3 => dsimp; rw [tensor_associativity]
-  slice_lhs 3 4 => rw [← tensor_μ_natural]
-  slice_lhs 2 3 => rw [← tensor_comp, tensor_id]
-  simp only [Category.assoc]
+  slice_lhs 1 3 => rw [tensor_associativity]
+  slice_lhs 3 4 => rw [← tensor_μ_natural_right]
+  simp
 #align Mon_.Mon_tensor_mul_assoc Mon_.Mon_tensor_mul_assoc
 
 theorem mul_associator {M N P : Mon_ C} :
@@ -453,6 +444,7 @@ theorem mul_associator {M N P : Mon_ C} :
   slice_lhs 2 3 => rw [← Category.id_comp P.mul, tensor_comp]
   slice_lhs 3 4 => rw [associator_naturality]
   slice_rhs 3 4 => rw [← Category.id_comp M.mul, tensor_comp]
+  simp only [tensorHom_id, id_tensorHom]
   slice_lhs 1 3 => rw [associator_monoidal]
   simp only [Category.assoc]
 #align Mon_.mul_associator Mon_.mul_associator
@@ -461,7 +453,8 @@ theorem mul_leftUnitor {M : Mon_ C} :
     (tensor_μ C (𝟙_ C, M.X) (𝟙_ C, M.X) ≫ ((λ_ (𝟙_ C)).hom ⊗ M.mul)) ≫ (λ_ M.X).hom =
       ((λ_ M.X).hom ⊗ (λ_ M.X).hom) ≫ M.mul := by
   rw [← Category.comp_id (λ_ (𝟙_ C)).hom, ← Category.id_comp M.mul, tensor_comp]
-  slice_lhs 3 4 => rw [leftUnitor_naturality]
+  simp only [tensorHom_id, id_tensorHom]
+  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
@@ -470,7 +463,8 @@ theorem mul_rightUnitor {M : Mon_ C} :
     (tensor_μ C (M.X, 𝟙_ C) (M.X, 𝟙_ C) ≫ (M.mul ⊗ (λ_ (𝟙_ C)).hom)) ≫ (ρ_ M.X).hom =
       ((ρ_ M.X).hom ⊗ (ρ_ M.X).hom) ≫ M.mul := by
   rw [← Category.id_comp M.mul, ← Category.comp_id (λ_ (𝟙_ C)).hom, tensor_comp]
-  slice_lhs 3 4 => rw [rightUnitor_naturality]
+  simp only [tensorHom_id, id_tensorHom]
+  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/Tactic/CategoryTheory/Coherence.lean b/Mathlib/Tactic/CategoryTheory/Coherence.lean
index 09bf3590c5f9a..f912e50c1cb10 100644
--- a/Mathlib/Tactic/CategoryTheory/Coherence.lean
+++ b/Mathlib/Tactic/CategoryTheory/Coherence.lean
@@ -90,11 +90,11 @@ instance LiftHom_comp {X Y Z : C} [LiftObj X] [LiftObj Y] [LiftObj Z] (f : X ⟶
 
 instance liftHom_WhiskerLeft (X : C) [LiftObj X] {Y Z : C} [LiftObj Y] [LiftObj Z]
     (f : Y ⟶ Z) [LiftHom f] : LiftHom (X ◁ f) where
-  lift := LiftObj.lift X ◁ LiftHom.lift f
+  lift := 𝟙 (LiftObj.lift X) ⊗ LiftHom.lift f
 
 instance liftHom_WhiskerRight {X Y : C} (f : X ⟶ Y) [LiftObj X] [LiftObj Y] [LiftHom f]
     {Z : C} [LiftObj Z] : LiftHom (f ▷ Z) where
-  lift := LiftHom.lift f ▷ LiftObj.lift Z
+  lift := LiftHom.lift f ⊗ 𝟙 (LiftObj.lift Z)
 
 instance LiftHom_tensor {W X Y Z : C} [LiftObj W] [LiftObj X] [LiftObj Y] [LiftObj Z]
     (f : W ⟶ X) (g : Y ⟶ Z) [LiftHom f] [LiftHom g] : LiftHom (f ⊗ g) where
@@ -129,12 +129,12 @@ instance whiskerRight (X Y Z : C) [LiftObj X] [LiftObj Y] [LiftObj Z] [MonoidalC
 @[simps]
 instance tensor_right (X Y : C) [LiftObj X] [LiftObj Y] [MonoidalCoherence (𝟙_ C) Y] :
     MonoidalCoherence X (X ⊗ Y) :=
-  ⟨(ρ_ X).inv ≫ (X ◁  MonoidalCoherence.hom)⟩
+  ⟨(ρ_ X).inv ≫ (𝟙 X ⊗  MonoidalCoherence.hom)⟩
 
 @[simps]
 instance tensor_right' (X Y : C) [LiftObj X] [LiftObj Y] [MonoidalCoherence Y (𝟙_ C)] :
     MonoidalCoherence (X ⊗ Y) X :=
-  ⟨(X ◁ MonoidalCoherence.hom) ≫ (ρ_ X).hom⟩
+  ⟨(𝟙 X ⊗ MonoidalCoherence.hom) ≫ (ρ_ X).hom⟩
 
 @[simps]
 instance left (X Y : C) [LiftObj X] [LiftObj Y] [MonoidalCoherence X Y] :
@@ -362,6 +362,27 @@ def coherence_loop (maxSteps := 37) : TacticM Unit :=
       -- and whose second terms can be identified by recursively called `coherence`.
       coherence_loop maxSteps'
 
+open Lean.Parser.Tactic
+
+/--
+Simp lemmas for rewriting a hom in monoical categories into a normal form.
+-/
+syntax (name := monoidal_simps) "monoidal_simps" (config)? : tactic
+
+@[inherit_doc monoidal_simps]
+elab_rules : tactic
+| `(tactic| monoidal_simps $[$cfg]?) => do
+  evalTactic (← `(tactic|
+    simp $[$cfg]? only [
+      Category.assoc, MonoidalCategory.tensor_whiskerLeft, MonoidalCategory.id_whiskerLeft,
+      MonoidalCategory.whiskerRight_tensor, MonoidalCategory.whiskerRight_id,
+      MonoidalCategory.whiskerLeft_comp, MonoidalCategory.whiskerLeft_id,
+      MonoidalCategory.comp_whiskerRight, MonoidalCategory.id_whiskerRight,
+      MonoidalCategory.whisker_assoc];
+    -- I'm not sure if `tensorHom` should be expanded.
+    try simp only [MonoidalCategory.tensorHom_def]
+    ))
+
 /--
 Use the coherence theorem for monoidal categories to solve equations in a monoidal equation,
 where the two sides only differ by replacing strings of monoidal structural morphisms
@@ -386,6 +407,10 @@ elab_rules : tactic
       Mathlib.Tactic.BicategoryCoherence.BicategoricalCoherence.hom,
       Mathlib.Tactic.BicategoryCoherence.BicategoricalCoherence.hom',
       monoidalComp]);
-    whisker_simps (config := {failIfUnchanged := false})
+    whisker_simps (config := {failIfUnchanged := false});
+    monoidal_simps (config := {failIfUnchanged := false});
+    -- Workaround until we define the whiskerings as the primitives in free monoidal categories.
+    simp (config := {failIfUnchanged := false}) only
+      [← MonoidalCategory.id_tensorHom, ← MonoidalCategory.tensorHom_id]
     ))
   coherence_loop