-- 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
j : J
x y : (↑(F.1 j) : Type u)
k : J
x' y' : (↑(F.obj k) : Type u)
hx :
  Eq (α := (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) k))
    ((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))
        x' :
      (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) k))
    (({
            toFun :=
              (⇑(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)),
            inj' := ⋯ } :
          (a : (↑(F.1 j) : Type u)) → CoconePt hc)
        x :
      CoconePt hc)
hy :
  Eq (α := (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) k))
    ((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' :
      (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) k))
    (({
            toFun :=
              (⇑(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)),
            inj' := ⋯ } :
          (a : (↑(F.1 j) : Type u)) → CoconePt hc)
        y :
      CoconePt hc)
h : x' ≤ y'
obtain :
  ∀ (l₁ : J) (a₁ : k ⟶ l₁) (b₁ : j ⟶ l₁)
    (hl₁ :
      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 k)) →
                (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj l₁))
            x' :
          (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 j)) →
                (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj l₁))
            x :
          (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₁))),
    x ≤ y
⊢ x ≤ y

Tactic:
obtain ⟨l₁, a₁, b₁, hl₁⟩ := (Types.FilteredColimit.isColimit_eq_iff _ hc).1 hx

Premises used: CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff, Iff.mp