-- Module: Mathlib.CategoryTheory.Limits.Types.Filtered
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
t : Cocone F
hsurj :
  ∀ (x : t.pt),
    ∃ (i : J) (xi : (fun (X : Type u) ↦ X) (F.obj i)),
      x =
        (hom (FC := TypeCat.Fun) (t.ι.app i) :
            (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj i))
          xi
hinj :
  ∀ (i j : J) (xi : (fun (X : Type u) ↦ X) (F.obj i)) (xj : (fun (X : Type u) ↦ X) (F.obj j)),
    Eq (α := (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) i))
        ((hom (FC := TypeCat.Fun) (t.ι.app i) :
              (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj i))
            xi :
          (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) i))
        ((hom (FC := TypeCat.Fun) (t.ι.app j) :
              (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj j))
            xj :
          (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) j)) →
      ∃ (k : J) (f : i ⟶ k) (g : j ⟶ k),
        Eq (α := (fun (X : Type u) ↦ X) (F.obj k))
          ((hom (FC := TypeCat.Fun) (F.map f) :
                (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k))
              xi :
            (fun (X : Type u) ↦ X) (F.obj k))
          ((hom (FC := TypeCat.Fun) (F.map g) :
                (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj k))
              xj :
            (fun (X : Type u) ↦ X) (F.obj k))
α : t.pt → J :=
  fun (x : t.pt) ↦
    ⋯.choose (p := fun (i : J) ↦
      ∃ (xi : (fun (X : Type u) ↦ X) (F.obj i)),
        x =
          (hom (FC := TypeCat.Fun) (t.ι.app i) :
              (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj i))
            xi)
f : (x : t.pt) → F.obj (α x) :=
  fun (x : t.pt) ↦
    ⋯.choose (p :=
      fun
        (xi :
          F.obj
            (⋯.choose (p := fun (i : J) ↦
              ∃ (xi : (fun (X : Type u) ↦ X) (F.obj i)),
                x =
                  (hom (FC := TypeCat.Fun) (t.ι.app i) :
                      (a : (fun (X : Type u) ↦ X) (F.obj i)) →
                        (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj i))
                    xi))) ↦
      x =
        (hom (FC := TypeCat.Fun)
              (t.ι.app
                (⋯.choose (p := fun (i : J) ↦
                  ∃ (xi : (fun (X : Type u) ↦ X) (F.obj i)),
                    x =
                      (hom (FC := TypeCat.Fun) (t.ι.app i) :
                          (a : (fun (X : Type u) ↦ X) (F.obj i)) →
                            (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj i))
                        xi))) :
            (a : (fun (X : Type u) ↦ X) (F.obj ⋯.choose)) →
              (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj ⋯.choose))
          xi)
hf :
  ∀ (x : t.pt),
    x =
      (hom (FC := TypeCat.Fun) (t.ι.app (α x)) :
          (a : (fun (X : Type u) ↦ X) (F.obj (α x))) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj (α x)))
        (f x)
⊢ IsColimit t

Tactic:
exact
    { desc s := ↾fun x => s.ι.app _ (f x)
      fac := fun s j => by
        ext y
        obtain ⟨k, l, g, eq⟩ := hinj _ _ _ _ (hf (t.ι.app j y))
        have h := congr_hom (s.ι.naturality g) (f (t.ι.app j y))
        have h' := congr_hom (s.ι.naturality l) y
        simp only [Functor.const_obj_obj, comp_apply, Functor.const_obj_map, Category.comp_id,
          TypeCat.Fun.toFun_apply, hom_ofHom, TypeCat.Fun.coe_mk] at h h' ⊢
        rw [← h, ← eq, h']
      uniq := fun s m hm => by
        ext x
        dsimp
        nth_rw 1 [hf x]
        simp [← hm, comp_apply] }