-- Module: Mathlib.CategoryTheory.Types.Monomorphisms
Goal:
J : Type u'
x : Category.{v', u'} J
h_1 : IsFiltered.{v', u'} J
F₁ F₂ : Functor.{v', u, u', u + 1} J (Type u)
c₁ : Cocone F₁
c₂ : Cocone F₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : F₁ ⟶ F₂
φ : c₁.pt ⟶ c₂.pt
hf :
  ∀ (j : J),
    Function.Injective (α := F₁.obj j) (β := F₂.obj j)
      (⇑(hom (FC := TypeCat.Fun) (f.app j)) : (a : F₁.obj j) → F₂.obj j)
hφ :
  ∀ (j : J) (x_1 : ToType (FC := TypeCat.Fun) (F₁.obj j)),
    Eq (α := c₂.pt)
      ((hom (FC := TypeCat.Fun) φ : (a : c₁.pt) → c₂.pt)
          ((hom (FC := TypeCat.Fun) (c₁.ι.app j) : (a : F₁.obj j) → c₁.pt) x_1 : c₁.pt) :
        c₂.pt)
      ((hom (FC := TypeCat.Fun) (c₂.ι.app j) : (a : F₂.obj j) → c₂.pt)
          ((hom (FC := TypeCat.Fun) (f.app j) : (a : F₁.obj j) → F₂.obj j) x_1 : F₂.obj j) :
        c₂.pt)
y₁ : c₁.pt
j : J
x₁ : F₁.obj j
h :
  Eq (α := c₂.pt)
    ((hom (FC := TypeCat.Fun) φ : (a : c₁.pt) → c₂.pt)
        ((hom (FC := TypeCat.Fun) (c₁.ι.app j) :
              (a : (fun (X : Type u) ↦ X) (F₁.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj c₁.pt).obj j))
            x₁ :
          (fun (X : Type u) ↦ X) (Functor.obj.{v', u, u', u + 1} (Functor.obj (Functor.const J) c₁.pt) j)) :
      c₂.pt)
    ((hom (FC := TypeCat.Fun) φ : (a : c₁.pt) → c₂.pt) y₁ : c₂.pt)
obtain :
  ∀ (l : J) (y₁ : F₁.obj l)
    (h :
      Eq (α := c₂.pt)
        ((hom (FC := TypeCat.Fun) φ : (a : c₁.pt) → c₂.pt)
            ((hom (FC := TypeCat.Fun) (c₁.ι.app j) :
                  (a : (fun (X : Type u) ↦ X) (F₁.obj j)) →
                    (fun (X : Type u) ↦ X) (((Functor.const J).obj c₁.pt).obj j))
                x₁ :
              (fun (X : Type u) ↦ X) (Functor.obj.{v', u, u', u + 1} (Functor.obj (Functor.const J) c₁.pt) j)) :
          c₂.pt)
        ((hom (FC := TypeCat.Fun) φ : (a : c₁.pt) → c₂.pt)
            ((hom (FC := TypeCat.Fun) (c₁.ι.app l) :
                  (a : (fun (X : Type u) ↦ X) (F₁.obj l)) →
                    (fun (X : Type u) ↦ X) (((Functor.const J).obj c₁.pt).obj l))
                y₁ :
              (fun (X : Type u) ↦ X) (Functor.obj.{v', u, u', u + 1} (Functor.obj (Functor.const J) c₁.pt) l)) :
          c₂.pt)),
    ∃ (j_1 : J) (x₁' : F₁.obj j_1) (y₁' : F₁.obj j_1),
      Eq (α := c₁.pt)
          ((hom (FC := TypeCat.Fun) (c₁.ι.app j) :
                (a : (fun (X : Type u) ↦ X) (F₁.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj c₁.pt).obj j))
              x₁ :
            (fun (X : Type u) ↦ X) (Functor.obj.{v', u, u', u + 1} (Functor.obj (Functor.const J) c₁.pt) j))
          ((hom (FC := TypeCat.Fun) (c₁.ι.app j_1) :
                (a : (fun (X : Type u) ↦ X) (F₁.obj j_1)) →
                  (fun (X : Type u) ↦ X) (((Functor.const J).obj c₁.pt).obj j_1))
              x₁' :
            (fun (X : Type u) ↦ X) (Functor.obj.{v', u, u', u + 1} (Functor.obj (Functor.const J) c₁.pt) j_1)) ∧
        Eq (α := c₁.pt)
          ((hom (FC := TypeCat.Fun) (c₁.ι.app l) :
                (a : (fun (X : Type u) ↦ X) (F₁.obj l)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj c₁.pt).obj l))
              y₁ :
            (fun (X : Type u) ↦ X) (Functor.obj.{v', u, u', u + 1} (Functor.obj (Functor.const J) c₁.pt) l))
          ((hom (FC := TypeCat.Fun) (c₁.ι.app j_1) :
                (a : (fun (X : Type u) ↦ X) (F₁.obj j_1)) →
                  (fun (X : Type u) ↦ X) (((Functor.const J).obj c₁.pt).obj j_1))
              y₁' :
            (fun (X : Type u) ↦ X) (Functor.obj.{v', u, u', u + 1} (Functor.obj (Functor.const J) c₁.pt) j_1))
⊢ ∃ (j_1 : J) (x₁' : F₁.obj j_1) (y₁' : F₁.obj j_1),
    Eq (α := c₁.pt)
        ((hom (FC := TypeCat.Fun) (c₁.ι.app j) :
              (a : (fun (X : Type u) ↦ X) (F₁.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj c₁.pt).obj j))
            x₁ :
          (fun (X : Type u) ↦ X) (Functor.obj.{v', u, u', u + 1} (Functor.obj (Functor.const J) c₁.pt) j))
        ((hom (FC := TypeCat.Fun) (c₁.ι.app j_1) :
              (a : (fun (X : Type u) ↦ X) (F₁.obj j_1)) →
                (fun (X : Type u) ↦ X) (((Functor.const J).obj c₁.pt).obj j_1))
            x₁' :
          (fun (X : Type u) ↦ X) (Functor.obj.{v', u, u', u + 1} (Functor.obj (Functor.const J) c₁.pt) j_1)) ∧
      y₁ =
        (hom (FC := TypeCat.Fun) (c₁.ι.app j_1) :
            (a : (fun (X : Type u) ↦ X) (F₁.obj j_1)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj c₁.pt).obj j_1))
          y₁'

Tactic:
obtain ⟨l, y₁, rfl⟩ := Types.jointly_surjective_of_isColimit hc₁ y₁

Premises used: CategoryTheory.Limits.Types.jointly_surjective_of_isColimit, rfl