∀ (C : Type u_2) [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {a : CategoryTheory.MonoidalSingleObj C} {b : CategoryTheory.MonoidalSingleObj C}
  {c d : CategoryTheory.MonoidalSingleObj C} (f g : C) {h h' : C} (η : h ⟶ h'),
  CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj f g) η =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator f g h).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft f (CategoryTheory.MonoidalCategoryStruct.whiskerLeft g η))
        (CategoryTheory.MonoidalCategoryStruct.associator f g h').inv)