∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C}
  [inst_3 : CategoryTheory.Limits.HasColimit F] {G : CategoryTheory.Functor K C}
  [inst_4 : CategoryTheory.Limits.HasColimit G] (e : J ≌ K) (w : e.functor.comp G ≅ F) (k : K),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι G k)
      (CategoryTheory.Limits.HasColimit.isoOfEquivalence e w).inv =
    CategoryTheory.CategoryStruct.comp (G.map (e.counitInv.app k))
      (CategoryTheory.CategoryStruct.comp (w.hom.app (e.inverse.obj k))
        (CategoryTheory.Limits.colimit.ι F (e.inverse.obj k)))