-- 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)
inst_1 : IsFilteredOrEmpty.{w, v} J
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) (x y : (fun (X : Type u) ↦ X) (F.obj i)),
    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))
            x :
          (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))
            y :
          (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) i)) →
      ∃ (k : J) (f : i ⟶ 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))
              x :
            (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))
              y :
            (fun (X : Type u) ↦ X) (F.obj k))
i j : J
xi : (fun (X : Type u) ↦ X) (F.obj i)
xj : (fun (X : Type u) ↦ X) (F.obj j)
h :
  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
g : IsFiltered.max.{w, v} i j ⟶ k
hg :
  Eq (α := (fun (X : Type u) ↦ X) (F.obj k))
    ((hom (FC := TypeCat.Fun) (F.map g) :
          (a : (fun (X : Type u) ↦ X) (F.obj (IsFiltered.max i j))) → (fun (X : Type u) ↦ X) (F.obj k))
        ((hom (FC := TypeCat.Fun) (F.map (IsFiltered.leftToMax i j)) :
              (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj (IsFiltered.max i j)))
            xi :
          (fun (X : Type u) ↦ X) (F.obj (IsFiltered.max.{w, v} i j))) :
      (fun (X : Type u) ↦ X) (F.obj k))
    ((hom (FC := TypeCat.Fun) (F.map g) :
          (a : (fun (X : Type u) ↦ X) (F.obj (IsFiltered.max i j))) → (fun (X : Type u) ↦ X) (F.obj k))
        ((hom (FC := TypeCat.Fun) (F.map (IsFiltered.rightToMax i j)) :
              (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj (IsFiltered.max i j)))
            xj :
          (fun (X : Type u) ↦ X) (F.obj (IsFiltered.max.{w, v} i j))) :
      (fun (X : Type u) ↦ X) (F.obj k))
⊢ ∃ (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))

Tactic:
exact ⟨k, IsFiltered.leftToMax i j ≫ g, IsFiltered.rightToMax i j ≫ g, by simpa using hg⟩