-- 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
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))
⊢ Eq (α := Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) s.pt) k)
    ((hom (FC := TypeCat.Fun) (F.map g ≫ s.ι.app k) :
          (a :
              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))) →
            ((Functor.const J).obj s.pt).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)) :
      Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) s.pt) k)
    ((hom (FC := TypeCat.Fun)
            (s.ι.app
                (α
                  ((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)) ≫
              Functor.map (Functor.obj (Functor.const J) s.pt) g) :
          (a :
              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))) →
            ((Functor.const J).obj s.pt).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)) :
      Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) s.pt) k)

Tactic:
have h := congr_hom (s.ι.naturality g) (f (t.ι.app j y))