case intro
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
a : (j : J) × (forget C).obj (F.obj j)
⊢ ∃ j y, (forget C).map (D.ι.app j) y = (fun a => (forget C).map (D.ι.app a.fst) a.snd) a
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
x : (forget C).obj D.pt
⊢ ∃ j y, (forget C).map (D.ι.app j) y = x
obtain ⟨a, rfl⟩ := Concrete.from_union_surjective_of_isColimit F hD x
no goals
case intro
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
a : (j : J) × (forget C).obj (F.obj j)
⊢ ∃ j y, (forget C).map (D.ι.app j) y = (fun a => (forget C).map (D.ι.app a.fst) a.snd) a
exact ⟨a.1, a.2, rfl⟩