∀ {C : Type u_6} [inst : CategoryTheory.Category.{u_5, u_6} C] {D : Type u_4}
  [inst_1 : CategoryTheory.Category.{u_3, u_4} D] {E : Type u_2} [inst_2 : CategoryTheory.Category.{u_1, u_2} E]
  (F : CategoryTheory.Functor (C × D) E) {X Y : C} (f : X ⟶ Y) {Y_1 Y' : D} (g : Y_1 ⟶ Y'),
  CategoryTheory.CategoryStruct.comp
      ({ obj := fun Y => F.obj (X, Y),
            map := fun {X_1 Y} g => F.map (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X) g),
            map_id := ⋯, map_comp := ⋯ }.map
        g)
      (F.map (CategoryTheory.Prod.mkHom f (CategoryTheory.CategoryStruct.id Y'))) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Prod.mkHom f (CategoryTheory.CategoryStruct.id Y_1)))
      ({ obj := fun Y_2 => F.obj (Y, Y_2),
            map := fun {X Y_2} g => F.map (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id Y) g),
            map_id := ⋯, map_comp := ⋯ }.map
        g)