From df404a8d882fd32412a3e2d5ee38b98e43296dda Mon Sep 17 00:00:00 2001
From: Yuma Mizuno <mizuno.y.aj@gmail.com>
Date: Sun, 28 Jan 2024 13:43:15 +0900
Subject: [PATCH 1/4] update

---
 .../Algebra/Category/AlgebraCat/Monoidal.lean |   5 +
 .../CategoryTheory/Bicategory/SingleObj.lean  |  23 +-
 .../Closed/FunctorCategory.lean               |   2 +-
 Mathlib/CategoryTheory/Monoidal/Braided.lean  |   4 +-
 Mathlib/CategoryTheory/Monoidal/Category.lean | 486 ++++++++++++++----
 Mathlib/CategoryTheory/Monoidal/Center.lean   |  35 +-
 .../Monoidal/CoherenceLemmas.lean             |   6 +-
 Mathlib/CategoryTheory/Monoidal/End.lean      |  26 +-
 .../Monoidal/Free/Coherence.lean              |   7 +-
 Mathlib/CategoryTheory/Monoidal/Functor.lean  |  28 +-
 .../Monoidal/FunctorCategory.lean             |   4 +
 Mathlib/CategoryTheory/Monoidal/Limits.lean   |   2 +-
 Mathlib/CategoryTheory/Monoidal/Opposite.lean |   2 +
 .../CategoryTheory/Monoidal/Preadditive.lean  |   4 +-
 .../CategoryTheory/Monoidal/Rigid/Basic.lean  |   8 +-
 .../CategoryTheory/Monoidal/Transport.lean    |  44 +-
 .../Monoidal/Types/Coyoneda.lean              |   2 +
 .../QuadraticModuleCat/Monoidal.lean          |  10 +
 18 files changed, 462 insertions(+), 236 deletions(-)

diff --git a/Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean b/Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean
index 0e7f3bd65ed71..326c4ee237078 100644
--- a/Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean
+++ b/Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean
@@ -82,6 +82,11 @@ noncomputable instance instMonoidalCategory : MonoidalCategory (AlgebraCat.{u} R
         simp only [eqToIso_refl, Iso.refl_trans, Iso.refl_symm, Iso.trans_hom, tensorIso_hom,
           Iso.refl_hom, MonoidalCategory.tensor_id]
         erw [Category.id_comp, Category.comp_id, MonoidalCategory.tensor_id, Category.id_comp]
+      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]
+        rfl
       rightUnitor_eq := fun X => by
         dsimp
         erw [Category.id_comp, MonoidalCategory.tensor_id, Category.id_comp]
diff --git a/Mathlib/CategoryTheory/Bicategory/SingleObj.lean b/Mathlib/CategoryTheory/Bicategory/SingleObj.lean
index 931fb282c6e6f..d19bfd4843cb4 100644
--- a/Mathlib/CategoryTheory/Bicategory/SingleObj.lean
+++ b/Mathlib/CategoryTheory/Bicategory/SingleObj.lean
@@ -53,18 +53,12 @@ instance : Bicategory (MonoidalSingleObj C) where
   Hom _ _ := C
   id _ := 𝟙_ C
   comp X Y := tensorObj X Y
-  whiskerLeft X Y Z f := tensorHom (𝟙 X) f
-  whiskerRight f Z := tensorHom f (𝟙 Z)
+  whiskerLeft X Y Z f := X ◁ f
+  whiskerRight f Z := f ▷ Z
   associator X Y Z := α_ X Y Z
   leftUnitor X := λ_ X
   rightUnitor X := ρ_ X
-  comp_whiskerLeft _ _ _ _ _ := by
-    simp_rw [associator_inv_naturality, Iso.hom_inv_id_assoc, tensor_id]
-  whisker_assoc _ _ _ _ _ := by simp_rw [associator_inv_naturality, Iso.hom_inv_id_assoc]
-  whiskerRight_comp _ _ _ := by simp_rw [← tensor_id, associator_naturality, Iso.inv_hom_id_assoc]
-  id_whiskerLeft _ := by simp_rw [leftUnitor_inv_naturality, Iso.hom_inv_id_assoc]
-  whiskerRight_id _ := by simp_rw [rightUnitor_inv_naturality, Iso.hom_inv_id_assoc]
-  pentagon _ _ _ _ := by simp_rw [pentagon]
+  whisker_exchange := whisker_exchange
 
 namespace MonoidalSingleObj
 
