refactor(category_theory/monoidal): rearrange simp lemmas to work better with coherence (#13409)

Change the direction of some simp lemma for monoidal categories, and remove some unused lemmas.

This PR is effectively a "no-op": no substantial changes to proofs. However, it should enable making `coherence` more powerful soon (following suggestions of @yuma-mizuno)!



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: kim-em

src/category_theory/monoidal/End.lean

@@ -50,7 +50,9 @@ def tensoring_right_monoidal [monoidal_category.{v} C] : monoidal_functor C (C 
   μ := λ X Y,
   { app := λ Z, (α_ Z X Y).hom,
     naturality' := λ Z Z' f, by { dsimp, rw associator_naturality, simp, } },
-  μ_natural' := λ X Y X' Y' f g, by { ext Z, dsimp, simp [associator_naturality], },
+  μ_natural' := λ X Y X' Y' f g, by { ext Z, dsimp,
+    simp only [←id_tensor_comp_tensor_id g f, id_tensor_comp, ←tensor_id, category.assoc,
+      associator_naturality, associator_naturality_assoc], },
   associativity' := λ X Y Z, by { ext W, dsimp, simp [pentagon], },
   left_unitality' := λ X, by { ext Y, dsimp, rw [category.id_comp, triangle, ←tensor_comp], simp, },
   right_unitality' := λ X,

src/category_theory/monoidal/Mon_.lean

@@ -58,9 +58,8 @@ def trivial : Mon_ C :=
 { X := 𝟙_ C,
   one := 𝟙 _,
   mul := (λ_ _).hom,
-  mul_assoc' :=
-    by simp_rw [triangle_assoc, iso.cancel_iso_hom_right, tensor_right_iff, unitors_equal],
-  mul_one' := by simp [unitors_equal] }
+  mul_assoc' := by coherence,
+  mul_one' := by coherence }
 
 instance : inhabited (Mon_ C) := ⟨trivial C⟩
 

src/category_theory/monoidal/braided.lean

@@ -81,16 +81,16 @@ I couldn't find a detailed proof in print, but this is discussed in:
 variables (C : Type u₁) [category.{v₁} C] [monoidal_category C] [braided_category C]
 
 lemma braiding_left_unitor_aux₁ (X : C) :
-  (α_ (𝟙_ C) (𝟙_ C) X).hom ≫ (𝟙 _ ⊗ (β_ X (𝟙_ C)).inv) ≫ (α_ _ X _).inv ≫ ((λ_ X).hom ⊗ 𝟙 _) =
-  ((λ_ _).hom ⊗ 𝟙 X) ≫ (β_ X _).inv :=
+  (α_ (𝟙_ C) (𝟙_ C) X).hom ≫ (𝟙 (𝟙_ C) ⊗ (β_ X (𝟙_ C)).inv) ≫ (α_ _ X _).inv ≫ ((λ_ X).hom ⊗ 𝟙 _) =
+  ((λ_ _).hom ⊗ 𝟙 X) ≫ (β_ X (𝟙_ C)).inv :=
 by { rw [←left_unitor_tensor, left_unitor_naturality], simp, }
 
 lemma braiding_left_unitor_aux₂ (X : 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)))
