J : Type u₁
inst✝⁵ : Category J
K : Type u₂
inst✝⁴ : Category K
C : Type u
inst✝³ : Category C
F : J ⥤ C
D : Type u'
inst✝² : Category D
inst✝¹ : HasColimit F
G : C ⥤ D
inst✝ : HasColimit (F ⋙ G)
j : J
⊢ (G.mapCocone (cocone F)).ι.app j = G.map (ι F j)
J : Type u₁
inst✝⁵ : Category J
K : Type u₂
inst✝⁴ : Category K
C : Type u
inst✝³ : Category C
F : J ⥤ C
D : Type u'
inst✝² : Category D
inst✝¹ : HasColimit F
G : C ⥤ D
inst✝ : HasColimit (F ⋙ G)
j : J
⊢ ι (F ⋙ G) j ≫ post F G = G.map (ι F j)
erw [IsColimit.fac]
no goals
J : Type u₁
inst✝⁵ : Category J
K : Type u₂
inst✝⁴ : Category K
C : Type u
inst✝³ : Category C
F : J ⥤ C
D : Type u'
inst✝² : Category D
inst✝¹ : HasColimit F
G : C ⥤ D
inst✝ : HasColimit (F ⋙ G)
j : J
⊢ (G.mapCocone (cocone F)).ι.app j = G.map (ι F j)
rfl