case w
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
c : Cocone F
X : C
f : c.pt ⟶ X
j✝ : J
⊢ ι F j✝ ≫ desc F (Cocone.extend c f) = ι F j✝ ≫ desc F c ≫ f
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
c : Cocone F
X : C
f : c.pt ⟶ X
⊢ desc F (Cocone.extend c f) = desc F c ≫ f
ext1
case w
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
c : Cocone F
X : C
f : c.pt ⟶ X
j✝ : J
⊢ ι F j✝ ≫ desc F (Cocone.extend c f) = (ι F j✝ ≫ desc F c) ≫ f
case w
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
c : Cocone F
X : C
f : c.pt ⟶ X
j✝ : J
⊢ ι F j✝ ≫ desc F (Cocone.extend c f) = ι F j✝ ≫ desc F c ≫ f
rw [← Category.assoc]
no goals
case w
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
c : Cocone F
X : C
f : c.pt ⟶ X
j✝ : J
⊢ ι F j✝ ≫ desc F (Cocone.extend c f) = (ι F j✝ ≫ desc F c) ≫ f
simp