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
t : ColimitCocone F
j : J
⊢ t.cocone.ι.app j ≫ IsColimit.desc t.isColimit (cocone F) = ι F j
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
t : ColimitCocone F
j : J
⊢ t.cocone.ι.app j ≫ (isoColimitCocone t).inv = ι F j
dsimp [colimit.isoColimitCocone, IsColimit.coconePointUniqueUpToIso]
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
t : ColimitCocone F
j : J
⊢ t.cocone.ι.app j ≫ IsColimit.desc t.isColimit (cocone F) = ι F j
aesop_cat