-- 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)
s : Cocone F
j : J
y : F.obj j
h :
  ∀ (k : J) (l : j ⟶ k)
    (g :
      α
          ((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))
            y) ⟶
        k)
    (eq :
      Eq (α := (fun (X : Type u) ↦ X) (F.obj k))
        ((hom (FC := TypeCat.Fun) (F.map l) : (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj k))
            y :
          (fun (X : Type u) ↦ X) (F.obj k))
        ((hom (FC := TypeCat.Fun) (F.map g) :
              (a :
                  (fun (X : Type u) ↦ X)
                    (F.obj
                      (α
                        ((hom (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))
                          y)))) →
                (fun (X : Type u) ↦ X) (F.obj k))
            (f
              ((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))
                y)) :
          (fun (X : Type u) ↦ X) (F.obj k))),
    TypeCat.Fun.toFun
        (hom (FC := TypeCat.Fun)
          (t.ι.app j ≫
            ↾fun (x : t.pt) ↦
              (hom (FC := TypeCat.Fun) (s.ι.app (α x)) :
                  (a : (fun (X : Type u) ↦ X) (F.obj (α x))) →
                    (fun (X : Type u) ↦ X) (((Functor.const J).obj s.pt).obj (α x)))
                (f x)))
        y =
      (hom (FC := TypeCat.Fun) (s.ι.app j)).toFun y
⊢ TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (t.ι.app j ≫
          ↾fun (x : t.pt) ↦
            (hom (FC := TypeCat.Fun) (s.ι.app (α x)) :
                (a : (fun (X : Type u) ↦ X) (F.obj (α x))) →
                  (fun (X : Type u) ↦ X) (((Functor.const J).obj s.pt).obj (α x)))
              (f x)))
      y =
    (hom (FC := TypeCat.Fun) (s.ι.app j)).toFun y

Tactic:
obtain ⟨k, l, g, eq⟩ := hinj _ _ _ _ (hf (t.ι.app j y))

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.Cocone.ι, DFunLike.coe, CategoryTheory.NatTrans.app