@@ -74,6 +68,8 @@ 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.
@@ -86,15 +82,6 @@ def endMonoidalStarFunctor : MonoidalFunctor (EndMonoidal (MonoidalSingleObj.sta
   map f := f
   ε := 𝟙 _
   μ X Y := 𝟙 _
-  -- The proof will be automated after merging #6307.
-  μ_natural_left f g := by
-    simp_rw [Category.id_comp, Category.comp_id]
-    -- Should we provide further simp lemmas so this goal becomes visible?
-    exact (tensor_id_comp_id_tensor _ _).symm
-  μ_natural_right f g := by
-    simp_rw [Category.id_comp, Category.comp_id]
-    -- Should we provide further simp lemmas so this goal becomes visible?
-    exact (tensor_id_comp_id_tensor _ _).symm
 #align category_theory.monoidal_single_obj.End_monoidal_star_functor CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctor
 
 /-- The equivalence between the endomorphisms of the single object
diff --git a/Mathlib/CategoryTheory/Closed/FunctorCategory.lean b/Mathlib/CategoryTheory/Closed/FunctorCategory.lean
index 11c268d6f8716..42364eefa1e07 100644
--- a/Mathlib/CategoryTheory/Closed/FunctorCategory.lean
+++ b/Mathlib/CategoryTheory/Closed/FunctorCategory.lean
@@ -56,7 +56,7 @@ def closedCounit (F : D ⥤ C) : closedIhom F ⋙ tensorLeft F ⟶ 𝟭 (D ⥤ C
       dsimp
       simp only [closedIhom_obj_map, pre_comm_ihom_map]
       rw [← tensor_id_comp_id_tensor, id_tensor_comp]
-      simp }
+      simp [tensor_id_comp_id_tensor_assoc] }
 #align category_theory.functor.closed_counit CategoryTheory.Functor.closedCounit
 
 /-- If `C` is a monoidal closed category and `D` is a groupoid, then every functor `F : D ⥤ C` is
diff --git a/Mathlib/CategoryTheory/Monoidal/Braided.lean b/Mathlib/CategoryTheory/Monoidal/Braided.lean
index fc15f000f6acf..01523f81a7e39 100644
--- a/Mathlib/CategoryTheory/Monoidal/Braided.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Braided.lean
@@ -200,7 +200,7 @@ 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
+  by rw [← leftUnitor_tensor, leftUnitor_naturality]; simp [id_tensorHom, tensorHom_id]
 #align category_theory.braiding_left_unitor_aux₁ CategoryTheory.braiding_leftUnitor_aux₁
 
 theorem braiding_leftUnitor_aux₂ (X : C) :
@@ -233,7 +233,7 @@ 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
+  by rw [← rightUnitor_tensor, rightUnitor_naturality]; simp [id_tensorHom, tensorHom_id]
 #align category_theory.braiding_right_unitor_aux₁ CategoryTheory.braiding_rightUnitor_aux₁
 
 theorem braiding_rightUnitor_aux₂ (X : C) :
diff --git a/Mathlib/CategoryTheory/Monoidal/Category.lean b/Mathlib/CategoryTheory/Monoidal/Category.lean
index 893f1489a2b69..f7fc5b296aff1 100644
--- a/Mathlib/CategoryTheory/Monoidal/Category.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Category.lean
@@ -41,6 +41,27 @@ you can use the alternative constructor `CategoryTheory.MonoidalCategory.ofTenso
 
 The whiskerings are useful when considering simp-normal forms of morphisms in monoidal categories.
 
+### Simp-normal form for morphisms
+
+Rewriting involving associators and unitors could be very complicated. We try to ease this
+complexity by putting carefully chosen simp lemmas that rewrite any morphisms into the simp-normal
+form defined below. Rewriting into simp-normal form is especially useful in preprocessing
+performed by the `coherence` tactic.
+
+The simp-normal form of morphisms is defined to be an expression that has the minimal number of
+parentheses. More precisely,
+1. it is a composition of morphisms like `f₁ ≫ f₂ ≫ f₃ ≫ f₄ ≫ f₅` such that each `fᵢ` is
+  either a structural morphisms (morphisms made up only of identities, associators, unitors)
+  or non-structural morphisms, and
+2. each non-structural morphism in the composition is of the form `X₁ ◁ X₂ ◁ X₃ ◁ f ▷ X₄ ▷ X₅`,
+  where each `Xᵢ` is a object that is not the identity or a tensor and `f` is a non-structural
+  morphisms that is not the identity or a composite.
+
+Note that `X₁ ◁ X₂ ◁ X₃ ◁ f ▷ X₄ ▷ X₅` is actually `X₁ ◁ (X₂ ◁ (X₃ ◁ ((f ▷ X₄) ▷ X₅)))`.
+
+Currently, the simp lemmas don't rewrite `𝟙 X ⊗ f` and `f ⊗ 𝟙 Y` into `X ◁ f` and `f ▷ Y`,
+respectively, since it requires a huge refactoring. We hope to add these simp lemmas soon.
+
 ## References
 * Tensor categories, Etingof, Gelaki, Nikshych, Ostrik,
   http://www-math.mit.edu/~etingof/egnobookfinal.pdf
@@ -193,24 +214,72 @@ attribute [simp] MonoidalCategory.tensor_comp
 attribute [reassoc] MonoidalCategory.associator_naturality
 attribute [reassoc] MonoidalCategory.leftUnitor_naturality
 attribute [reassoc] MonoidalCategory.rightUnitor_naturality
-attribute [reassoc] MonoidalCategory.pentagon
+attribute [reassoc (attr := simp)] MonoidalCategory.pentagon
 attribute [reassoc (attr := simp)] MonoidalCategory.triangle
 
 namespace MonoidalCategory
 
 variable {C : Type u} [𝒞 : Category.{v} C] [MonoidalCategory C]
 
+-- Note: this will be a simp lemma after merging #6307.
 theorem id_tensorHom (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂) :
-    (𝟙 X) ⊗ f = X ◁ f := by
+    𝟙 X ⊗ f = X ◁ f := by
   simp [tensorHom_def]
 
+-- Note: this will be a simp lemma after merging #6307.
 theorem tensorHom_id {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) :
-    f ⊗ (𝟙 Y) = f ▷ Y := by
+    f ⊗ 𝟙 Y = f ▷ Y := by
   simp [tensorHom_def]
 
+theorem whiskerLeft_comp (W : C) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
+    W ◁ (f ≫ g) = W ◁ f ≫ W ◁ g := by
+  intros; simp only [← id_tensorHom, ← tensor_comp, comp_id]
+
+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]
+
+theorem tensor_whiskerLeft (X Y : C) {Z Z' : C} (f : Z ⟶ Z') :
+    (X ⊗ Y) ◁ f = (α_ X Y Z).hom ≫ X ◁ Y ◁ f ≫ (α_ X Y Z').inv := by
+  intros
+  simp only [← id_tensorHom, ← tensorHom_id]
+  rw [← assoc, ← associator_naturality]
+  simp
+
+theorem comp_whiskerRight {W X Y : C} (f : W ⟶ X) (g : X ⟶ Y) (Z : C) :
+    (f ≫ g) ▷ Z = f ▷ Z ≫ g ▷ Z := by
+  intros; simp only [← tensorHom_id, ← tensor_comp, id_comp]
+
+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]
+
+theorem whiskerRight_tensor {X X' : C} (f : X ⟶ X') (Y Z : C) :
+    f ▷ (Y ⊗ Z) = (α_ X Y Z).inv ≫ f ▷ Y ▷ Z ≫ (α_ X' Y Z).hom := by
+  intros
+  simp only [← id_tensorHom, ← tensorHom_id]
+  rw [associator_naturality]
+  simp [tensor_id]
+
+theorem whisker_assoc (X : C) {Y Y' : C} (f : Y ⟶ Y') (Z : C) :
+    (X ◁ f) ▷ Z = (α_ X Y Z).hom ≫ X ◁ f ▷ Z ≫ (α_ X Y' Z).inv := by
+  intros
+  simp only [← id_tensorHom, ← tensorHom_id]
+  rw [← assoc, ← associator_naturality]
+  simp
+
 theorem whisker_exchange {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) :
     W ◁ g ≫ f ▷ Z = f ▷ Y ≫ X ◁ g := by
-  simp [← id_tensorHom, ← tensorHom_id, ← tensor_comp]
+  simp only [← id_tensorHom, ← tensorHom_id, ← tensor_comp, id_comp, comp_id]
+
+attribute [reassoc]
+  whiskerLeft_comp id_whiskerLeft tensor_whiskerLeft comp_whiskerRight whiskerRight_id
+  whiskerRight_tensor whisker_assoc whisker_exchange
+
+attribute [simp]
+  whiskerLeft_id whiskerRight_id
+  whiskerLeft_comp id_whiskerLeft tensor_whiskerLeft comp_whiskerRight id_whiskerRight
+  whiskerRight_tensor whisker_assoc
 
 @[reassoc]
 theorem tensorHom_def' {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) :
@@ -229,42 +298,42 @@ namespace MonoidalCategory
 @[reassoc (attr := simp)]
 theorem whiskerLeft_hom_inv (X : C) {Y Z : C} (f : Y ≅ Z) :
     X ◁ f.hom ≫ X ◁ f.inv = 𝟙 (X ⊗ Y) := by
-  simp [← id_tensorHom, ← tensor_comp]
+  rw [← whiskerLeft_comp, hom_inv_id, whiskerLeft_id]
 
 @[reassoc (attr := simp)]
 theorem hom_inv_whiskerRight {X Y : C} (f : X ≅ Y) (Z : C) :
     f.hom ▷ Z ≫ f.inv ▷ Z = 𝟙 (X ⊗ Z) := by
-  simp [← tensorHom_id, ← tensor_comp]
+  rw [← comp_whiskerRight, hom_inv_id, id_whiskerRight]
 
 @[reassoc (attr := simp)]
 theorem whiskerLeft_inv_hom (X : C) {Y Z : C} (f : Y ≅ Z) :
     X ◁ f.inv ≫ X ◁ f.hom = 𝟙 (X ⊗ Z) := by
-  simp [← id_tensorHom, ← tensor_comp]
+  rw [← whiskerLeft_comp, inv_hom_id, whiskerLeft_id]
 
 @[reassoc (attr := simp)]
 theorem inv_hom_whiskerRight {X Y : C} (f : X ≅ Y) (Z : C) :
     f.inv ▷ Z ≫ f.hom ▷ Z = 𝟙 (Y ⊗ Z) := by
-  simp [← tensorHom_id, ← tensor_comp]
+  rw [← comp_whiskerRight, inv_hom_id, id_whiskerRight]
 
 @[reassoc (attr := simp)]
 theorem whiskerLeft_hom_inv' (X : C) {Y Z : C} (f : Y ⟶ Z) [IsIso f] :
     X ◁ f ≫ X ◁ inv f = 𝟙 (X ⊗ Y) := by
-  simp [← id_tensorHom, ← tensor_comp]
+  rw [← whiskerLeft_comp, IsIso.hom_inv_id, whiskerLeft_id]
 
 @[reassoc (attr := simp)]
 theorem hom_inv_whiskerRight' {X Y : C} (f : X ⟶ Y) [IsIso f] (Z : C) :
     f ▷ Z ≫ inv f ▷ Z = 𝟙 (X ⊗ Z) := by
-  simp [← tensorHom_id, ← tensor_comp]
+  rw [← comp_whiskerRight, IsIso.hom_inv_id, id_whiskerRight]
 
 @[reassoc (attr := simp)]
 theorem whiskerLeft_inv_hom' (X : C) {Y Z : C} (f : Y ⟶ Z) [IsIso f] :
     X ◁ inv f ≫ X ◁ f = 𝟙 (X ⊗ Z) := by
-  simp [← id_tensorHom, ← tensor_comp]
+  rw [← whiskerLeft_comp, IsIso.inv_hom_id, whiskerLeft_id]
 
 @[reassoc (attr := simp)]
 theorem inv_hom_whiskerRight' {X Y : C} (f : X ⟶ Y) [IsIso f] (Z : C) :
     inv f ▷ Z ≫ f ▷ Z = 𝟙 (Y ⊗ Z) := by
-  simp [← tensorHom_id, ← tensor_comp]
+  rw [← comp_whiskerRight, IsIso.inv_hom_id, id_whiskerRight]
 
 /-- The left whiskering of an isomorphism is an isomorphism. -/
 @[simps]
@@ -322,12 +391,21 @@ instance tensor_isIso {W X Y Z : C} (f : W ⟶ X) [IsIso f] (g : Y ⟶ Z) [IsIso
 @[simp]
 theorem inv_tensor {W X Y Z : C} (f : W ⟶ X) [IsIso f] (g : Y ⟶ Z) [IsIso g] :
     inv (f ⊗ g) = inv f ⊗ inv g := by
-  apply IsIso.inv_eq_of_hom_inv_id
-  simp [← tensor_comp]
+  simp [tensorHom_def ,whisker_exchange]
 #align category_theory.monoidal_category.inv_tensor CategoryTheory.MonoidalCategory.inv_tensor
 
 variable {U V W X Y Z : C}
 
+theorem whiskerLeft_dite {P : Prop} [Decidable P]
+    (X : C) {Y Z : C} (f : P → (Y ⟶ Z)) (f' : ¬P → (Y ⟶ Z)) :
+      X ◁ (if h : P then f h else f' h) = if h : P then X ◁ f h else X ◁ f' h := by
+  split_ifs <;> rfl
+
+theorem dite_whiskerRight {P : Prop} [Decidable P]
+    {X Y : C} (f : P → (X ⟶ Y)) (f' : ¬P → (X ⟶ Y)) (Z : C):
+      (if h : P then f h else f' h) ▷ Z = if h : P then f h ▷ Z else f' h ▷ Z := by
+  split_ifs <;> rfl
+
 theorem tensor_dite {P : Prop} [Decidable P] {W X Y Z : C} (f : W ⟶ X) (g : P → (Y ⟶ Z))
     (g' : ¬P → (Y ⟶ Z)) : (f ⊗ if h : P then g h else g' h) = if h : P then f ⊗ g h else f ⊗ g' h :=
   by split_ifs <;> rfl
@@ -338,106 +416,211 @@ theorem dite_tensor {P : Prop} [Decidable P] {W X Y Z : C} (f : W ⟶ X) (g : P
   by split_ifs <;> rfl
 #align category_theory.monoidal_category.dite_tensor CategoryTheory.MonoidalCategory.dite_tensor
 
-@[reassoc, simp]
-theorem comp_tensor_id (f : W ⟶ X) (g : X ⟶ Y) : f ≫ g ⊗ 𝟙 Z = (f ⊗ 𝟙 Z) ≫ (g ⊗ 𝟙 Z) := by
-  rw [← tensor_comp]
-  simp
-#align category_theory.monoidal_category.comp_tensor_id CategoryTheory.MonoidalCategory.comp_tensor_id
+@[simp]
+theorem whiskerLeft_eqToHom (X : C) {Y Z : C} (f : Y = Z) :
+    X ◁ eqToHom f = eqToHom (congr_arg₂ tensorObj rfl f) := by
+  cases f
+  simp only [whiskerLeft_id, eqToHom_refl]
 
-@[reassoc, simp]
-theorem id_tensor_comp (f : W ⟶ X) (g : X ⟶ Y) : 𝟙 Z ⊗ f ≫ g = (𝟙 Z ⊗ f) ≫ (𝟙 Z ⊗ g) := by
-  rw [← tensor_comp]
-  simp
-#align category_theory.monoidal_category.id_tensor_comp CategoryTheory.MonoidalCategory.id_tensor_comp
+@[simp]
+theorem eqToHom_whiskerRight {X Y : C} (f : X = Y) (Z : C) :
+    eqToHom f ▷ Z = eqToHom (congr_arg₂ tensorObj f rfl) := by
+  cases f
+  simp only [id_whiskerRight, eqToHom_refl]
 
-@[reassoc (attr := simp)]
-theorem id_tensor_comp_tensor_id (f : W ⟶ X) (g : Y ⟶ Z) : (𝟙 Y ⊗ f) ≫ (g ⊗ 𝟙 X) = g ⊗ f := by
-  rw [← tensor_comp]
-  simp
-#align category_theory.monoidal_category.id_tensor_comp_tensor_id CategoryTheory.MonoidalCategory.id_tensor_comp_tensor_id
+@[reassoc]
+theorem associator_naturality_left {X X' : C} (f : X ⟶ X') (Y Z : C) :
+    f ▷ Y ▷ Z ≫ (α_ X' Y Z).hom = (α_ X Y Z).hom ≫ f ▷ (Y ⊗ Z) := by simp
 
-@[reassoc (attr := simp)]
-theorem tensor_id_comp_id_tensor (f : W ⟶ X) (g : Y ⟶ Z) : (g ⊗ 𝟙 W) ≫ (𝟙 Z ⊗ f) = g ⊗ f := by
-  rw [← tensor_comp]
-  simp
-#align category_theory.monoidal_category.tensor_id_comp_id_tensor CategoryTheory.MonoidalCategory.tensor_id_comp_id_tensor
+@[reassoc]
+theorem associator_inv_naturality_left {X X' : C} (f : X ⟶ X') (Y Z : C) :
+    f ▷ (Y ⊗ Z) ≫ (α_ X' Y Z).inv = (α_ X Y Z).inv ≫ f ▷ Y ▷ Z := by simp
 
-@[simp]
-theorem rightUnitor_conjugation {X Y : C} (f : X ⟶ Y) :
-    f ⊗ 𝟙 (𝟙_ C) = (ρ_ X).hom ≫ f ≫ (ρ_ Y).inv := by
-  rw [← rightUnitor_naturality_assoc, Iso.hom_inv_id, Category.comp_id]
-#align category_theory.monoidal_category.right_unitor_conjugation CategoryTheory.MonoidalCategory.rightUnitor_conjugation
+@[reassoc]
+theorem whiskerRight_tensor_symm {X X' : C} (f : X ⟶ X') (Y Z : C) :
+    f ▷ Y ▷ Z = (α_ X Y Z).hom ≫ f ▷ (Y ⊗ Z) ≫ (α_ X' Y Z).inv := by simp
 
-@[simp]
-theorem leftUnitor_conjugation {X Y : C} (f : X ⟶ Y) :
-    𝟙 (𝟙_ C) ⊗ f = (λ_ X).hom ≫ f ≫ (λ_ Y).inv := by
-  rw [← leftUnitor_naturality_assoc, Iso.hom_inv_id, Category.comp_id]
-#align category_theory.monoidal_category.left_unitor_conjugation CategoryTheory.MonoidalCategory.leftUnitor_conjugation
+@[reassoc]
+theorem associator_naturality_middle (X : C) {Y Y' : C} (f : Y ⟶ Y') (Z : C) :
+    (X ◁ f) ▷ Z ≫ (α_ X Y' Z).hom = (α_ X Y Z).hom ≫ X ◁ f ▷ Z := by simp
 
 @[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
+theorem associator_inv_naturality_middle (X : C) {Y Y' : C} (f : Y ⟶ Y') (Z : C) :
+    X ◁ f ▷ Z ≫ (α_ X Y' Z).inv = (α_ X Y Z).inv ≫ (X ◁ f) ▷ Z := by simp
 
 @[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
+theorem whisker_assoc_symm (X : C) {Y Y' : C} (f : Y ⟶ Y') (Z : C) :
+    X ◁ f ▷ Z = (α_ X Y Z).inv ≫ (X ◁ f) ▷ Z ≫ (α_ X Y' Z).hom := by simp
 
-theorem tensor_left_iff {X Y : C} (f g : X ⟶ Y) : 𝟙 (𝟙_ C) ⊗ f = 𝟙 (𝟙_ C) ⊗ g ↔ f = g := by simp
-#align category_theory.monoidal_category.tensor_left_iff CategoryTheory.MonoidalCategory.tensor_left_iff
+@[reassoc]
+theorem associator_naturality_right (X Y : C) {Z Z' : C} (f : Z ⟶ Z') :
+    (X ⊗ Y) ◁ f ≫ (α_ X Y Z').hom = (α_ X Y Z).hom ≫ X ◁ Y ◁ f := by simp
 
-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 associator_inv_naturality_right (X Y : C) {Z Z' : C} (f : Z ⟶ Z') :
+    X ◁ Y ◁ f ≫ (α_ X Y Z').inv = (α_ X Y Z).inv ≫ (X ⊗ Y) ◁ f := by simp
+
+@[reassoc]
+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_inv_naturality' {X Y : C} (f : X ⟶ Y) :
+    f ≫ (λ_ Y).inv = (λ_ X).inv ≫ (_ ◁ f) := by simp
+
+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_inv_naturality' {X X' : C} (f : X ⟶ X') :
+    f ≫ (ρ_ X').inv = (ρ_ X).inv ≫ (f ▷ _) := by simp
+
+theorem whiskerRight_id_symm {X Y : C} (f : X ⟶ Y) :
+    f = (ρ_ X).inv ≫ f ▷ 𝟙_ C ≫ (ρ_ Y).hom := by
+  simp
+
+theorem whiskerLeft_iff {X Y : C} (f g : X ⟶ Y) : 𝟙_ C ◁ f = 𝟙_ C ◁ g ↔ f = g := by simp
+
+theorem whiskerRight_iff {X Y : C} (f g : X ⟶ Y) : f ▷ 𝟙_ C = g ▷ 𝟙_ C ↔ f = g := by simp
 
 /-! The lemmas in the next section are true by coherence,
 but we prove them directly as they are used in proving the coherence theorem. -/
 
-
 section
 
-@[reassoc]
-theorem pentagon_inv (W X Y Z : C) :
-    (𝟙 W ⊗ (α_ X Y Z).inv) ≫ (α_ W (X ⊗ Y) Z).inv ≫ ((α_ W X Y).inv ⊗ 𝟙 Z) =
+@[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' :
+    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
+  eq_of_inv_eq_inv (by simp)
 
-@[reassoc, simp]
-theorem rightUnitor_tensor (X Y : C) :
-    (ρ_ (X ⊗ Y)).hom = (α_ X Y (𝟙_ C)).hom ≫ (𝟙 X ⊗ (ρ_ Y).hom) := by
-  rw [← tensor_right_iff, comp_tensor_id, ← cancel_mono (α_ X Y (𝟙_ C)).hom, assoc,
-    associator_naturality, ← triangle_assoc, ← triangle, id_tensor_comp, pentagon_assoc, ←
-    associator_naturality, tensor_id]
-#align category_theory.monoidal_category.right_unitor_tensor CategoryTheory.MonoidalCategory.rightUnitor_tensor
+@[reassoc (attr := simp)]
+theorem pentagon_inv_inv_hom_hom_inv :
+    (α_ W (X ⊗ Y) Z).inv ≫ (α_ W X Y).inv ▷ Z ≫ (α_ (W ⊗ X) Y Z).hom =
+      W ◁ (α_ X Y Z).hom ≫ (α_ W X (Y ⊗ Z)).inv := by
+  rw [← cancel_epi (W ◁ (α_ X Y Z).inv), ← cancel_mono (α_ (W ⊗ X) Y Z).inv]
+  simp
 
-@[reassoc, simp]
-theorem rightUnitor_tensor_inv (X Y : C) :
-    (ρ_ (X ⊗ Y)).inv = (𝟙 X ⊗ (ρ_ Y).inv) ≫ (α_ X Y (𝟙_ C)).inv :=
+@[reassoc (attr := simp)]
+theorem pentagon_inv_hom_hom_hom_inv :
+    (α_ (W ⊗ X) Y Z).inv ≫ (α_ W X Y).hom ▷ Z ≫ (α_ W (X ⊗ Y) Z).hom =
+      (α_ W X (Y ⊗ Z)).hom ≫ W ◁ (α_ X Y Z).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
-  rw [← triangle, Iso.inv_hom_id_assoc]
-#align category_theory.monoidal_category.triangle_assoc_comp_right CategoryTheory.MonoidalCategory.triangle_assoc_comp_right
+theorem pentagon_hom_inv_inv_inv_inv :
+    W ◁ (α_ X Y Z).hom ≫ (α_ W X (Y ⊗ Z)).inv ≫ (α_ (W ⊗ X) Y Z).inv =
+      (α_ W (X ⊗ Y) Z).inv ≫ (α_ W X Y).inv ▷ Z :=
+  by simp [← cancel_epi (W ◁ (α_ X Y Z).inv)]
 
 @[reassoc (attr := simp)]
-theorem triangle_assoc_comp_left_inv (X Y : C) :
-    (𝟙 X ⊗ (λ_ Y).inv) ≫ (α_ X (𝟙_ C) Y).inv = (ρ_ X).inv ⊗ 𝟙 Y := by
-  apply (cancel_mono ((ρ_ X).hom ⊗ 𝟙 Y)).1
-  simp only [triangle_assoc_comp_right, assoc]
-  rw [← id_tensor_comp, Iso.inv_hom_id, ← comp_tensor_id, Iso.inv_hom_id]
-#align category_theory.monoidal_category.triangle_assoc_comp_left_inv CategoryTheory.MonoidalCategory.triangle_assoc_comp_left_inv
+theorem pentagon_hom_hom_inv_hom_hom :
+    (α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom ≫ W ◁ (α_ X Y Z).inv =
+      (α_ W X Y).hom ▷ Z ≫ (α_ W (X ⊗ Y) Z).hom :=
+  eq_of_inv_eq_inv (by simp)
+
+@[reassoc (attr := simp)]
+theorem pentagon_hom_inv_inv_inv_hom :
+    (α_ W X (Y ⊗ Z)).hom ≫ W ◁ (α_ X Y Z).inv ≫ (α_ W (X ⊗ Y) Z).inv =
+      (α_ (W ⊗ X) Y Z).inv ≫ (α_ W X Y).hom ▷ Z := by
+  rw [← cancel_epi (α_ W X (Y ⊗ Z)).inv, ← cancel_mono ((α_ W X Y).inv ▷ Z)]
+  simp
+
+@[reassoc (attr := simp)]
+theorem pentagon_hom_hom_inv_inv_hom :
+    (α_ W (X ⊗ Y) Z).hom ≫ W ◁ (α_ X Y Z).hom ≫ (α_ W X (Y ⊗ Z)).inv =
+      (α_ W X Y).inv ▷ Z ≫ (α_ (W ⊗ X) Y Z).hom :=
+  eq_of_inv_eq_inv (by simp)
+
+@[reassoc (attr := simp)]
+theorem pentagon_inv_hom_hom_hom_hom :
+    (α_ W X Y).inv ▷ Z ≫ (α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom =
+      (α_ W (X ⊗ Y) Z).hom ≫ W ◁ (α_ X Y Z).hom :=
+  by simp [← cancel_epi ((α_ W X Y).hom ▷ Z)]
+
+@[reassoc (attr := simp)]
+theorem pentagon_inv_inv_hom_inv_inv :
+    (α_ W X (Y ⊗ Z)).inv ≫ (α_ (W ⊗ X) Y Z).inv ≫ (α_ W X Y).hom ▷ Z =
+      W ◁ (α_ X Y Z).inv ≫ (α_ W (X ⊗ Y) Z).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) :
+    (α_ X (𝟙_ C) Y).inv ≫ ((ρ_ X).hom ▷ Y) = X ◁ (λ_ Y).hom := by
+  rw [← triangle', Iso.inv_hom_id_assoc]
+
+@[reassoc (attr := simp)]
+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)]
+
+@[reassoc (attr := simp)]
+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)]
+
+/-- We state it as a simp lemma, which is regarded as an involved version of
+`id_whiskerRight X Y : 𝟙 X ▷ Y = 𝟙 (X ⊗ Y)`.
+-/
+@[reassoc, simp]
+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]
+
+@[reassoc, simp]
+theorem leftUnitor_inv_whiskerRight (X Y : C) :
+    (λ_ X).inv ▷ Y = (λ_ (X ⊗ Y)).inv ≫ (α_ (𝟙_ C) X Y).inv :=
+  eq_of_inv_eq_inv (by simp)
+
+@[reassoc, simp]
+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',
+      associator_inv_naturality_right]
+
+@[reassoc, simp]
+theorem whiskerLeft_rightUnitor_inv (X Y : C) :
+    X ◁ (ρ_ Y).inv = (ρ_ (X ⊗ Y)).inv ≫ (α_ X Y (𝟙_ C)).hom :=
+  eq_of_inv_eq_inv (by simp)
+
+@[reassoc]
+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) :
+    (λ_ (X ⊗ Y)).inv = (λ_ X).inv ▷ Y ≫ (α_ (𝟙_ C) X Y).hom := by simp
+
+@[reassoc]
+theorem rightUnitor_tensor' (X Y : C) :
+    (ρ_ (X ⊗ Y)).hom = (α_ X Y (𝟙_ C)).hom ≫ X ◁ (ρ_ Y).hom := by simp
+
+@[reassoc]
+theorem rightUnitor_tensor_inv' (X Y : C) :
+    (ρ_ (X ⊗ Y)).inv = X ◁ (ρ_ Y).inv ≫ (α_ X Y (𝟙_ C)).inv := by simp
 
 end
 
 @[reassoc]
 theorem associator_inv_naturality {X Y Z X' Y' Z' : C} (f : X ⟶ X') (g : Y ⟶ Y') (h : Z ⟶ Z') :
     (f ⊗ g ⊗ h) ≫ (α_ X' Y' Z').inv = (α_ X Y Z).inv ≫ ((f ⊗ g) ⊗ h) := by
-  rw [comp_inv_eq, assoc, associator_naturality]
-  simp
+  simp [tensorHom_def]
 #align category_theory.monoidal_category.associator_inv_naturality CategoryTheory.MonoidalCategory.associator_inv_naturality
 
 @[reassoc, simp]
@@ -469,49 +652,49 @@ theorem id_tensor_associator_inv_naturality {X Y Z X' : C} (f : X ⟶ X') :
 @[reassoc (attr := simp)]
 theorem hom_inv_id_tensor {V W X Y Z : C} (f : V ≅ W) (g : X ⟶ Y) (h : Y ⟶ Z) :
     (f.hom ⊗ g) ≫ (f.inv ⊗ h) = (𝟙 V ⊗ g) ≫ (𝟙 V ⊗ h) := by
-  rw [← tensor_comp, f.hom_inv_id, id_tensor_comp]
+  rw [← tensor_comp, f.hom_inv_id]; simp [id_tensorHom]
 #align category_theory.monoidal_category.hom_inv_id_tensor CategoryTheory.MonoidalCategory.hom_inv_id_tensor
 
 @[reassoc (attr := simp)]
 theorem inv_hom_id_tensor {V W X Y Z : C} (f : V ≅ W) (g : X ⟶ Y) (h : Y ⟶ Z) :
     (f.inv ⊗ g) ≫ (f.hom ⊗ h) = (𝟙 W ⊗ g) ≫ (𝟙 W ⊗ h) := by
-  rw [← tensor_comp, f.inv_hom_id, id_tensor_comp]
+  rw [← tensor_comp, f.inv_hom_id]; simp [id_tensorHom]
 #align category_theory.monoidal_category.inv_hom_id_tensor CategoryTheory.MonoidalCategory.inv_hom_id_tensor
 
 @[reassoc (attr := simp)]
 theorem tensor_hom_inv_id {V W X Y Z : C} (f : V ≅ W) (g : X ⟶ Y) (h : Y ⟶ Z) :
     (g ⊗ f.hom) ≫ (h ⊗ f.inv) = (g ⊗ 𝟙 V) ≫ (h ⊗ 𝟙 V) := by
-  rw [← tensor_comp, f.hom_inv_id, comp_tensor_id]
+  rw [← tensor_comp, f.hom_inv_id]; simp [tensorHom_id]
 #align category_theory.monoidal_category.tensor_hom_inv_id CategoryTheory.MonoidalCategory.tensor_hom_inv_id
 
 @[reassoc (attr := simp)]
 theorem tensor_inv_hom_id {V W X Y Z : C} (f : V ≅ W) (g : X ⟶ Y) (h : Y ⟶ Z) :
     (g ⊗ f.inv) ≫ (h ⊗ f.hom) = (g ⊗ 𝟙 W) ≫ (h ⊗ 𝟙 W) := by
-  rw [← tensor_comp, f.inv_hom_id, comp_tensor_id]
+  rw [← tensor_comp, f.inv_hom_id]; simp [tensorHom_id]
 #align category_theory.monoidal_category.tensor_inv_hom_id CategoryTheory.MonoidalCategory.tensor_inv_hom_id
 
 @[reassoc (attr := simp)]
 theorem hom_inv_id_tensor' {V W X Y Z : C} (f : V ⟶ W) [IsIso f] (g : X ⟶ Y) (h : Y ⟶ Z) :
     (f ⊗ g) ≫ (inv f ⊗ h) = (𝟙 V ⊗ g) ≫ (𝟙 V ⊗ h) := by
-  rw [← tensor_comp, IsIso.hom_inv_id, id_tensor_comp]
+  rw [← tensor_comp, IsIso.hom_inv_id]; simp [id_tensorHom]
 #align category_theory.monoidal_category.hom_inv_id_tensor' CategoryTheory.MonoidalCategory.hom_inv_id_tensor'
 
 @[reassoc (attr := simp)]
 theorem inv_hom_id_tensor' {V W X Y Z : C} (f : V ⟶ W) [IsIso f] (g : X ⟶ Y) (h : Y ⟶ Z) :
     (inv f ⊗ g) ≫ (f ⊗ h) = (𝟙 W ⊗ g) ≫ (𝟙 W ⊗ h) := by
-  rw [← tensor_comp, IsIso.inv_hom_id, id_tensor_comp]
+  rw [← tensor_comp, IsIso.inv_hom_id]; simp [id_tensorHom]
 #align category_theory.monoidal_category.inv_hom_id_tensor' CategoryTheory.MonoidalCategory.inv_hom_id_tensor'
 
 @[reassoc (attr := simp)]
 theorem tensor_hom_inv_id' {V W X Y Z : C} (f : V ⟶ W) [IsIso f] (g : X ⟶ Y) (h : Y ⟶ Z) :
     (g ⊗ f) ≫ (h ⊗ inv f) = (g ⊗ 𝟙 V) ≫ (h ⊗ 𝟙 V) := by
-  rw [← tensor_comp, IsIso.hom_inv_id, comp_tensor_id]
+  rw [← tensor_comp, IsIso.hom_inv_id]; simp [tensorHom_id]
 #align category_theory.monoidal_category.tensor_hom_inv_id' CategoryTheory.MonoidalCategory.tensor_hom_inv_id'
 
 @[reassoc (attr := simp)]
 theorem tensor_inv_hom_id' {V W X Y Z : C} (f : V ⟶ W) [IsIso f] (g : X ⟶ Y) (h : Y ⟶ Z) :
     (g ⊗ inv f) ≫ (h ⊗ f) = (g ⊗ 𝟙 W) ≫ (h ⊗ 𝟙 W) := by
-  rw [← tensor_comp, IsIso.inv_hom_id, comp_tensor_id]
+  rw [← tensor_comp, IsIso.inv_hom_id]; simp [tensorHom_id]
 #align category_theory.monoidal_category.tensor_inv_hom_id' CategoryTheory.MonoidalCategory.tensor_inv_hom_id'
 
 /--
@@ -557,8 +740,111 @@ abbrev ofTensorHom [MonoidalCategoryStruct C]
   tensorHom_def := by intros; simp [← id_tensorHom, ← tensorHom_id, ← tensor_comp]
   whiskerLeft_id := by intros; simp [← id_tensorHom, ← tensor_id]
   id_whiskerRight := by intros; simp [← tensorHom_id, tensor_id]
-  pentagon := pentagon
-  triangle := triangle
+  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]
+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]
+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
+
+@[reassoc]
+theorem id_tensor_comp_tensor_id (f : W ⟶ X) (g : Y ⟶ Z) : (𝟙 Y ⊗ f) ≫ (g ⊗ 𝟙 X) = g ⊗ f := by
+  rw [← tensor_comp]
+  simp
+#align category_theory.monoidal_category.id_tensor_comp_tensor_id CategoryTheory.MonoidalCategory.id_tensor_comp_tensor_id
+
+@[reassoc]
+theorem tensor_id_comp_id_tensor (f : W ⟶ X) (g : Y ⟶ Z) : (g ⊗ 𝟙 W) ≫ (𝟙 Z ⊗ f) = g ⊗ f := by
+  rw [← tensor_comp]
+  simp
+#align category_theory.monoidal_category.tensor_id_comp_id_tensor CategoryTheory.MonoidalCategory.tensor_id_comp_id_tensor
+
+theorem tensor_left_iff {X Y : C} (f g : X ⟶ Y) : 𝟙 (𝟙_ C) ⊗ f = 𝟙 (𝟙_ C) ⊗ g ↔ f = g := by simp
+#align category_theory.monoidal_category.tensor_left_iff CategoryTheory.MonoidalCategory.tensor_left_iff
+
+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
+
+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
+
+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_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
+  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
 
@@ -662,6 +948,8 @@ def rightUnitorNatIso : tensorUnitRight C ≅ 𝟭 C :=
 
 section
 
+attribute [local simp] id_tensorHom tensorHom_id 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]
 
@@ -676,10 +964,7 @@ def tensorLeft (X : C) : C ⥤ C where
 tensoring on the left with `Y`, and then again with `X`.
 -/
 def tensorLeftTensor (X Y : C) : tensorLeft (X ⊗ Y) ≅ tensorLeft Y ⋙ tensorLeft X :=
-  NatIso.ofComponents (associator _ _) fun {Z} {Z'} f => by
-    dsimp
-    rw [← tensor_id]
-    apply associator_naturality
+  NatIso.ofComponents (associator _ _) fun {Z} {Z'} f => by simp
 #align category_theory.monoidal_category.tensor_left_tensor CategoryTheory.MonoidalCategory.tensorLeftTensor
 
 @[simp]
@@ -742,10 +1027,7 @@ variable {C : Type u} [Category.{v} C] [MonoidalCategory.{v} C]
 tensoring on the right with `X`, and then again with `Y`.
 -/
 def tensorRightTensor (X Y : C) : tensorRight (X ⊗ Y) ≅ tensorRight X ⋙ tensorRight Y :=
-  NatIso.ofComponents (fun Z => (associator Z X Y).symm) fun {Z} {Z'} f => by
-    dsimp
-    rw [← tensor_id]
-    apply associator_inv_naturality
+  NatIso.ofComponents (fun Z => (associator Z X Y).symm) fun {Z} {Z'} f => by simp
 #align category_theory.monoidal_category.tensor_right_tensor CategoryTheory.MonoidalCategory.tensorRightTensor
 
 @[simp]
@@ -773,7 +1055,7 @@ variable (C₂ : Type u₂) [Category.{v₂} C₂] [MonoidalCategory.{v₂} C₂
 
 attribute [local simp] associator_naturality leftUnitor_naturality rightUnitor_naturality pentagon
 
-@[simps! tensorObj tensorHom tensorUnit associator]
+@[simps! tensorObj tensorHom tensorUnit whiskerLeft whiskerRight associator]
 instance prodMonoidal : MonoidalCategory (C₁ × C₂) where
   tensorObj X Y := (X.1 ⊗ Y.1, X.2 ⊗ Y.2)
   tensorHom f g := (f.1 ⊗ g.1, f.2 ⊗ g.2)
diff --git a/Mathlib/CategoryTheory/Monoidal/Center.lean b/Mathlib/CategoryTheory/Monoidal/Center.lean
index b02aaa4b60e53..19d7d10a0f7e6 100644
--- a/Mathlib/CategoryTheory/Monoidal/Center.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Center.lean
@@ -176,47 +176,33 @@ def tensorHom {X₁ Y₁ X₂ Y₂ : Center C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶
       associator_naturality_assoc, ← id_tensor_comp, tensor_id_comp_id_tensor]
 #align category_theory.center.tensor_hom CategoryTheory.Center.tensorHom
 
+section
+
+attribute [local simp] id_tensorHom tensorHom_id
+
 /-- Auxiliary definition for the `MonoidalCategory` instance on `Center C`. -/
 @[simps]
 def tensorUnit : Center C :=
-  ⟨𝟙_ C,
-    { β := fun U => λ_ U ≪≫ (ρ_ U).symm
-      monoidal := fun U U' => by simp
-      naturality := fun f => by
-        dsimp
-        rw [leftUnitor_naturality_assoc, rightUnitor_inv_naturality, Category.assoc] }⟩
+  ⟨𝟙_ C, { β := fun U => λ_ U ≪≫ (ρ_ U).symm }⟩
 #align category_theory.center.tensor_unit CategoryTheory.Center.tensorUnit
 
 /-- Auxiliary definition for the `MonoidalCategory` instance on `Center C`. -/
 def associator (X Y Z : Center C) : tensorObj (tensorObj X Y) Z ≅ tensorObj X (tensorObj Y Z) :=
-  isoMk
-    ⟨(α_ X.1 Y.1 Z.1).hom, fun U => by
-      dsimp
-      simp only [comp_tensor_id, id_tensor_comp, ← tensor_id, associator_conjugation]
-      coherence⟩
+  isoMk ⟨(α_ X.1 Y.1 Z.1).hom, fun U => by simp⟩
 #align category_theory.center.associator CategoryTheory.Center.associator
 
 /-- Auxiliary definition for the `MonoidalCategory` instance on `Center C`. -/
 def leftUnitor (X : Center C) : tensorObj tensorUnit X ≅ X :=
-  isoMk
-    ⟨(λ_ X.1).hom, fun U => by
-      dsimp
-      simp only [Category.comp_id, Category.assoc, tensor_inv_hom_id, comp_tensor_id,
-        tensor_id_comp_id_tensor, triangle_assoc_comp_right_inv]
-      rw [← leftUnitor_tensor, leftUnitor_naturality, leftUnitor_tensor'_assoc]⟩
+  isoMk ⟨(λ_ X.1).hom, fun U => by simp⟩
 #align category_theory.center.left_unitor CategoryTheory.Center.leftUnitor
 
 /-- Auxiliary definition for the `MonoidalCategory` instance on `Center C`. -/
 def rightUnitor (X : Center C) : tensorObj X tensorUnit ≅ X :=
-  isoMk
-    ⟨(ρ_ X.1).hom, fun U => by
-      dsimp
-      simp only [tensor_id_comp_id_tensor_assoc, triangle_assoc, id_tensor_comp, Category.assoc]
-      rw [← tensor_id_comp_id_tensor_assoc (ρ_ U).inv, cancel_epi, ← rightUnitor_tensor_inv_assoc,
-        ← rightUnitor_inv_naturality_assoc]
-      simp⟩
+  isoMk ⟨(ρ_ X.1).hom, fun U => by simp⟩
 #align category_theory.center.right_unitor CategoryTheory.Center.rightUnitor
 
+end
+
 section
 
 attribute [local simp] associator_naturality leftUnitor_naturality rightUnitor_naturality pentagon
@@ -226,6 +212,7 @@ attribute [local simp] Center.associator Center.leftUnitor Center.rightUnitor
 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`
diff --git a/Mathlib/CategoryTheory/Monoidal/CoherenceLemmas.lean b/Mathlib/CategoryTheory/Monoidal/CoherenceLemmas.lean
index 3bb669914909a..976570b1031bf 100644
--- a/Mathlib/CategoryTheory/Monoidal/CoherenceLemmas.lean
+++ b/Mathlib/CategoryTheory/Monoidal/CoherenceLemmas.lean
@@ -27,12 +27,12 @@ variable {C : Type*} [Category C] [MonoidalCategory C]
 
 -- See Proposition 2.2.4 of <http://www-math.mit.edu/~etingof/egnobookfinal.pdf>
 @[reassoc]
-theorem leftUnitor_tensor' (X Y : C) :
+theorem leftUnitor_tensor'' (X Y : C) :
     (α_ (𝟙_ C) X Y).hom ≫ (λ_ (X ⊗ Y)).hom = (λ_ 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, simp]
+@[reassoc]
 theorem leftUnitor_tensor (X Y : C) :
     (λ_ (X ⊗ Y)).hom = (α_ (𝟙_ C) X Y).inv ≫ ((λ_ X).hom ⊗ 𝟙 Y) := by
   coherence
diff --git a/Mathlib/CategoryTheory/Monoidal/End.lean b/Mathlib/CategoryTheory/Monoidal/End.lean
index 04b6ffaff04e4..a8e56563035b6 100644
--- a/Mathlib/CategoryTheory/Monoidal/End.lean
+++ b/Mathlib/CategoryTheory/Monoidal/End.lean
@@ -90,6 +90,8 @@ attribute [local instance] endofunctorMonoidalCategory
 -- porting note: used `dsimp [endofunctorMonoidalCategory]` when necessary instead
 -- attribute [local reducible] endofunctorMonoidalCategory
 
+attribute [local simp] id_tensorHom tensorHom_id
+
 /-- Tensoring on the right gives a monoidal functor from `C` into endofunctors of `C`.
 -/
 @[simps!]
@@ -97,30 +99,10 @@ def tensoringRightMonoidal [MonoidalCategory.{v} C] : MonoidalFunctor C (C ⥤ C
   { tensoringRight C with
     ε := (rightUnitorNatIso C).inv
     μ := fun X Y => { app := fun Z => (α_ Z X Y).hom }
-    -- The proof will be automated after merging #6307.
-    μ_natural_left := fun f X => by
-      ext Z
-      dsimp
-      simp only [← id_tensor_comp_tensor_id f (𝟙 X), id_tensor_comp, ← tensor_id, Category.assoc,
-        associator_naturality, associator_naturality_assoc]
-      simp only [tensor_id, Category.id_comp]
-    μ_natural_right := fun X g => by
-      ext Z
-      dsimp
-      simp only [← id_tensor_comp_tensor_id (𝟙 X) g, id_tensor_comp, ← tensor_id, Category.assoc,
-        associator_naturality, associator_naturality_assoc]
-      simp only [tensor_id, Category.comp_id]
-    associativity := fun X Y Z => by
-      ext W
-      simp [pentagon]
     μ_isIso := fun X Y =>
       -- We could avoid needing to do this explicitly by
       -- constructing a partially applied analogue of `associatorNatIso`.
-      ⟨⟨{ app := fun Z => (α_ Z X Y).inv
-          naturality := fun Z Z' f => by
-            dsimp
-            rw [← associator_inv_naturality]
-            simp },
+      ⟨⟨{ app := fun Z => (α_ Z X Y).inv },
           by aesop_cat⟩⟩ }
 #align category_theory.tensoring_right_monoidal CategoryTheory.tensoringRightMonoidal
 
@@ -335,7 +317,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/Coherence.lean b/Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean
index 54face86b9cf9..9d76a833a3a0f 100644
--- a/Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean
@@ -252,9 +252,8 @@ def normalizeIso : tensorFunc C ≅ normalize' C :=
         simp only [← Category.assoc]
         congr 4
         simp only [Category.assoc, ← cancel_epi (𝟙 (inclusionObj n.as) ⊗ (α_ X₁ X₂ X₃).inv),
-          pentagon_inv_assoc (inclusionObj n.as) X₁ X₂ X₃,
-          tensor_inv_hom_id_assoc, tensor_id, Category.id_comp, Iso.inv_hom_id,
-          Category.comp_id]
+          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]
       · ext n
         dsimp
         rw [mk_α_inv, NatTrans.comp_app, NatTrans.comp_app]
@@ -272,7 +271,7 @@ def normalizeIso : tensorFunc C ≅ normalize' C :=
         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_left_inv_assoc, inv_hom_id_tensor_assoc, tensor_id,
+        simp only [triangle_assoc_comp_right_assoc, tensor_inv_hom_id_assoc, tensor_id,
           Category.id_comp, Category.comp_id]
         rfl
       · ext n
diff --git a/Mathlib/CategoryTheory/Monoidal/Functor.lean b/Mathlib/CategoryTheory/Monoidal/Functor.lean
index 26649e79610a2..e899d4b4ece1e 100644
--- a/Mathlib/CategoryTheory/Monoidal/Functor.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Functor.lean
@@ -115,11 +115,11 @@ section
 variable {C D}
 
 @[reassoc (attr := simp)]
-theorem  LaxMonoidalFunctor.μ_natural (F : LaxMonoidalFunctor C D) {X Y X' Y' : C}
+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 [← tensor_id_comp_id_tensor_assoc]
-  rw [F.μ_natural_right, F.μ_natural_left_assoc]
+  rw [tensorHom_def, ← id_tensorHom, ← tensorHom_id]
+  simp only [assoc, μ_natural_right, μ_natural_left_assoc]
   rw [← F.map_comp, tensor_id_comp_id_tensor]
 
 /--
@@ -334,18 +334,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 Y Z f => by
-    convert F.μ_natural (𝟙 X) f using 2
-    simp
+  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 Y Z f => by
-    convert F.μ_natural f (𝟙 X) using 2
-    simp
+  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
@@ -401,19 +397,7 @@ def comp : LaxMonoidalFunctor.{v₁, v₃} C E :=
       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]