-         : by simp
+         : 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], }
@@ -111,16 +111,16 @@ lemma braiding_left_unitor (X : C) : (β_ X (𝟙_ C)).hom ≫ (λ_ X).hom = (ρ
 by rw [←tensor_right_iff, comp_tensor_id, braiding_left_unitor_aux₂]
 
 lemma braiding_right_unitor_aux₁ (X : C) :
-  (α_ X (𝟙_ C) (𝟙_ C)).inv ≫ ((β_ (𝟙_ C) X).inv ⊗ 𝟙 _) ≫ (α_ _ X _).hom ≫ (𝟙 _ ⊗ (ρ_ X).hom) =
-  (𝟙 X ⊗ (ρ_ _).hom) ≫ (β_ _ X).inv :=
+  (α_ X (𝟙_ C) (𝟙_ C)).inv ≫ ((β_ (𝟙_ C) X).inv ⊗ 𝟙 (𝟙_ C)) ≫ (α_ _ X _).hom ≫ (𝟙 _ ⊗ (ρ_ X).hom) =
+  (𝟙 X ⊗ (ρ_ _).hom) ≫ (β_ (𝟙_ C) X).inv :=
 by { rw [←right_unitor_tensor, right_unitor_naturality], simp, }
 
 lemma braiding_right_unitor_aux₂ (X : C) :
   ((𝟙 (𝟙_ 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)
-         : by simp
+         : 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], }

src/category_theory/monoidal/category.lean

@@ -186,43 +186,35 @@ by { rw [←tensor_comp], simp }
   (g ⊗ (𝟙 W)) ≫ ((𝟙 Z) ⊗ f) = g ⊗ f :=
 by { rw [←tensor_comp], simp }
 
+@[simp]
+lemma right_unitor_conjugation {X Y : C} (f : X ⟶ Y) :
+  (f ⊗ (𝟙 (𝟙_ C))) = (ρ_ X).hom ≫ f ≫ (ρ_ Y).inv :=
+by rw [←right_unitor_naturality_assoc, iso.hom_inv_id, category.comp_id]
+
+@[simp]
+lemma left_unitor_conjugation {X Y : C} (f : X ⟶ Y) :
+  ((𝟙 (𝟙_ C)) ⊗ f) = (λ_ X).hom ≫ f ≫ (λ_ Y).inv :=
+by rw [←left_unitor_naturality_assoc, iso.hom_inv_id, category.comp_id]
+
 @[reassoc]
 lemma left_unitor_inv_naturality {X X' : C} (f : X ⟶ X') :
   f ≫ (λ_ X').inv = (λ_ X).inv ≫ (𝟙 _ ⊗ f) :=
-begin
-  apply (cancel_mono (λ_ X').hom).1,
-  simp only [assoc, comp_id, iso.inv_hom_id],
-  rw [left_unitor_naturality, ←category.assoc, iso.inv_hom_id, category.id_comp]
-end
+by simp
 
 @[reassoc]
 lemma right_unitor_inv_naturality {X X' : C} (f : X ⟶ X') :
   f ≫ (ρ_ X').inv = (ρ_ X).inv ≫ (f ⊗ 𝟙 _) :=
-begin
-  apply (cancel_mono (ρ_ X').hom).1,
-  simp only [assoc, comp_id, iso.inv_hom_id],
-  rw [right_unitor_naturality, ←category.assoc, iso.inv_hom_id, category.id_comp]
-end
+by simp
 
-@[simp]
-lemma right_unitor_conjugation {X Y : C} (f : X ⟶ Y) :
-  (ρ_ X).inv ≫ (f ⊗ (𝟙 (𝟙_ C))) ≫ (ρ_ Y).hom = f :=
-by rw [right_unitor_naturality, ←category.assoc, iso.inv_hom_id, category.id_comp]
-
-@[simp]
-lemma left_unitor_conjugation {X Y : C} (f : X ⟶ Y) :
-  (λ_ X).inv ≫ ((𝟙 (𝟙_ C)) ⊗ f) ≫ (λ_ Y).hom = f :=
-by rw [left_unitor_naturality, ←category.assoc, iso.inv_hom_id, category.id_comp]
-
-@[simp] lemma tensor_left_iff
+lemma tensor_left_iff
   {X Y : C} (f g : X ⟶ Y) :
   ((𝟙 (𝟙_ C)) ⊗ f = (𝟙 (𝟙_ C)) ⊗ g) ↔ (f = g) :=
-by { rw [←cancel_mono (λ_ Y).hom, left_unitor_naturality, left_unitor_naturality], simp }
+by simp
 
-@[simp] lemma tensor_right_iff
+lemma tensor_right_iff
   {X Y : C} (f g : X ⟶ Y) :
   (f ⊗ (𝟙 (𝟙_ C)) = g ⊗ (𝟙 (𝟙_ C))) ↔ (f = g) :=
-by { rw [←cancel_mono (ρ_ Y).hom, right_unitor_naturality, right_unitor_naturality], simp }
+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. -/
@@ -247,13 +239,9 @@ lemma right_unitor_tensor_inv (X Y : C) :
   ((ρ_ (X ⊗ Y)).inv) = ((𝟙 X) ⊗ (ρ_ Y).inv) ≫ (α_ X Y (𝟙_ C)).inv :=
 eq_of_inv_eq_inv (by simp)
 
-lemma triangle_assoc_comp_left (X Y : C) :
-  (α_ X (𝟙_ C) Y).hom ≫ ((𝟙 X) ⊗ (λ_ Y).hom) = (ρ_ X).hom ⊗ 𝟙 Y :=
-monoidal_category.triangle X Y
-
 @[simp, reassoc] lemma triangle_assoc_comp_right (X Y : C) :
   (α_ X (𝟙_ C) Y).inv ≫ ((ρ_ X).hom ⊗ 𝟙 Y) = ((𝟙 X) ⊗ (λ_ Y).hom) :=
-by rw [←triangle_assoc_comp_left, iso.inv_hom_id_assoc]
+by rw [←triangle, iso.inv_hom_id_assoc]
 
 @[simp, reassoc] lemma triangle_assoc_comp_left_inv (X Y : C) :
   ((𝟙 X) ⊗ (λ_ Y).inv) ≫ (α_ X (𝟙_ C) Y).inv = ((ρ_ X).inv ⊗ 𝟙 Y) :=
@@ -270,55 +258,47 @@ lemma associator_inv_naturality {X Y Z X' Y' Z' : C} (f : X ⟶ X') (g : Y ⟶ Y
   (f ⊗ (g ⊗ h)) ≫ (α_ X' Y' Z').inv = (α_ X Y Z).inv ≫ ((f ⊗ g) ⊗ h) :=
 by { rw [comp_inv_eq, assoc, associator_naturality], simp }
 
-@[reassoc]
-lemma id_tensor_associator_naturality {X Y Z Z' : C} (h : Z ⟶ Z') :
-  (𝟙 (X ⊗ Y) ⊗ h) ≫ (α_ X Y Z').hom = (α_ X Y Z).hom ≫ (𝟙 X ⊗ (𝟙 Y ⊗ h)) :=
-by { rw [←tensor_id, associator_naturality], }
-
-@[reassoc]
-lemma id_tensor_associator_inv_naturality {X Y Z X' : C} (f : X ⟶ X')  :
-  (f ⊗ 𝟙 (Y ⊗ Z)) ≫ (α_ X' Y Z).inv = (α_ X Y Z).inv ≫ ((f ⊗ 𝟙 Y) ⊗ 𝟙 Z) :=
-by { rw [←tensor_id, associator_inv_naturality] }
-
-@[reassoc]
+@[reassoc, simp]
 lemma associator_conjugation {X X' Y Y' Z Z' : C} (f : X ⟶ X') (g : Y ⟶ Y') (h : Z ⟶ Z') :
-  (α_ X Y Z).hom ≫ (f ⊗ (g ⊗ h)) ≫ (α_ X' Y' Z').inv = (f ⊗ g) ⊗ h :=
+  (f ⊗ g) ⊗ h = (α_ X Y Z).hom ≫ (f ⊗ (g ⊗ h)) ≫ (α_ X' Y' Z').inv :=
 by rw [associator_inv_naturality, hom_inv_id_assoc]
 
 @[reassoc]
 lemma associator_inv_conjugation {X X' Y Y' Z Z' : C} (f : X ⟶ X') (g : Y ⟶ Y') (h : Z ⟶ Z') :
-  (α_ X Y Z).inv ≫ ((f ⊗ g) ⊗ h) ≫ (α_ X' Y' Z').hom = f ⊗ g ⊗ h :=
+  f ⊗ g ⊗ h = (α_ X Y Z).inv ≫ ((f ⊗ g) ⊗ h) ≫ (α_ X' Y' Z').hom :=
 by rw [associator_naturality, inv_hom_id_assoc]
 
+-- TODO these next two lemmas aren't so fundamental, and perhaps could be removed
+-- (replacing their usages by their proofs).
 @[reassoc]
-lemma right_unitor_inv_comp_tensor (f : W ⟶ X) (g : 𝟙_ C ⟶ Z) :
-  (ρ_ _).inv ≫ (f ⊗ g) = f ≫ (ρ_ _).inv ≫ (𝟙 _ ⊗ g) :=
-by { slice_rhs 1 2 { rw right_unitor_inv_naturality }, simp }
+lemma id_tensor_associator_naturality {X Y Z Z' : C} (h : Z ⟶ Z') :
+  (𝟙 (X ⊗ Y) ⊗ h) ≫ (α_ X Y Z').hom = (α_ X Y Z).hom ≫ (𝟙 X ⊗ (𝟙 Y ⊗ h)) :=
+by { rw [←tensor_id, associator_naturality], }
 
 @[reassoc]
-lemma left_unitor_inv_comp_tensor (f : W ⟶ X) (g : 𝟙_ C ⟶ Z) :
-  (λ_ _).inv ≫ (g ⊗ f) = f ≫ (λ_ _).inv ≫ (g ⊗ 𝟙 _) :=
-by { slice_rhs 1 2 { rw left_unitor_inv_naturality }, simp }
+lemma id_tensor_associator_inv_naturality {X Y Z X' : C} (f : X ⟶ X')  :
+  (f ⊗ 𝟙 (Y ⊗ Z)) ≫ (α_ X' Y Z).inv = (α_ X Y Z).inv ≫ ((f ⊗ 𝟙 Y) ⊗ 𝟙 Z) :=
+by { rw [←tensor_id, associator_inv_naturality] }
 
 @[simp, reassoc]
 lemma 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 ≫ h) :=
-by rw [←tensor_comp, f.hom_inv_id]
+  (f.hom ⊗ g) ≫ (f.inv ⊗ h) = (𝟙 V ⊗ g) ≫ (𝟙 V ⊗ h) :=
+by rw [←tensor_comp, f.hom_inv_id, id_tensor_comp]
 
 @[simp, reassoc]
 lemma 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 ≫ h) :=
-by rw [←tensor_comp, f.inv_hom_id]
+  (f.inv ⊗ g) ≫ (f.hom ⊗ h) = (𝟙 W ⊗ g) ≫ (𝟙 W ⊗ h) :=
+by rw [←tensor_comp, f.inv_hom_id, id_tensor_comp]
 
 @[simp, reassoc]
 lemma 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 ≫ h) ⊗ 𝟙 V :=
-by rw [←tensor_comp, f.hom_inv_id]
+  (g ⊗ f.hom) ≫ (h ⊗ f.inv) = (g ⊗ 𝟙 V) ≫ (h ⊗ 𝟙 V) :=
+by rw [←tensor_comp, f.hom_inv_id, comp_tensor_id]
 
 @[simp, reassoc]
 lemma 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 ≫ h) ⊗ 𝟙 W :=
-by rw [←tensor_comp, f.inv_hom_id]
+  (g ⊗ f.inv) ≫ (h ⊗ f.hom) = (g ⊗ 𝟙 W) ≫ (h ⊗ 𝟙 W) :=
+by rw [←tensor_comp, f.inv_hom_id, comp_tensor_id]
 
 end
 

src/category_theory/monoidal/center.lean

@@ -127,10 +127,10 @@ def tensor_obj (X Y : center C) : center C :=
       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, },
+      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,
     end,
@@ -175,7 +175,7 @@ def tensor_unit : center C :=
 def associator (X Y Z : center C) : tensor_obj (tensor_obj X Y) Z ≅ tensor_obj X (tensor_obj Y Z) :=
 iso_mk ⟨(α_ X.1 Y.1 Z.1).hom, λ U, begin
   dsimp,
-  simp only [comp_tensor_id, id_tensor_comp, ←tensor_id, ←associator_conjugation],
+  simp only [comp_tensor_id, id_tensor_comp, ←tensor_id, associator_conjugation],
   coherence,
 end⟩
 

src/category_theory/monoidal/free/coherence.lean

@@ -195,8 +195,9 @@ begin
     simp only [discrete.functor_map_id, iso.cancel_iso_inv_left, category.assoc],
     dsimp, simp only [category.comp_id] },
   { dsimp,
-    simp only [←(iso.eq_comp_inv _).1 (right_unitor_tensor_inv _ _), iso.hom_inv_id_assoc,
-      right_unitor_conjugation, discrete.functor_map_id, category.assoc],
+    simp only [←(iso.eq_comp_inv _).1 (right_unitor_tensor_inv _ _), right_unitor_conjugation,
+      discrete.functor_map_id, category.assoc,
+      iso.hom_inv_id, iso.hom_inv_id_assoc, iso.inv_hom_id, iso.inv_hom_id_assoc],
     dsimp, simp only [category.comp_id], },
   { dsimp at *,
     rw [id_tensor_comp, category.assoc, f_ih_g ⟦f_g⟧, ←category.assoc, f_ih_f ⟦f_f⟧, category.assoc,

src/category_theory/monoidal/opposite.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import category_theory.monoidal.category
+import category_theory.monoidal.coherence
 
 /-!
 # Monoidal opposites
@@ -115,38 +115,11 @@ instance monoidal_category_op : monoidal_category Cᵒᵖ :=
   associator := λ X Y Z, (α_ (unop X) (unop Y) (unop Z)).symm.op,
   left_unitor := λ X, (λ_ (unop X)).symm.op,
   right_unitor := λ X, (ρ_ (unop X)).symm.op,
-  associator_naturality' :=
-  begin
-    intros,
-    apply quiver.hom.unop_inj,
-    simp [associator_inv_naturality],
-  end,
-  left_unitor_naturality' :=
-  begin
-    intros,
-    apply quiver.hom.unop_inj,
-    simp [left_unitor_inv_naturality],
-  end,
-  right_unitor_naturality' :=
-  begin
-    intros,
-    apply quiver.hom.unop_inj,
-    simp [right_unitor_inv_naturality],
-  end,
-  triangle' :=
-  begin
-    intros,
-    apply quiver.hom.unop_inj,
-    dsimp,
-    simp,
-  end,
-  pentagon' :=
-  begin
-    intros,
-    apply quiver.hom.unop_inj,
-    dsimp,
-    simp [pentagon_inv],
-  end }
+  associator_naturality' := by { intros, apply quiver.hom.unop_inj, simp, },
+  left_unitor_naturality' := by { intros, apply quiver.hom.unop_inj, simp, },
+  right_unitor_naturality' := by { intros, apply quiver.hom.unop_inj, simp, },
+  triangle' := by { intros, apply quiver.hom.unop_inj, coherence, },
+  pentagon' := by { intros, apply quiver.hom.unop_inj, coherence, }, }
 
 lemma op_tensor_obj (X Y : Cᵒᵖ) : X ⊗ Y = op (unop X ⊗ unop Y) := rfl
 lemma op_tensor_unit : (𝟙_ Cᵒᵖ) = op (𝟙_ C) := rfl
@@ -158,38 +131,11 @@ instance monoidal_category_mop : monoidal_category Cᴹᵒᵖ :=
   associator := λ X Y Z, (α_ (unmop Z) (unmop Y) (unmop X)).symm.mop,
   left_unitor := λ X, (ρ_ (unmop X)).mop,
   right_unitor := λ X, (λ_ (unmop X)).mop,
-  associator_naturality' :=
-  begin
-    intros,
-    apply unmop_inj,
-    simp [associator_inv_naturality],
-  end,
-  left_unitor_naturality' :=
-  begin
-    intros,
-    apply unmop_inj,
-    simp [right_unitor_naturality],
-  end,
-  right_unitor_naturality' :=
-  begin
-    intros,
-    apply unmop_inj,
-    simp [left_unitor_naturality],
-  end,
-  triangle' :=
-  begin
-    intros,
-    apply unmop_inj,
-    dsimp,
-    simp,
-  end,
-  pentagon' :=
-  begin
-    intros,
-    apply unmop_inj,
-    dsimp,
-    simp [pentagon_inv],
-  end }
+  associator_naturality' := by { intros, apply unmop_inj, simp, },
+  left_unitor_naturality' := by { intros, apply unmop_inj, simp, },
+  right_unitor_naturality' := by { intros, apply unmop_inj, simp, },
+  triangle' := by { intros, apply unmop_inj, coherence, },
+  pentagon' := by { intros, apply unmop_inj, coherence, }, }
 
 lemma mop_tensor_obj (X Y : Cᴹᵒᵖ) : X ⊗ Y = mop (unmop Y ⊗ unmop X) := rfl
 lemma mop_tensor_unit : (𝟙_ Cᴹᵒᵖ) = mop (𝟙_ C) := rfl

src/category_theory/monoidal/transport.lean

@@ -170,8 +170,8 @@ def lax_to_transported (e : C ≌ D) : lax_monoidal_functor C (transported e) :=
     conv_rhs { rw [←id_tensor_comp_tensor_id _ (e.unit_inv.app X)], },
     dsimp only [functor.comp_obj],
     slice_rhs 3 4 { rw [←id_tensor_comp, iso.hom_inv_id_app], dsimp, rw [tensor_id] },
-    simp only [id_comp],
-    simp [associator_naturality],
+    simp only [associator_conjugation, ←tensor_id, ←tensor_comp, iso.inv_hom_id,
+      iso.inv_hom_id_assoc, category.assoc, category.id_comp, category.comp_id],
   end,
   left_unitality' := λ X,
   begin
@@ -180,8 +180,7 @@ def lax_to_transported (e : C ≌ D) : lax_monoidal_functor C (transported e) :=
     rw equivalence.counit_app_functor,
     simp only [←e.functor.map_comp],
     congr' 1,
-    rw [←left_unitor_naturality],
-    simp,
+    simp only [←left_unitor_naturality, id_comp, ←tensor_comp_assoc, comp_id],
   end,
   right_unitality' := λ X,
   begin
@@ -190,8 +189,7 @@ def lax_to_transported (e : C ≌ D) : lax_monoidal_functor C (transported e) :=
     rw equivalence.counit_app_functor,
     simp only [←e.functor.map_comp],
     congr' 1,
-    rw [←right_unitor_naturality],
-    simp,
+    simp only [←right_unitor_naturality, id_comp, ←tensor_comp_assoc, comp_id],
   end, }.
 
 /--