∀ {R : Type u_1} {inst : Semiring R} {C : Type u_2} {inst_1 : CategoryTheory.Category.{v_1, u_2} C}
  {inst_2 : CategoryTheory.Preadditive C} {inst_3 : CategoryTheory.Linear R C}
  {inst_4 : CategoryTheory.MonoidalCategory C} {inst_5 : CategoryTheory.MonoidalPreadditive C}
  [self : CategoryTheory.MonoidalLinear R C] (X : C) {Y Z : C} (r : R) (f : Y ⟶ Z),
  CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (r • f) =
    r • CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f