∀ {A : Type u_2} [inst : CategoryTheory.Category.{u_4, u_2} A] {A' : Type u_5}
  [inst_1 : CategoryTheory.Category.{u_6, u_5} A'] {B : Type u_1} [inst_2 : CategoryTheory.Category.{u_3, u_1} B]
  {X Y : CategoryTheory.Functor A B × CategoryTheory.Functor A' B} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.Sum.functorEquiv A A' B).inverse.comp
            ((CategoryTheory.Functor.whiskeringLeft A (A ⊕ A') B).obj (CategoryTheory.Sum.inl_ A A'))).map
        f)
      ((fun x => x.1.inlCompSum' x.2) Y).hom =
    CategoryTheory.CategoryStruct.comp ((fun x => x.1.inlCompSum' x.2) X).hom
      ((CategoryTheory.Prod.fst (CategoryTheory.Functor A B) (CategoryTheory.Functor A' B)).map f)