chore(CategoryTheory/Monoidal): replace 𝟙 X ⊗ f with X ◁ f (#11223)

Extracted from #6307

Mathlib/Algebra/Category/FGModuleCat/Basic.lean

@@ -269,13 +269,13 @@ theorem FGModuleCatEvaluation_apply (f : FGModuleCatDual K V) (x : V) :
 
 private theorem coevaluation_evaluation :
     letI V' : FGModuleCat K := FGModuleCatDual K V
-    (𝟙 V' ⊗ FGModuleCatCoevaluation K V) ≫ (α_ V' V V').inv ≫ (FGModuleCatEvaluation K V ⊗ 𝟙 V') =
+    V' ◁ FGModuleCatCoevaluation K V ≫ (α_ V' V V').inv ≫ FGModuleCatEvaluation K V ▷ V' =
       (ρ_ V').hom ≫ (λ_ V').inv := by
   apply contractLeft_assoc_coevaluation K V
 
 private theorem evaluation_coevaluation :
-    (FGModuleCatCoevaluation K V ⊗ 𝟙 V) ≫
-        (α_ V (FGModuleCatDual K V) V).hom ≫ (𝟙 V ⊗ FGModuleCatEvaluation K V) =
+    FGModuleCatCoevaluation K V ▷ V ≫
+        (α_ V (FGModuleCatDual K V) V).hom ≫ V ◁ FGModuleCatEvaluation K V =
       (λ_ V).hom ≫ (ρ_ V).inv := by
   apply contractLeft_assoc_coevaluation' K V
 

Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean

@@ -136,9 +136,9 @@ variable (R)
 
 private theorem pentagon_aux (W X Y Z : Type*) [AddCommMonoid W] [AddCommMonoid X]
     [AddCommMonoid Y] [AddCommMonoid Z] [Module R W] [Module R X] [Module R Y] [Module R Z] :
-    ((map (1 : W →ₗ[R] W) (assoc R X Y Z).toLinearMap).comp
+    (((assoc R X Y Z).toLinearMap.lTensor W).comp
             (assoc R W (X ⊗[R] Y) Z).toLinearMap).comp
-        (map ↑(assoc R W X Y) (1 : Z →ₗ[R] Z)) =
+        ((assoc R W X Y).rTensor Z) =
       (assoc R W X (Y ⊗[R] Z)).toLinearMap.comp (assoc R (W ⊗[R] X) Y Z).toLinearMap := by
   apply TensorProduct.ext_fourfold
   intro w x y z
@@ -156,8 +156,8 @@ theorem associator_naturality {X₁ X₂ X₃ Y₁ Y₂ Y₃ : ModuleCat R} (f
 #align Module.monoidal_category.associator_naturality ModuleCat.MonoidalCategory.associator_naturality
 
 theorem pentagon (W X Y Z : ModuleCat R) :
-    tensorHom (associator W X Y).hom (𝟙 Z) ≫
-        (associator W (tensorObj X Y) Z).hom ≫ tensorHom (𝟙 W) (associator X Y Z).hom =
+    whiskerRight (associator W X Y).hom Z ≫
+        (associator W (tensorObj X Y) Z).hom ≫ whiskerLeft W (associator X Y Z).hom =
       (associator (tensorObj W X) Y Z).hom ≫ (associator W X (tensorObj Y Z)).hom := by
   convert pentagon_aux R W X Y Z using 1
 #align Module.monoidal_category.pentagon ModuleCat.MonoidalCategory.pentagon
@@ -288,30 +288,30 @@ instance : MonoidalPreadditive (ModuleCat.{u} R) := by
     simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply]
     rw [LinearMap.zero_apply]
     -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-    erw [MonoidalCategory.hom_apply]
+    erw [MonoidalCategory.whiskerLeft_apply]
     rw [LinearMap.zero_apply, TensorProduct.tmul_zero]
   · dsimp only [autoParam]; intros
     refine' TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => _)
     simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply]
     rw [LinearMap.zero_apply]
     -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-    erw [MonoidalCategory.hom_apply]
+    erw [MonoidalCategory.whiskerRight_apply]
     rw [LinearMap.zero_apply, TensorProduct.zero_tmul]
   · dsimp only [autoParam]; intros
     refine' TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => _)
     simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply]
     rw [LinearMap.add_apply]
     -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-    erw [MonoidalCategory.hom_apply, MonoidalCategory.hom_apply]
