∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.CartesianMonoidalCategory C]
  (F₁ : CategoryTheory.Functor J C) {F₂ F₂' : CategoryTheory.Functor J C} (g : F₂ ⟶ F₂') (j : J),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.whiskerLeft F₁ g).app j)
      (CategoryTheory.SemiCartesianMonoidalCategory.snd (F₁.obj j) (F₂'.obj j)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd (F₁.obj j) (F₂.obj j))
      (g.app j)