feat(CategoryTheory/Monoidal): add lemmas for whiskering operators

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

@@ -230,6 +230,18 @@ theorem hom_apply {K L M N : ModuleCat.{u} R} (f : K ⟶ L) (g : M ⟶ N) (k : K
   rfl
 #align Module.monoidal_category.hom_apply ModuleCat.MonoidalCategory.hom_apply
 
+@[simp]
+theorem whiskerLeft_apply (L : ModuleCat.{u} R) {M N : ModuleCat.{u} R} (f : M ⟶ N)
+    (l : L) (m : M) :
+      (L ◁ f) (l ⊗ₜ m) = l ⊗ₜ f m :=
+  rfl
+
+@[simp]
+theorem whiskerRight_apply {L M : ModuleCat.{u} R} (f : L ⟶ M) (N : ModuleCat.{u} R)
+    (l : L) (n : N) :
+      (f ▷ N) (l ⊗ₜ n) = f l ⊗ₜ n :=
+  rfl
+
 @[simp]
 theorem leftUnitor_hom_apply {M : ModuleCat.{u} R} (r : R) (m : M) :
     ((λ_ M).hom : 𝟙_ (ModuleCat R) ⊗ M ⟶ M) (r ⊗ₜ[R] m) = r • m :=

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

@@ -39,6 +39,18 @@ theorem braiding_naturality {X₁ X₂ Y₁ Y₂ : ModuleCat.{u} R} (f : X₁ 
 set_option linter.uppercaseLean3 false in
 #align Module.monoidal_category.braiding_naturality ModuleCat.MonoidalCategory.braiding_naturality
 
+@[simp]
+theorem braiding_naturality_left {X Y : ModuleCat R} (f : X ⟶ Y) (Z : ModuleCat R) :
+    f ▷ Z ≫ (braiding Y Z).hom = (braiding X Z).hom ≫ Z ◁ f := by
+  simp_rw [← id_tensorHom]
+  apply braiding_naturality
+
+@[simp]
+theorem braiding_naturality_right (X : ModuleCat R) {Y Z : ModuleCat R} (f : Y ⟶ Z) :
+    X ◁ f ≫ (braiding X Z).hom = (braiding X Y).hom ≫ f ▷ X := by
+  simp_rw [← id_tensorHom]
+  apply braiding_naturality
+
 @[simp]
 theorem hexagon_forward (X Y Z : ModuleCat.{u} R) :
     (α_ X Y Z).hom ≫ (braiding X _).hom ≫ (α_ Y Z X).hom =

Mathlib/CategoryTheory/Monoidal/Types/Basic.lean

@@ -33,6 +33,16 @@ theorem tensor_apply {W X Y Z : Type u} (f : W ⟶ X) (g : Y ⟶ Z) (p : W ⊗ Y
   rfl
 #align category_theory.tensor_apply CategoryTheory.tensor_apply
 
+@[simp]
+theorem whiskerLeft_apply (X : Type u) {Y Z : Type u} (f : Y ⟶ Z) (p : X ⊗ Y) :
+    (X ◁ f) p = (p.1, f p.2) :=
+  rfl
+
+@[simp]
+theorem whiskerRight_apply {Y Z : Type u} (f : Y ⟶ Z) (X : Type u) (p : Y ⊗ X) :
+    (f ▷ X) p = (f p.1, p.2) :=
+  rfl
+
 @[simp]
 theorem leftUnitor_hom_apply {X : Type u} {x : X} {p : PUnit} :
     ((λ_ X).hom : 𝟙_ (Type u) ⊗ X → X) (p, x) = x :=

Mathlib/RepresentationTheory/Action.lean

@@ -504,10 +504,20 @@ set_option linter.uppercaseLean3 false in
 #align Action.tensor_rho Action.tensor_rho
 
 @[simp]
-theorem tensorHom {W X Y Z : Action V G} (f : W ⟶ X) (g : Y ⟶ Z) : (f ⊗ g).hom = f.hom ⊗ g.hom :=
+theorem tensor_hom {W X Y Z : Action V G} (f : W ⟶ X) (g : Y ⟶ Z) : (f ⊗ g).hom = f.hom ⊗ g.hom :=
   rfl
 set_option linter.uppercaseLean3 false in
-#align Action.tensor_hom Action.tensorHom
+#align Action.tensor_hom Action.tensor_hom
+
+@[simp]
+theorem whiskerLeft_hom (X : Action V G) {Y Z : Action V G} (f : Y ⟶ Z) :
+    (X ◁ f).hom = X.V ◁ f.hom :=
+  rfl
+
+@[simp]
+theorem whiskerRight_hom {X Y : Action V G} (f : X ⟶ Y) (Z : Action V G) :
+    (f ▷ Z).hom = f.hom ▷ Z.V :=
+  rfl
 
 -- porting note: removed @[simp] as the simpNF linter complains
 theorem associator_hom_hom {X Y Z : Action V G} :