-    left_unitality := fun X => by
-      dsimp
-      rw [G.left_unitality, comp_tensor_id, Category.assoc, Category.assoc]
-      apply congr_arg
-      rw [F.left_unitality, map_comp, ← NatTrans.id_app, ← Category.assoc, ←
-        LaxMonoidalFunctor.μ_natural, NatTrans.id_app, map_id, ← Category.assoc, map_comp]
-    right_unitality := fun X => by
-      dsimp
-      rw [G.right_unitality, id_tensor_comp, Category.assoc, Category.assoc]
-      apply congr_arg
-      rw [F.right_unitality, map_comp, ← NatTrans.id_app, ← Category.assoc, ←
-        LaxMonoidalFunctor.μ_natural, NatTrans.id_app, map_id, ← Category.assoc, map_comp] }
+        G.toFunctor.map_comp, F.associativity] }
 #align category_theory.lax_monoidal_functor.comp CategoryTheory.LaxMonoidalFunctor.comp
 
 @[inherit_doc]
diff --git a/Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean b/Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean
index c005ad6d3be94..765730247e217 100644
--- a/Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean
+++ b/Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean
@@ -77,6 +77,8 @@ 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`.
@@ -163,6 +165,8 @@ 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/Limits.lean b/Mathlib/CategoryTheory/Monoidal/Limits.lean
index b5553b1312089..813036093795a 100644
--- a/Mathlib/CategoryTheory/Monoidal/Limits.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Limits.lean
@@ -78,7 +78,7 @@ instance limitLaxMonoidal : LaxMonoidal fun F : J ⥤ C => limit F := .ofTensorH
     slice_rhs 2 3 =>
       rw [← id_tensor_comp, limit.lift_π]
       dsimp
-    dsimp; simp)
+    dsimp; rw [id_tensor_comp_tensor_id])
   (left_unitality := fun X => by
     ext j; dsimp
     simp only [limit.lift_map, Category.assoc, limit.lift_π, Cones.postcompose_obj_pt,
diff --git a/Mathlib/CategoryTheory/Monoidal/Opposite.lean b/Mathlib/CategoryTheory/Monoidal/Opposite.lean
index 3ad2597b81651..c2461d32479ac 100644
--- a/Mathlib/CategoryTheory/Monoidal/Opposite.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Opposite.lean
@@ -169,6 +169,8 @@ 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 08a1baae71b96..3f8b6dbf511b2 100644
--- a/Mathlib/CategoryTheory/Monoidal/Preadditive.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Preadditive.lean
@@ -63,11 +63,11 @@ theorem zero_tensor {W X Y Z : C} (f : Y ⟶ Z) : (0 : W ⟶ X) ⊗ f = 0 := by
 
 theorem tensor_add {W X Y Z : C} (f : W ⟶ X) (g h : Y ⟶ Z) : f ⊗ (g + h) = f ⊗ g + f ⊗ h := by
   rw [← tensor_id_comp_id_tensor]
-  simp
+  simp [tensor_id_comp_id_tensor]
 
 theorem add_tensor {W X Y Z : C} (f g : W ⟶ X) (h : Y ⟶ Z) : (f + g) ⊗ h = f ⊗ h + g ⊗ h := by
   rw [← tensor_id_comp_id_tensor]
-  simp
+  simp [tensor_id_comp_id_tensor]
 
 end MonoidalPreadditive
 
diff --git a/Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean b/Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean
index 43522f0502b8b..e2262551c3d6c 100644
--- a/Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean
@@ -468,7 +468,7 @@ theorem tensorLeftHomEquiv_symm_coevaluation_comp_id_tensor {Y Y' Z : C} [ExactP
   slice_lhs 2 3 => rw [associator_inv_naturality]
   slice_lhs 3 4 => rw [tensor_id, id_tensor_comp_tensor_id, ← tensor_id_comp_id_tensor]
   slice_lhs 1 3 => rw [coevaluation_evaluation]
-  simp
+  simp [id_tensorHom]
 #align category_theory.tensor_left_hom_equiv_symm_coevaluation_comp_id_tensor CategoryTheory.tensorLeftHomEquiv_symm_coevaluation_comp_id_tensor
 
 @[simp]
@@ -495,7 +495,7 @@ theorem tensorRightHomEquiv_symm_coevaluation_comp_tensor_id {Y Y' Z : C} [Exact
   slice_lhs 2 3 => rw [associator_naturality]
   slice_lhs 3 4 => rw [tensor_id, tensor_id_comp_id_tensor, ← id_tensor_comp_tensor_id]
   slice_lhs 1 3 => rw [evaluation_coevaluation]
-  simp
+  simp [tensorHom_id]
 #align category_theory.tensor_right_hom_equiv_symm_coevaluation_comp_tensor_id CategoryTheory.tensorRightHomEquiv_symm_coevaluation_comp_tensor_id
 
 @[simp]
@@ -506,7 +506,7 @@ theorem tensorLeftHomEquiv_id_tensor_comp_evaluation {Y Z : C} [HasLeftDual Z] (
   slice_lhs 3 4 => rw [← associator_naturality]
   slice_lhs 2 3 => rw [tensor_id, tensor_id_comp_id_tensor, ← id_tensor_comp_tensor_id]
   slice_lhs 3 5 => rw [evaluation_coevaluation]
-  simp
+  simp [id_tensorHom]
 #align category_theory.tensor_left_hom_equiv_id_tensor_comp_evaluation CategoryTheory.tensorLeftHomEquiv_id_tensor_comp_evaluation
 
 @[simp]
@@ -531,7 +531,7 @@ theorem tensorRightHomEquiv_tensor_id_comp_evaluation {X Y : C} [HasRightDual X]
   slice_lhs 3 4 => rw [← associator_inv_naturality]
   slice_lhs 2 3 => rw [tensor_id, id_tensor_comp_tensor_id, ← tensor_id_comp_id_tensor]
   slice_lhs 3 5 => rw [coevaluation_evaluation]
-  simp
+  simp [tensorHom_id]
 #align category_theory.tensor_right_hom_equiv_tensor_id_comp_evaluation CategoryTheory.tensorRightHomEquiv_tensor_id_comp_evaluation
 
 -- Next four lemmas passing `fᘁ` or `ᘁf` through (co)evaluations.
diff --git a/Mathlib/CategoryTheory/Monoidal/Transport.lean b/Mathlib/CategoryTheory/Monoidal/Transport.lean
index 6afb99b0e151e..e9e66fdc33602 100644
--- a/Mathlib/CategoryTheory/Monoidal/Transport.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Transport.lean
@@ -103,40 +103,22 @@ abbrev induced [MonoidalCategoryStruct D] (F : D ⥤ C) [Faithful F]
   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,
-      Iso.trans_hom, Iso.symm_hom, tensorIso_hom, Iso.refl_hom, Functor.map_id, comp_tensor_id,
-      associator_conjugation, tensor_id, assoc, id_tensor_comp, Iso.hom_inv_id_assoc,
-      tensor_hom_inv_id_assoc, id_comp, hom_inv_id_tensor_assoc, Iso.inv_hom_id_assoc,
-      id_tensor_comp_tensor_id_assoc, Iso.cancel_iso_inv_left]
-    slice_lhs 6 8 =>
-      rw [← id_tensor_comp, hom_inv_id_tensor, tensor_id, comp_id,
-        tensor_id]
-    simp only [comp_id, assoc, pentagon_assoc, Iso.inv_hom_id_assoc,
-      ← associator_naturality_assoc, tensor_id, tensor_id_comp_id_tensor_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]
+    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
-    have := leftUnitor_naturality (F.map f)
-    simp only [Functor.map_comp, fData.tensorHom_eq, Functor.map_id, fData.leftUnitor_eq,
-      Iso.trans_assoc, Iso.trans_hom, Iso.symm_hom, tensorIso_hom, Iso.refl_hom, assoc,
-      Iso.hom_inv_id_assoc, id_tensor_comp_tensor_id_assoc, Iso.cancel_iso_inv_left]
-    rw [← this, ← assoc, ← tensor_comp, id_comp, comp_id]
+    simp [fData.leftUnitor_eq, fData.tensorHom_eq, whisker_exchange_assoc,
+      id_tensorHom, tensorHom_id]
   rightUnitor_naturality {X Y : D} f := F.map_injective <| by
-    have := rightUnitor_naturality (F.map f)
-    simp only [Functor.map_comp, fData.tensorHom_eq, Functor.map_id, fData.rightUnitor_eq,
-      Iso.trans_assoc, Iso.trans_hom, Iso.symm_hom, tensorIso_hom, Iso.refl_hom, assoc,
-      Iso.hom_inv_id_assoc, tensor_id_comp_id_tensor_assoc, Iso.cancel_iso_inv_left]
-    rw [← this, ← assoc, ← tensor_comp, id_comp, comp_id]
+    simp [fData.rightUnitor_eq, fData.tensorHom_eq, ← whisker_exchange_assoc,
+      id_tensorHom, tensorHom_id]
   associator_naturality {X₁ X₂ X₃ Y₁ Y₂ Y₃} f₁ f₂ f₃ := F.map_injective <| by
-    have := associator_naturality (F.map f₁) (F.map f₂) (F.map f₃)
-    simp [fData.associator_eq, fData.tensorHom_eq]
-    simp_rw [← assoc, ← tensor_comp, assoc, Iso.hom_inv_id, ← assoc]
-    congr 1
-    conv_rhs => rw [← comp_id (F.map f₁), ← id_comp (F.map f₁)]
-    simp only [tensor_comp]
-    simp only [tensor_id, comp_id, assoc, tensor_hom_inv_id_assoc, id_comp]
-    slice_rhs 2 3 => rw [← this]
-    simp only [← assoc, Iso.inv_hom_id, comp_id]
-    congr 2
-    simp_rw [← tensor_comp, id_comp]
-
+    simp [fData.tensorHom_eq, fData.associator_eq, tensorHom_def, whisker_exchange_assoc]
 
 /--
 We can upgrade `F` to a monoidal functor from `D` to `E` with the induced structure.
diff --git a/Mathlib/CategoryTheory/Monoidal/Types/Coyoneda.lean b/Mathlib/CategoryTheory/Monoidal/Types/Coyoneda.lean
index e421ed3e56026..215e05af141ca 100644
--- a/Mathlib/CategoryTheory/Monoidal/Types/Coyoneda.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Types/Coyoneda.lean
@@ -33,6 +33,8 @@ 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] :
diff --git a/Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat/Monoidal.lean b/Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat/Monoidal.lean
index 64362a66e5e54..45332314b6198 100644
--- a/Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat/Monoidal.lean
+++ b/Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat/Monoidal.lean
@@ -81,6 +81,16 @@ noncomputable instance instMonoidalCategory : MonoidalCategory (QuadraticModuleC
     (forget₂ (QuadraticModuleCat R) (ModuleCat R))
     { μIso := fun X Y => Iso.refl _
       εIso := Iso.refl _
+      leftUnitor_eq := fun X => by
+        simp only [forget₂_obj, forget₂_map, Iso.refl_symm, Iso.trans_assoc, Iso.trans_hom,
+          Iso.refl_hom, tensorIso_hom, MonoidalCategory.tensorHom_id]
+        erw [MonoidalCategory.id_whiskerRight, Category.id_comp, Category.id_comp]
+        rfl
+      rightUnitor_eq := fun X => by
+        simp only [forget₂_obj, forget₂_map, Iso.refl_symm, Iso.trans_assoc, Iso.trans_hom,
+          Iso.refl_hom, tensorIso_hom, MonoidalCategory.id_tensorHom]
+        erw [MonoidalCategory.whiskerLeft_id, Category.id_comp, Category.id_comp]
+        rfl
       associator_eq := fun X Y Z => by
         dsimp only [forget₂_obj, forget₂_map_associator_hom]
         simp only [eqToIso_refl, Iso.refl_trans, Iso.refl_symm, Iso.trans_hom, tensorIso_hom,

From 3d7a0b0d12c1fb1619dbcbaf4ad885845362ebb3 Mon Sep 17 00:00:00 2001
From: Yuma Mizuno <mizuno.y.aj@gmail.com>
Date: Sun, 28 Jan 2024 13:51:59 +0900
Subject: [PATCH 2/4] revert

---
 Mathlib/CategoryTheory/Monoidal/End.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/CategoryTheory/Monoidal/End.lean b/Mathlib/CategoryTheory/Monoidal/End.lean
index a8e56563035b6..829147a0e031b 100644
--- a/Mathlib/CategoryTheory/Monoidal/End.lean
+++ b/Mathlib/CategoryTheory/Monoidal/End.lean
@@ -90,7 +90,7 @@ attribute [local instance] endofunctorMonoidalCategory
 -- porting note: used `dsimp [endofunctorMonoidalCategory]` when necessary instead
 -- attribute [local reducible] endofunctorMonoidalCategory
 
-attribute [local simp] id_tensorHom tensorHom_id
+attribute [local simp] id_tensorHom tensorHom_id in
 
 /-- Tensoring on the right gives a monoidal functor from `C` into endofunctors of `C`.
 -/
@@ -317,7 +317,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

From 043e280868f9e11765cc1d83b804ad5eac41a8cc Mon Sep 17 00:00:00 2001
From: Yuma Mizuno <mizuno.y.aj@gmail.com>
Date: Sun, 28 Jan 2024 14:01:26 +0900
Subject: [PATCH 3/4] clean up

---
 Mathlib/CategoryTheory/Monoidal/Category.lean | 17 ++++++++---------
 1 file changed, 8 insertions(+), 9 deletions(-)

diff --git a/Mathlib/CategoryTheory/Monoidal/Category.lean b/Mathlib/CategoryTheory/Monoidal/Category.lean
index f7fc5b296aff1..7a13f5e7abf6f 100644
--- a/Mathlib/CategoryTheory/Monoidal/Category.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Category.lean
@@ -231,14 +231,17 @@ theorem tensorHom_id {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) :
     f ⊗ 𝟙 Y = f ▷ Y := by
   simp [tensorHom_def]
 
+@[reassoc, simp]
 theorem whiskerLeft_comp (W : C) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
     W ◁ (f ≫ g) = W ◁ f ≫ W ◁ g := by
   intros; simp only [← id_tensorHom, ← tensor_comp, comp_id]
 
+@[reassoc, simp]
 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]
 
+@[reassoc, simp]
 theorem tensor_whiskerLeft (X Y : C) {Z Z' : C} (f : Z ⟶ Z') :
     (X ⊗ Y) ◁ f = (α_ X Y Z).hom ≫ X ◁ Y ◁ f ≫ (α_ X Y Z').inv := by
   intros
@@ -246,14 +249,17 @@ theorem tensor_whiskerLeft (X Y : C) {Z Z' : C} (f : Z ⟶ Z') :
   rw [← assoc, ← associator_naturality]
   simp
 
+@[reassoc, simp]
 theorem comp_whiskerRight {W X Y : C} (f : W ⟶ X) (g : X ⟶ Y) (Z : C) :
     (f ≫ g) ▷ Z = f ▷ Z ≫ g ▷ Z := by
   intros; simp only [← tensorHom_id, ← tensor_comp, id_comp]
 
+@[reassoc, simp]
 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]
 
+@[reassoc, simp]
 theorem whiskerRight_tensor {X X' : C} (f : X ⟶ X') (Y Z : C) :
     f ▷ (Y ⊗ Z) = (α_ X Y Z).inv ≫ f ▷ Y ▷ Z ≫ (α_ X' Y Z).hom := by
   intros
@@ -261,6 +267,7 @@ theorem whiskerRight_tensor {X X' : C} (f : X ⟶ X') (Y Z : C) :
   rw [associator_naturality]
   simp [tensor_id]
 
+@[reassoc, simp]
 theorem whisker_assoc (X : C) {Y Y' : C} (f : Y ⟶ Y') (Z : C) :
     (X ◁ f) ▷ Z = (α_ X Y Z).hom ≫ X ◁ f ▷ Z ≫ (α_ X Y' Z).inv := by
   intros
@@ -268,19 +275,11 @@ theorem whisker_assoc (X : C) {Y Y' : C} (f : Y ⟶ Y') (Z : C) :
   rw [← assoc, ← associator_naturality]
   simp
 
+@[reassoc]
 theorem whisker_exchange {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) :
     W ◁ g ≫ f ▷ Z = f ▷ Y ≫ X ◁ g := by
   simp only [← id_tensorHom, ← tensorHom_id, ← tensor_comp, id_comp, comp_id]
 
-attribute [reassoc]
-  whiskerLeft_comp id_whiskerLeft tensor_whiskerLeft comp_whiskerRight whiskerRight_id
-  whiskerRight_tensor whisker_assoc whisker_exchange
-
-attribute [simp]
-  whiskerLeft_id whiskerRight_id
-  whiskerLeft_comp id_whiskerLeft tensor_whiskerLeft comp_whiskerRight id_whiskerRight
-  whiskerRight_tensor whisker_assoc
-
 @[reassoc]
 theorem tensorHom_def' {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) :
     f ⊗ g = X₁ ◁ g ≫ f ▷ Y₂ :=

From 0b3fa867b31c05a17a64a10bbdcb8d6e3a56cf2c Mon Sep 17 00:00:00 2001
From: Yuma Mizuno <mizuno.y.aj@gmail.com>
Date: Wed, 31 Jan 2024 04:12:39 +0900
Subject: [PATCH 4/4] reassoc

---
 Mathlib/CategoryTheory/Monoidal/Category.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Mathlib/CategoryTheory/Monoidal/Category.lean b/Mathlib/CategoryTheory/Monoidal/Category.lean
index 7a13f5e7abf6f..7ffcd258802f9 100644
--- a/Mathlib/CategoryTheory/Monoidal/Category.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Category.lean
@@ -811,11 +811,13 @@ theorem triangle_assoc_comp_left_inv (X Y : C) :
   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