feat(CategoryTheory/Monoidal): replace 𝟙 X ⊗ f with X ◁ f (#10912)

We set `id_tensorHom` and `tensorHom_id` as simp lemmas. Partially extracted from #6307.

Author: yuma-mizuno

Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean

@@ -85,7 +85,7 @@ noncomputable instance instMonoidalCategory : MonoidalCategory (AlgebraCat.{u} R
       leftUnitor_eq := fun X => by
         dsimp only [forget₂_module_obj, forget₂_module_map, Iso.refl_symm, Iso.trans_hom,
           Iso.refl_hom, tensorIso_hom]
-        simp only [MonoidalCategory.leftUnitor_conjugation, Category.id_comp, Iso.hom_inv_id]
+        erw [Category.id_comp, MonoidalCategory.tensor_id, Category.id_comp]
         rfl
       rightUnitor_eq := fun X => by
         dsimp

Mathlib/CategoryTheory/Bicategory/SingleObj.lean

@@ -68,8 +68,6 @@ protected def star : MonoidalSingleObj C :=
   PUnit.unit
 #align category_theory.monoidal_single_obj.star CategoryTheory.MonoidalSingleObj.star
 
-attribute [local simp] id_tensorHom tensorHom_id in
-
 /-- The monoidal functor from the endomorphisms of the single object
 when we promote a monoidal category to a single object bicategory,
 to the original monoidal category.

Mathlib/CategoryTheory/Closed/Monoidal.lean

@@ -72,7 +72,7 @@ def unitClosed : Closed (𝟙_ C) where
                 right_inv := by aesop_cat }
             homEquiv_naturality_left_symm := fun f g => by
               dsimp
-              rw [leftUnitor_naturality'_assoc]
+              rw [leftUnitor_naturality_assoc]
             -- This used to be automatic before leanprover/lean4#2644
             homEquiv_naturality_right := by  -- aesop failure
               dsimp

Mathlib/CategoryTheory/Enriched/Basic.lean

@@ -53,10 +53,10 @@ class EnrichedCategory (C : Type u₁) where
   Hom : C → C → V
   id (X : C) : 𝟙_ V ⟶ Hom X X
   comp (X Y Z : C) : Hom X Y ⊗ Hom Y Z ⟶ Hom X Z
-  id_comp (X Y : C) : (λ_ (Hom X Y)).inv ≫ (id X ⊗ 𝟙 _) ≫ comp X X Y = 𝟙 _ := by aesop_cat
-  comp_id (X Y : C) : (ρ_ (Hom X Y)).inv ≫ (𝟙 _ ⊗ id Y) ≫ comp X Y Y = 𝟙 _ := by aesop_cat
-  assoc (W X Y Z : C) : (α_ _ _ _).inv ≫ (comp W X Y ⊗ 𝟙 _) ≫ comp W Y Z =
-    (𝟙 _ ⊗ comp X Y Z) ≫ comp W X Z := by aesop_cat
+  id_comp (X Y : C) : (λ_ (Hom X Y)).inv ≫ id X ▷ _ ≫ comp X X Y = 𝟙 _ := by aesop_cat
+  comp_id (X Y : C) : (ρ_ (Hom X Y)).inv ≫ _ ◁ id Y ≫ comp X Y Y = 𝟙 _ := by aesop_cat
+  assoc (W X Y Z : C) : (α_ _ _ _).inv ≫ comp W X Y ▷ _ ≫ comp W Y Z =
+    _ ◁ comp X Y Z ≫ comp W X Z := by aesop_cat
 #align category_theory.enriched_category CategoryTheory.EnrichedCategory
 
 notation X " ⟶[" V "] " Y:10 => (EnrichedCategory.Hom X Y : V)
@@ -78,20 +78,20 @@ def eComp (X Y Z : C) : ((X ⟶[V] Y) ⊗ Y ⟶[V] Z) ⟶ X ⟶[V] Z :=
 -- We don't just use `restate_axiom` here; that would leave `V` as an implicit argument.
 @[reassoc (attr := simp)]
 theorem e_id_comp (X Y : C) :
-    (λ_ (X ⟶[V] Y)).inv ≫ (eId V X ⊗ 𝟙 _) ≫ eComp V X X Y = 𝟙 (X ⟶[V] Y) :=
+    (λ_ (X ⟶[V] Y)).inv ≫ eId V X ▷ _ ≫ eComp V X X Y = 𝟙 (X ⟶[V] Y) :=
   EnrichedCategory.id_comp X Y
 #align category_theory.e_id_comp CategoryTheory.e_id_comp
 
 @[reassoc (attr := simp)]
 theorem e_comp_id (X Y : C) :
-    (ρ_ (X ⟶[V] Y)).inv ≫ (𝟙 _ ⊗ eId V Y) ≫ eComp V X Y Y = 𝟙 (X ⟶[V] Y) :=
+    (ρ_ (X ⟶[V] Y)).inv ≫ _ ◁ eId V Y ≫ eComp V X Y Y = 𝟙 (X ⟶[V] Y) :=
   EnrichedCategory.comp_id X Y
 #align category_theory.e_comp_id CategoryTheory.e_comp_id
 
 @[reassoc (attr := simp)]
 theorem e_assoc (W X Y Z : C) :
-    (α_ _ _ _).inv ≫ (eComp V W X Y ⊗ 𝟙 _) ≫ eComp V W Y Z =
-      (𝟙 _ ⊗ eComp V X Y Z) ≫ eComp V W X Z :=
+    (α_ _ _ _).inv ≫ eComp V W X Y ▷ _ ≫ eComp V W Y Z =
+      _ ◁ eComp V X Y Z ≫ eComp V W X Z :=
   EnrichedCategory.assoc W X Y Z
 #align category_theory.e_assoc CategoryTheory.e_assoc
 
@@ -114,18 +114,23 @@ instance (F : LaxMonoidalFunctor V W) : EnrichedCategory W (TransportEnrichment
   id := fun X : C => F.ε ≫ F.map (eId V X)
   comp := fun X Y Z : C => F.μ _ _ ≫ F.map (eComp V X Y Z)
   id_comp X Y := by
-    rw [comp_tensor_id, Category.assoc, ← F.toFunctor.map_id, F.μ_natural_assoc,
-      F.toFunctor.map_id, F.left_unitality_inv_assoc, ← F.toFunctor.map_comp, ←
-      F.toFunctor.map_comp, e_id_comp, F.toFunctor.map_id]
+    simp only [comp_whiskerRight, Category.assoc, LaxMonoidalFunctor.μ_natural_left_assoc,
+      LaxMonoidalFunctor.left_unitality_inv_assoc]
+    simp_rw [← F.map_comp]
+    convert F.map_id _
+    simp
   comp_id X Y := by
-    rw [id_tensor_comp, Category.assoc, ← F.toFunctor.map_id, F.μ_natural_assoc,
-      F.toFunctor.map_id, F.right_unitality_inv_assoc, ← F.toFunctor.map_comp, ←
-      F.toFunctor.map_comp, e_comp_id, F.toFunctor.map_id]
+    simp only [MonoidalCategory.whiskerLeft_comp, Category.assoc,
+      LaxMonoidalFunctor.μ_natural_right_assoc,
+      LaxMonoidalFunctor.right_unitality_inv_assoc]
+    simp_rw [← F.map_comp]
+    convert F.map_id _
+    simp
   assoc P Q R S := by
-    rw [comp_tensor_id, Category.assoc, ← F.toFunctor.map_id, F.μ_natural_assoc,
-      F.toFunctor.map_id, ← F.associativity_inv_assoc, ← F.toFunctor.map_comp, ←
-      F.toFunctor.map_comp, e_assoc, id_tensor_comp, Category.assoc, ← F.toFunctor.map_id,
-      F.μ_natural_assoc, F.toFunctor.map_comp]
+    rw [comp_whiskerRight, Category.assoc, F.μ_natural_left_assoc,
+      ← F.associativity_inv_assoc, ← F.map_comp, ← F.map_comp, e_assoc,
+      F.map_comp, MonoidalCategory.whiskerLeft_comp, Category.assoc,
+      LaxMonoidalFunctor.μ_natural_right_assoc]
 
 end
 

Mathlib/CategoryTheory/Monoidal/Bimod.lean

@@ -255,7 +255,7 @@ theorem one_act_left' : (R.one ▷ _) ≫ actLeft P Q = (λ_ _).hom := by
   slice_lhs 2 3 => rw [whiskerLeft_π_actLeft]
   slice_lhs 1 2 => rw [associator_inv_naturality_left]
   slice_lhs 2 3 => rw [← comp_whiskerRight, one_actLeft]
-  slice_rhs 1 2 => rw [leftUnitor_naturality']
+  slice_rhs 1 2 => rw [leftUnitor_naturality]
   coherence
 set_option linter.uppercaseLean3 false in
 #align Bimod.tensor_Bimod.one_act_left' Bimod.TensorBimod.one_act_left'
@@ -668,7 +668,7 @@ theorem hom_inv_id : hom P ≫ inv P = 𝟙 _ := by
   dsimp only [hom, inv, TensorBimod.X]
   ext; dsimp
   slice_lhs 1 2 => rw [coequalizer.π_desc]
-  slice_lhs 1 2 => rw [leftUnitor_inv_naturality']
+  slice_lhs 1 2 => rw [leftUnitor_inv_naturality]
   slice_lhs 2 3 => rw [whisker_exchange]
   slice_lhs 3 3 => rw [← Iso.inv_hom_id_assoc (α_ R.X R.X P.X) (R.X ◁ P.actLeft)]
   slice_lhs 4 6 => rw [← Category.assoc, ← coequalizer.condition]
@@ -736,7 +736,7 @@ theorem hom_inv_id : hom P ≫ inv P = 𝟙 _ := by
   dsimp only [hom, inv, TensorBimod.X]
   ext; dsimp
   slice_lhs 1 2 => rw [coequalizer.π_desc]
-  slice_lhs 1 2 => rw [rightUnitor_inv_naturality']
+  slice_lhs 1 2 => rw [rightUnitor_inv_naturality]
   slice_lhs 2 3 => rw [← whisker_exchange]
   slice_lhs 3 4 => rw [coequalizer.condition]
   slice_lhs 2 3 => rw [associator_naturality_right]
@@ -858,7 +858,7 @@ theorem id_whiskerLeft_bimod {X Y : Mon_ C} {M N : Bimod X Y} (f : M ⟶ N) :
   slice_rhs 1 2 => rw [coequalizer.π_desc]
   dsimp [LeftUnitorBimod.inv]
   slice_rhs 1 2 => rw [Hom.left_act_hom]
-  slice_rhs 2 3 => rw [leftUnitor_inv_naturality']
+  slice_rhs 2 3 => rw [leftUnitor_inv_naturality]
   slice_rhs 3 4 => rw [whisker_exchange]
   slice_rhs 4 4 => rw [← Iso.inv_hom_id_assoc (α_ X.X X.X N.X) (X.X ◁ N.actLeft)]
   slice_rhs 5 7 => rw [← Category.assoc, ← coequalizer.condition]
@@ -918,7 +918,7 @@ theorem whiskerRight_id_bimod {X Y : Mon_ C} {M N : Bimod X Y} (f : M ⟶ N) :
   slice_rhs 1 2 => rw [coequalizer.π_desc]
   dsimp [RightUnitorBimod.inv]
   slice_rhs 1 2 => rw [Hom.right_act_hom]
-  slice_rhs 2 3 => rw [rightUnitor_inv_naturality']
+  slice_rhs 2 3 => rw [rightUnitor_inv_naturality]
   slice_rhs 3 4 => rw [← whisker_exchange]
   slice_rhs 4 5 => rw [coequalizer.condition]
   slice_rhs 3 4 => rw [associator_naturality_right]

Mathlib/CategoryTheory/Monoidal/Braided.lean

@@ -206,37 +206,37 @@ def braidedCategoryOfFaithful {C D : Type*} [Category C] [Category D] [MonoidalC
     intros
     apply F.map_injective
     refine (cancel_epi (F.μ ?_ ?_)).1 ?_
-    rw [Functor.map_comp, ← LaxMonoidalFunctor.μ_natural_left'_assoc, w, Functor.map_comp,
-      reassoc_of% w, braiding_naturality_left_assoc, LaxMonoidalFunctor.μ_natural_right']
+    rw [Functor.map_comp, ← LaxMonoidalFunctor.μ_natural_left_assoc, w, Functor.map_comp,
+      reassoc_of% w, braiding_naturality_left_assoc, LaxMonoidalFunctor.μ_natural_right]
   braiding_naturality_right := by
     intros
     apply F.map_injective
     refine (cancel_epi (F.μ ?_ ?_)).1 ?_
-    rw [Functor.map_comp, ← LaxMonoidalFunctor.μ_natural_right'_assoc, w, Functor.map_comp,
-      reassoc_of% w, braiding_naturality_right_assoc, LaxMonoidalFunctor.μ_natural_left']
+    rw [Functor.map_comp, ← LaxMonoidalFunctor.μ_natural_right_assoc, w, Functor.map_comp,
+      reassoc_of% w, braiding_naturality_right_assoc, LaxMonoidalFunctor.μ_natural_left]
   hexagon_forward := by
     intros
     apply F.map_injective
     refine (cancel_epi (F.μ _ _)).1 ?_
     refine (cancel_epi (F.μ _ _ ▷ _)).1 ?_
     rw [Functor.map_comp, Functor.map_comp, Functor.map_comp, Functor.map_comp, ←
-      LaxMonoidalFunctor.μ_natural_left'_assoc, ← comp_whiskerRight_assoc, w,
-      comp_whiskerRight_assoc, LaxMonoidalFunctor.associativity'_assoc,
-      LaxMonoidalFunctor.associativity'_assoc, ← LaxMonoidalFunctor.μ_natural_right', ←
+      LaxMonoidalFunctor.μ_natural_left_assoc, ← comp_whiskerRight_assoc, w,
+      comp_whiskerRight_assoc, LaxMonoidalFunctor.associativity_assoc,
+      LaxMonoidalFunctor.associativity_assoc, ← LaxMonoidalFunctor.μ_natural_right, ←
       MonoidalCategory.whiskerLeft_comp_assoc, w, MonoidalCategory.whiskerLeft_comp_assoc,
       reassoc_of% w, braiding_naturality_right_assoc,
-      LaxMonoidalFunctor.associativity', hexagon_forward_assoc]
+      LaxMonoidalFunctor.associativity, hexagon_forward_assoc]
   hexagon_reverse := by
     intros
     apply F.toFunctor.map_injective
     refine (cancel_epi (F.μ _ _)).1 ?_
     refine (cancel_epi (_ ◁ F.μ _ _)).1 ?_
     rw [Functor.map_comp, Functor.map_comp, Functor.map_comp, Functor.map_comp, ←
-      LaxMonoidalFunctor.μ_natural_right'_assoc, ← MonoidalCategory.whiskerLeft_comp_assoc, w,
-      MonoidalCategory.whiskerLeft_comp_assoc, LaxMonoidalFunctor.associativity_inv'_assoc,
-      LaxMonoidalFunctor.associativity_inv'_assoc, ← LaxMonoidalFunctor.μ_natural_left',
+      LaxMonoidalFunctor.μ_natural_right_assoc, ← MonoidalCategory.whiskerLeft_comp_assoc, w,
+      MonoidalCategory.whiskerLeft_comp_assoc, LaxMonoidalFunctor.associativity_inv_assoc,
+      LaxMonoidalFunctor.associativity_inv_assoc, ← LaxMonoidalFunctor.μ_natural_left,
       ← comp_whiskerRight_assoc, w, comp_whiskerRight_assoc, reassoc_of% w,
-      braiding_naturality_left_assoc, LaxMonoidalFunctor.associativity_inv', hexagon_reverse_assoc]
+      braiding_naturality_left_assoc, LaxMonoidalFunctor.associativity_inv, hexagon_reverse_assoc]
 #align category_theory.braided_category_of_faithful CategoryTheory.braidedCategoryOfFaithful
 
 /-- Pull back a braiding along a fully faithful monoidal functor. -/
@@ -290,7 +290,7 @@ theorem braiding_leftUnitor_aux₂ (X : C) :
     _ = (α_ _ _ _).hom ≫ (_ ◁ (λ_ _).hom) ≫ (β_ _ _).hom ≫ (β_ X _).inv :=
       by (slice_lhs 2 3 => rw [← braiding_naturality_right]); simp only [assoc]
     _ = (α_ _ _ _).hom ≫ (_ ◁ (λ_ _).hom) := by rw [Iso.hom_inv_id, comp_id]
-    _ = (ρ_ X).hom ▷ 𝟙_ C := by rw [triangle']
+    _ = (ρ_ X).hom ▷ 𝟙_ C := by rw [triangle]
 
 #align category_theory.braiding_left_unitor_aux₂ CategoryTheory.braiding_leftUnitor_aux₂
 
@@ -323,7 +323,7 @@ theorem braiding_rightUnitor_aux₂ (X : C) :
     _ = (α_ _ _ _).inv ≫ ((ρ_ _).hom ▷ _) ≫ (β_ _ X).hom ≫ (β_ _ _).inv :=
       by (slice_lhs 2 3 => rw [← braiding_naturality_left]); simp only [assoc]
     _ = (α_ _ _ _).inv ≫ ((ρ_ _).hom ▷ _) := by rw [Iso.hom_inv_id, comp_id]
-    _ = 𝟙_ C ◁ (λ_ X).hom := by rw [triangle_assoc_comp_right']
+    _ = 𝟙_ C ◁ (λ_ X).hom := by rw [triangle_assoc_comp_right]
 
 #align category_theory.braiding_right_unitor_aux₂ CategoryTheory.braiding_rightUnitor_aux₂
 
@@ -552,8 +552,6 @@ theorem tensor_μ_natural {X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C} (f₁ :
   simp only [assoc]
 #align category_theory.tensor_μ_natural CategoryTheory.tensor_μ_natural
 
-attribute [local simp] id_tensorHom tensorHom_id
-
 @[reassoc]
 theorem tensor_μ_natural_left {X₁ X₂ Y₁ Y₂ : C} (f₁: X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (Z₁ Z₂ : C) :
     (f₁ ⊗ f₂) ▷ (Z₁ ⊗ Z₂) ≫ tensor_μ C (Y₁, Y₂) (Z₁, Z₂) =
@@ -737,11 +735,10 @@ monoidal opposite, upgraded to a braided functor. -/
 @[simps!] def mopBraidedFunctor : BraidedFunctor C Cᴹᵒᵖ where
   μ X Y := (β_ (mop X) (mop Y)).hom
   ε := 𝟙 (𝟙_ Cᴹᵒᵖ)
-  -- `id_tensorHom`, `tensorHom_id` should be simp lemmas when #6307 is merged
-  -- we could then make this fully automated if we mark `yang_baxter` as simp
+  -- we could make this fully automated if we mark `← yang_baxter_assoc` as simp
   -- should it be marked as such?
   associativity X Y Z := by
-    simp [id_tensorHom, tensorHom_id, ← yang_baxter_assoc]
+    simp [← yang_baxter_assoc]
   __ := mopFunctor C
 
 /-- The identity functor on `C`, viewed as a functor from the
@@ -750,7 +747,7 @@ monoidal opposite of `C` to `C`, upgraded to a braided functor. -/
   μ X Y := (β_ (unmop X) (unmop Y)).hom
   ε := 𝟙 (𝟙_ C)
   associativity X Y Z := by
-    simp [id_tensorHom, tensorHom_id, ← yang_baxter_assoc]
+    simp [← yang_baxter_assoc]
   __ := unmopFunctor C
 
 end MonoidalOpposite