∀ {J : Type u_5} {K : Type u_6} [inst : CategoryTheory.Category.{u_3, u_5} J]
  [inst_1 : CategoryTheory.Category.{u_4, u_6} K] {C : Type u_2} [inst_2 : CategoryTheory.Category.{u_1, u_2} C]
  (G : CategoryTheory.Functor (J × K) C) [inst_3 : CategoryTheory.Limits.HasColimitsOfShape K C]
  [inst_4 : CategoryTheory.Limits.HasColimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim)]
  (c' : CategoryTheory.Limits.Cocone G) (f : J × K),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.coconeOfHasColimitCurryCompColim G).ι.app f)
      (CategoryTheory.Limits.colimit.desc ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim)
        (CategoryTheory.Limits.coconeOfCoconeCurry G
          (fun j => CategoryTheory.Limits.colimit.isColimit ((CategoryTheory.Functor.curry.obj G).obj j)) c')) =
    c'.ι.app f