-    erw [MonoidalCategory.hom_apply]
+    erw [MonoidalCategory.whiskerLeft_apply, MonoidalCategory.whiskerLeft_apply]
+    erw [MonoidalCategory.whiskerLeft_apply]
     rw [LinearMap.add_apply, TensorProduct.tmul_add]
   · dsimp only [autoParam]; intros
     refine' TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => _)
     simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply]
     rw [LinearMap.add_apply]
     -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-    erw [MonoidalCategory.hom_apply, MonoidalCategory.hom_apply]
-    erw [MonoidalCategory.hom_apply]
+    erw [MonoidalCategory.whiskerRight_apply, MonoidalCategory.whiskerRight_apply]
+    erw [MonoidalCategory.whiskerRight_apply]
     rw [LinearMap.add_apply, TensorProduct.add_tmul]
 
 -- Porting note: simp wasn't firing but rw was, annoying
@@ -322,14 +322,14 @@ instance : MonoidalLinear R (ModuleCat.{u} R) := by
     simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply]
     rw [LinearMap.smul_apply]
     -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-    erw [MonoidalCategory.hom_apply, MonoidalCategory.hom_apply]
+    erw [MonoidalCategory.whiskerLeft_apply, MonoidalCategory.whiskerLeft_apply]
     rw [LinearMap.smul_apply, TensorProduct.tmul_smul]
   · dsimp only [autoParam]; intros
     refine' TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => _)
     simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply]
     rw [LinearMap.smul_apply]
     -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-    erw [MonoidalCategory.hom_apply, MonoidalCategory.hom_apply]
+    erw [MonoidalCategory.whiskerRight_apply, MonoidalCategory.whiskerRight_apply]
     rw [LinearMap.smul_apply, TensorProduct.smul_tmul, TensorProduct.tmul_smul]
 
 end ModuleCat

Mathlib/Algebra/Category/ModuleCat/Monoidal/Symmetric.lean

