∀ (J₁ : Type u₁) (J₂ : Type u₂) (C : Type u₃) [inst : CategoryTheory.Category.{v₁, u₁} J₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} J₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  [inst_3 : CategoryTheory.MonoidalCategory C] {X Y : CategoryTheory.Functor J₁ C × CategoryTheory.Functor J₂ C}
  (f : X ⟶ Y) (X_1 : J₁ × J₂),
  ((CategoryTheory.MonoidalCategory.externalProductBifunctor J₁ J₂ C).map f).app X_1 =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (f.1.app X_1.1) (X.2.obj X_1.2))
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (Y.1.obj X_1.1) (f.2.app X_1.2))