-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Filtered (goal)
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
⊢ 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
have 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
Tactic: obtain ⟨k, l, g, eq⟩ := hinj _ _ _ _ (hf (t.ι.app j y))