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

Premises used: TypeCat.Fun.coe_mk, CategoryTheory.Category.comp_id, TypeCat.Fun.toFun_apply, CategoryTheory.comp_apply, CategoryTheory.Functor.const_obj_obj, CategoryTheory.ConcreteCategory.hom_ofHom, CategoryTheory.Functor.const_obj_map