-- Module: Mathlib.CategoryTheory.Limits.Set
Goal:
J : Type w
inst : Category.{w', w} J
X : Type u
inst_1 : IsFilteredOrEmpty.{w', w} J
F : CategoryTheory.Functor.{w', u, w, u} J (Set X)
hsurj :
  ∀ (x : Cocone.pt (F := F ⋙ functorToTypes) (Functor.mapCocone functorToTypes (colimitCocone F).cocone)),
    ∃ (i : J) (xi : (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj i)),
      x =
        (ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app (Cocone.ι (Functor.mapCocone functorToTypes (colimitCocone F).cocone)) i) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj i)) →
              (fun (X : Type u) ↦ X)
                (((Functor.const J).obj (functorToTypes.mapCocone (colimitCocone F).cocone).pt).obj i))
          xi
hinj :
  ∀ (i j : J) (xi : (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj i))
    (xj : (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj j)),
    Eq (α :=
        (fun (X : Type u) ↦ X)
          (Functor.obj.{w', u, w, u + 1}
            (Functor.obj (Functor.const J)
              (Cocone.pt (F := F ⋙ functorToTypes) (Functor.mapCocone functorToTypes (colimitCocone F).cocone)))
            i))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app (Cocone.ι (Functor.mapCocone functorToTypes (colimitCocone F).cocone)) i) :
              (a : (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj i)) →
                (fun (X : Type u) ↦ X)
                  (((Functor.const J).obj (functorToTypes.mapCocone (colimitCocone F).cocone).pt).obj i))
            xi :
          (fun (X : Type u) ↦ X)
            (Functor.obj.{w', u, w, u + 1}
              (Functor.obj (Functor.const J)
                (Cocone.pt (F := F ⋙ functorToTypes) (Functor.mapCocone functorToTypes (colimitCocone F).cocone)))
              i))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app (Cocone.ι (Functor.mapCocone functorToTypes (colimitCocone F).cocone)) j) :
              (a : (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj j)) →
                (fun (X : Type u) ↦ X)
                  (((Functor.const J).obj (functorToTypes.mapCocone (colimitCocone F).cocone).pt).obj j))
            xj :
          (fun (X : Type u) ↦ X)
            (Functor.obj.{w', u, w, u + 1}
              (Functor.obj (Functor.const J)
                (Cocone.pt (F := F ⋙ functorToTypes) (Functor.mapCocone functorToTypes (colimitCocone F).cocone)))
              j)) →
      ∃ (k : J) (f : i ⟶ k) (g : j ⟶ k),
        Eq (α := (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ functorToTypes).map f) :
                (a : (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj i)) →
                  (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj k))
              xi :
            (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ functorToTypes).map g) :
                (a : (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj j)) →
                  (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj k))
              xj :
            (fun (X : Type u) ↦ X) ((F ⋙ functorToTypes).obj k))
⊢ IsColimit (F := F ⋙ functorToTypes) (Functor.mapCocone functorToTypes (colimitCocone F).cocone)

Tactic:
apply Types.FilteredColimit.isColimitOf

Premises used: CategoryTheory.Limits.Types.FilteredColimit.isColimitOf