no goals
J : Type u₁
inst✝⁴ : Category J
K : Type u₂
inst✝³ : Category K
C : Type u
inst✝² : Category C
F✝ F : J ⥤ C
inst✝¹ : HasColimit F
G : K ⥤ C
inst✝ : HasColimit G
e : J ≌ K
w : e.functor ⋙ G ≅ F
k : K
⊢ colimit.ι G k ≫ (isoOfEquivalence e w).inv =
    G.map ((Equivalence.counitInv e).app k) ≫ w.hom.app (e.inverse.obj k) ≫ colimit.ι F (e.inverse.obj k)
simp [HasColimit.isoOfEquivalence, IsColimit.coconePointsIsoOfEquivalence_inv]