-- Module: Mathlib.Order.Category.PartOrdEmb
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsFiltered J
F : J ⥤ PartOrdEmb
c :
  Cocone (F ⋙ forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier))
hc : IsColimit c
x y z : CoconePt hc
j : J
x₁ y₁ : (↑(F.obj j) : Type u)
hx₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j) :
        (a : (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj j)) →
          (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj j))
      x₁ =
    x
hy₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j) :
        (a : (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj j)) →
          (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj j))
      y₁ =
    y
hxy : x₁ ≤ y₁
k : J
y₂ z₁ : (↑(F.obj k) : Type u)
hy₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app k) :
        (a : (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj k)) →
          (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj k))
      y₂ =
    y
hz₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app k) :
        (a : (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj k)) →
          (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj k))
      z₁ =
    z
hyz : y₂ ≤ z₁
l : J
a : j ⟶ l
b : k ⟶ l
h :
  Eq (α :=
    (fun (X : Type u) ↦ X)
      ((F ⋙
            forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
              carrier)).obj
        l))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((F ⋙
                  forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                    carrier)).map
              a) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj j)) →
            (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj l))
        y₁ :
      (fun (X : Type u) ↦ X)
        ((F ⋙
              forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                carrier)).obj
          l))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((F ⋙
                  forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                    carrier)).map
              b) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj k)) →
            (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj l))
        y₂ :
      (fun (X : Type u) ↦ X)
        ((F ⋙
              forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                carrier)).obj
          l))
⊢ ∃ (j : J) (x' : (↑(F.obj j) : Type u)) (y' : (↑(F.obj j) : Type u)) (_ :
    (ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj j)) →
            (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj j))
        x' =
      x)
    (_ :
    (ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj j)) →
            (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj j))
        y' =
      z),
    x' ≤ y'

Tactic:
⟨l, F.map a x₁, F.map b z₁,
      (ConcreteCategory.congr_hom (c.w a) x₁).trans hx₁,
      (ConcreteCategory.congr_hom (c.w b) z₁).trans hz₁,
      ((F.map a).hom.monotone hxy).trans
        (le_of_eq_of_le h ((F.map b).hom.monotone hyz))⟩

Premises used: OrderEmbedding.monotone, CategoryTheory.ConcreteCategory.hom, PartOrdEmb.Hom.hom, CategoryTheory.Functor.map, Exists.intro, le_of_eq_of_le, LE.le.trans, DFunLike.coe