-- Mathlib/CategoryTheory/Limits/ConcreteCategory/Basic.lean
theorem from_union_surjective_of_isColimit {D : Cocone F} (hD : IsColimit D) :
    let ff : (Σj : J, ToType (F.obj j)) → ToType D.pt := fun a => D.ι.app a.1 a.2
    Function.Surjective ff

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type t
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
inst✝¹ : Category.{r, w} J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
ff : (j : J) × ToType (F.obj j) → ToType D.pt := fun a => (ConcreteCategory.hom (D.ι.app a.fst)) a.snd
x : ToType D.pt
⊢ ∃ a, ff a = x

Tactic:
let E : Cocone (F ⋙ forget C) := (forget C).mapCocone D

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type t
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
inst✝¹ : Category.{r, w} J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
ff : (j : J) × ToType (F.obj j) → ToType D.pt := fun a => (ConcreteCategory.hom (D.ι.app a.fst)) a.snd
x : ToType D.pt
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
⊢ ∃ a, ff a = x

Proof state:
case intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type t
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
inst✝¹ : Category.{r, w} J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
ff : (j : J) × ToType (F.obj j) → ToType D.pt := fun a => (ConcreteCategory.hom (D.ι.app a.fst)) a.snd
x : ToType D.pt
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
j : J
y : (F ⋙ forget C).obj j
hy : E.ι.app j y = x
⊢ ∃ a, ff a = x

Tactic:
exact ⟨⟨j, y⟩, hy⟩

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type t
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
inst✝¹ : Category.{r, w} J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
ff : (j : J) × ToType (F.obj j) → ToType D.pt := fun a => (ConcreteCategory.hom (D.ι.app a.fst)) a.snd
x : ToType D.pt
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
⊢ ∃ a, ff a = x

Tactic:
obtain ⟨j, y, hy⟩ := Types.jointly_surjective_of_isColimit hE x

Result:
case intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type t
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
inst✝¹ : Category.{r, w} J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
ff : (j : J) × ToType (F.obj j) → ToType D.pt := fun a => (ConcreteCategory.hom (D.ι.app a.fst)) a.snd
x : ToType D.pt
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
j : J
y : (F ⋙ forget C).obj j
hy : E.ι.app j y = x
⊢ ∃ a, ff a = x

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type t
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
inst✝¹ : Category.{r, w} J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
⊢ let ff := fun a => (ConcreteCategory.hom (D.ι.app a.fst)) a.snd;
  Function.Surjective ff

Tactic:
intro ff x

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type t
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
inst✝¹ : Category.{r, w} J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
ff : (j : J) × ToType (F.obj j) → ToType D.pt := fun a => (ConcreteCategory.hom (D.ι.app a.fst)) a.snd
x : ToType D.pt
⊢ ∃ a, ff a = x

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type t
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
inst✝¹ : Category.{r, w} J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
ff : (j : J) × ToType (F.obj j) → ToType D.pt := fun a => (ConcreteCategory.hom (D.ι.app a.fst)) a.snd
x : ToType D.pt
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
⊢ ∃ a, ff a = x

Tactic:
let hE : IsColimit E := isColimitOfPreserves (forget C) hD

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type t
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
inst✝¹ : Category.{r, w} J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
ff : (j : J) × ToType (F.obj j) → ToType D.pt := fun a => (ConcreteCategory.hom (D.ι.app a.fst)) a.snd
x : ToType D.pt
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
⊢ ∃ a, ff a = x