∀ (A : Type u_5) [inst : CategoryTheory.Category.{u_1, u_5} A] (A' : Type u_4)
  [inst_1 : CategoryTheory.Category.{u_2, u_4} A'] (B : Type u_6) [inst_2 : CategoryTheory.Category.{u_3, u_6} B]
  {X Y : CategoryTheory.Functor (A ⊕ A') B} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.id (CategoryTheory.Functor (A ⊕ A') B)).map f)
      ((fun F => F.isoSum) Y).hom =
    CategoryTheory.CategoryStruct.comp ((fun F => F.isoSum) X).hom
      (({ obj := fun F => ((CategoryTheory.Sum.inl_ A A').comp F, (CategoryTheory.Sum.inr_ A A').comp F),
                map := fun {X Y} η =>
                  CategoryTheory.Prod.mkHom ((CategoryTheory.Sum.inl_ A A').whiskerLeft η)
                    ((CategoryTheory.Sum.inr_ A A').whiskerLeft η),
                map_id := ⋯, map_comp := ⋯ }.comp
            { obj := fun F => F.1.sum' F.2, map := fun {X Y} η => CategoryTheory.NatTrans.sum' η.1 η.2, map_id := ⋯,
              map_comp := ⋯ }).map
        f)