∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [inst_3 : CategoryTheory.Limits.HasColimitsOfShape J C]
  (F : CategoryTheory.Functor K (CategoryTheory.Functor J C)) (X : K),
  (CategoryTheory.Limits.colimitFlipIsoCompColim F).inv.app X =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.HasColimit.isoOfNatIso (CategoryTheory.flipCompEvaluation F X)).inv
      (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation F.flip X).inv