@@ -54,7 +54,7 @@ theorem braiding_naturality_right (X : ModuleCat R) {Y Z : ModuleCat R} (f : Y 
 @[simp]
 theorem hexagon_forward (X Y Z : ModuleCat.{u} R) :
     (α_ X Y Z).hom ≫ (braiding X _).hom ≫ (α_ Y Z X).hom =
-      ((braiding X Y).hom ⊗ 𝟙 Z) ≫ (α_ Y X Z).hom ≫ (𝟙 Y ⊗ (braiding X Z).hom) := by
+      (braiding X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (braiding X Z).hom := by
   apply TensorProduct.ext_threefold
   intro x y z
   rfl
@@ -64,7 +64,7 @@ set_option linter.uppercaseLean3 false in
 @[simp]
 theorem hexagon_reverse (X Y Z : ModuleCat.{u} R) :
     (α_ X Y Z).inv ≫ (braiding _ Z).hom ≫ (α_ Z X Y).inv =
-      (𝟙 X ⊗ (Y.braiding Z).hom) ≫ (α_ X Z Y).inv ≫ ((X.braiding Z).hom ⊗ 𝟙 Y) := by
+      X ◁ (Y.braiding Z).hom ≫ (α_ X Z Y).inv ≫ (X.braiding Z).hom ▷ Y := by
   apply (cancel_epi (α_ X Y Z).hom).1
   apply TensorProduct.ext_threefold
   intro x y z

Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean

@@ -291,7 +291,6 @@ theorem braiding_leftUnitor_aux₂ (X : C) :
       by (slice_lhs 2 3 => rw [← braiding_naturality_right]); simp only [assoc]
     _ = (α_ _ _ _).hom ≫ (_ ◁ (λ_ _).hom) := by rw [Iso.hom_inv_id, comp_id]
     _ = (ρ_ X).hom ▷ 𝟙_ C := by rw [triangle]
-
 #align category_theory.braiding_left_unitor_aux₂ CategoryTheory.braiding_leftUnitor_aux₂
 
 @[reassoc]
@@ -324,7 +323,6 @@ theorem braiding_rightUnitor_aux₂ (X : C) :
       by (slice_lhs 2 3 => rw [← braiding_naturality_left]); simp only [assoc]
     _ = (α_ _ _ _).inv ≫ ((ρ_ _).hom ▷ _) := by rw [Iso.hom_inv_id, comp_id]
     _ = 𝟙_ C ◁ (λ_ X).hom := by rw [triangle_assoc_comp_right]
-
 #align category_theory.braiding_right_unitor_aux₂ CategoryTheory.braiding_rightUnitor_aux₂
 
 @[reassoc]

Mathlib/CategoryTheory/Monoidal/Preadditive.lean

@@ -202,7 +202,7 @@ theorem leftDistributor_assoc {J : Type} [Fintype J] (X Y : C) (f : J → C) :
   simp_rw [← id_tensorHom]
   simp only [← id_tensor_comp, biproduct.ι_π]
   simp only [id_tensor_comp, tensor_dite, comp_dite]
-  simp [id_tensorHom]
+  simp
 #align category_theory.left_distributor_assoc CategoryTheory.leftDistributor_assoc
 
 /-- The isomorphism showing how tensor product on the right distributes over direct sums. -/

Mathlib/Tactic/CategoryTheory/Coherence.lean

@@ -262,7 +262,8 @@ elab_rules : tactic
       MonoidalCategory.whiskerRight_tensor, MonoidalCategory.whiskerRight_id,
       MonoidalCategory.whiskerLeft_comp, MonoidalCategory.whiskerLeft_id,
       MonoidalCategory.comp_whiskerRight, MonoidalCategory.id_whiskerRight,
-      MonoidalCategory.whisker_assoc];
+      MonoidalCategory.whisker_assoc,
+      MonoidalCategory.id_tensorHom, MonoidalCategory.tensorHom_id];
     -- I'm not sure if `tensorHom` should be expanded.
     try simp only [MonoidalCategory.tensorHom_def]
     ))

Mathlib/Tactic/CategoryTheory/MonoidalComp.lean

@@ -90,22 +90,22 @@ instance refl (X : C) : MonoidalCoherence X X := ⟨𝟙 _⟩
 @[simps]
 instance whiskerLeft (X Y Z : C) [MonoidalCoherence Y Z] :
     MonoidalCoherence (X ⊗ Y) (X ⊗ Z) :=
-  ⟨𝟙 X ⊗ ⊗𝟙⟩
+  ⟨X ◁ ⊗𝟙⟩
 
 @[simps]
 instance whiskerRight (X Y Z : C) [MonoidalCoherence X Y] :
     MonoidalCoherence (X ⊗ Z) (Y ⊗ Z) :=
-  ⟨⊗𝟙 ⊗ 𝟙 Z⟩
+  ⟨⊗𝟙 ▷ Z⟩
 
 @[simps]
 instance tensor_right (X Y : C) [MonoidalCoherence (𝟙_ C) Y] :
     MonoidalCoherence X (X ⊗ Y) :=
-  ⟨(ρ_ X).inv ≫ (𝟙 X ⊗  ⊗𝟙)⟩
+  ⟨(ρ_ X).inv ≫ X ◁  ⊗𝟙⟩
 
 @[simps]
 instance tensor_right' (X Y : C) [MonoidalCoherence Y (𝟙_ C)] :
     MonoidalCoherence (X ⊗ Y) X :=
-  ⟨(𝟙 X ⊗ ⊗𝟙) ≫ (ρ_ X).hom⟩
+  ⟨X ◁ ⊗𝟙 ≫ (ρ_ X).hom⟩
 
 @[simps]
 instance left (X Y : C) [MonoidalCoherence X Y] :