refactor(CategoryTheory/Monoidal/Braided): use monoidalComp in the proofs (#10078)

- [x] depends on: #10061

Author: yuma-mizuno

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

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

Mathlib/CategoryTheory/Monoidal/Braided.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

Mathlib/CategoryTheory/Monoidal/Category.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

Mathlib/CategoryTheory/Monoidal/Center.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 :=