no goals
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
c₁ c₂ : Cocone F
t : IsColimit c₁
⊢ ∀ (j : J), (G.mapCocone c₁).ι.app j ≫ G.map (IsColimit.desc t c₂) = (G.mapCocone c₂).ι.app j
simp [← G.map_comp]