∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c)
  (d : CategoryTheory.Limits.Cocone G) (α : F ⟶ G) (j : J) {Z : C} (h : d.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (c.ι.app j) (CategoryTheory.CategoryStruct.comp (hc.map d α) h) =
    CategoryTheory.CategoryStruct.comp (α.app j) (CategoryTheory.CategoryStruct.comp (d.ι.app j) h)