case w
J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u
inst✝¹ : Category C
F : J ⥤ C
inst✝ : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
c : Cocone G
⊢ ∀ (j : J), ι F j ≫ colimMap α ≫ desc G c = ι F j ≫ desc F ((Cocones.precompose α).obj c)
J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u
inst✝¹ : Category C
F : J ⥤ C
inst✝ : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
c : Cocone G
⊢ colimMap α ≫ desc G c = desc F ((Cocones.precompose α).obj c)
apply Limits.colimit.hom_ext
case w
J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u
inst✝¹ : Category C
F : J ⥤ C
inst✝ : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
c : Cocone G
j : J
⊢ ι F j ≫ colimMap α ≫ desc G c = ι F j ≫ desc F ((Cocones.precompose α).obj c)
case w
J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u
inst✝¹ : Category C
F : J ⥤ C
inst✝ : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
c : Cocone G
⊢ ∀ (j : J), ι F j ≫ colimMap α ≫ desc G c = ι F j ≫ desc F ((Cocones.precompose α).obj c)
intro j
no goals
case w
J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u
inst✝¹ : Category C
F : J ⥤ C
inst✝ : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
c : Cocone G
j : J
⊢ ι F j ≫ colimMap α ≫ desc G c = ι F j ≫ desc F ((Cocones.precompose α).obj c)
simp [← assoc, colimit.ι_map, assoc, colimit.ι_desc, colimit.ι_desc]