∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor J C) {D : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} D]
  [inst_3 : CategoryTheory.Limits.HasColimit F] (G : CategoryTheory.Functor C D)
  [inst_4 : CategoryTheory.Limits.HasColimit (F.comp G)] {E : Type u''} [inst_5 : CategoryTheory.Category.{v'', u''} E]
  (H : CategoryTheory.Functor D E) [h : CategoryTheory.Limits.HasColimit ((F.comp G).comp H)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.post (F.comp G) H)
      (H.map (CategoryTheory.Limits.colimit.post F G)) =
    CategoryTheory.Limits.colimit.post F (G.comp H)