-- 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
s : Cocone F
x y : CoconePt hc
obtain :
  ∀ (j : J)
    (x' y' :
      (F ⋙
            forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
              carrier)).obj
        j),
    LE.le (α := (↑s.pt : Type u))
        (({
                toFun :=
                  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
                        (hc.desc
                          (Functor.mapCocone
                            (forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u))
                              (CC := carrier))
                            s))) :
                    (a : (fun (X : Type u) ↦ X) c.pt) → (fun (X : Type u) ↦ X) ((forget PartOrdEmb).mapCocone s).pt),
                inj' := ⋯ } :
              (a : CoconePt hc) → (↑s.pt : 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' :
              (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) j)) :
          (↑s.pt : Type u))
        (({
                toFun :=
                  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
                        (hc.desc
                          (Functor.mapCocone
                            (forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u))
                              (CC := carrier))
                            s))) :
                    (a : (fun (X : Type u) ↦ X) c.pt) → (fun (X : Type u) ↦ X) ((forget PartOrdEmb).mapCocone s).pt),
                inj' := ⋯ } :
              (a : CoconePt hc) → (↑s.pt : 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))
                y' :
              (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) j)) :
          (↑s.pt : Type u)) ↔
      LE.le (α := CoconePt hc)
        ((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' :
          (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) j))
        ((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' :
          (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) j))
⊢ LE.le (α := (↑s.pt : Type u))
      (({
              toFun :=
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
                      (hc.desc
                        (Functor.mapCocone
                          (forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u))
                            (CC := carrier))
                          s))) :
                  (a : (fun (X : Type u) ↦ X) c.pt) → (fun (X : Type u) ↦ X) ((forget PartOrdEmb).mapCocone s).pt),
              inj' := ⋯ } :
            (a : CoconePt hc) → (↑s.pt : Type u))
          x :
        (↑s.pt : Type u))
      (({
              toFun :=
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
                      (hc.desc
                        (Functor.mapCocone
                          (forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u))
                            (CC := carrier))
                          s))) :
                  (a : (fun (X : Type u) ↦ X) c.pt) → (fun (X : Type u) ↦ X) ((forget PartOrdEmb).mapCocone s).pt),
              inj' := ⋯ } :
            (a : CoconePt hc) → (↑s.pt : Type u))
          y :
        (↑s.pt : Type u)) ↔
    x ≤ y

Tactic:
obtain ⟨j, x', y', rfl, rfl⟩ :=
      Types.FilteredColimit.jointly_surjective_of_isColimit₂ hc x y

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