case w
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
J : Type w
inst✝³ : Category J
F : J ⥤ C
inst✝² : PreservesColimit F G
inst✝¹ : HasColimit F
inst✝ : HasColimit (F ⋙ G)
t : Cocone F
j✝ : J
⊢ colimit.ι (F ⋙ G) j✝ ≫ (preservesColimitIso G F).inv ≫ G.map (colimit.desc F t) =
    colimit.ι (F ⋙ G) j✝ ≫ colimit.desc (F ⋙ G) (G.mapCocone t)
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
J : Type w
inst✝³ : Category J
F : J ⥤ C
inst✝² : PreservesColimit F G
inst✝¹ : HasColimit F
inst✝ : HasColimit (F ⋙ G)
t : Cocone F
⊢ (preservesColimitIso G F).inv ≫ G.map (colimit.desc F t) = colimit.desc (F ⋙ G) (G.mapCocone t)
ext
no goals
case w
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
J : Type w
inst✝³ : Category J
F : J ⥤ C
inst✝² : PreservesColimit F G
inst✝¹ : HasColimit F
inst✝ : HasColimit (F ⋙ G)
t : Cocone F
j✝ : J
⊢ colimit.ι (F ⋙ G) j✝ ≫ (preservesColimitIso G F).inv ≫ G.map (colimit.desc F t) =
    colimit.ι (F ⋙ G) j✝ ≫ colimit.desc (F ⋙ G) (G.mapCocone t)
simp [← G.map_comp]