-- Lean 4 proof step from Mathlib.Order.Category.PartOrdEmb (goal)
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
h :
  Eq (α := (↑s.pt : Type u))
    ((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)
        x :
      (fun (X : Type u) ↦ X)
        (Cocone.pt (F :=
          F ⋙ forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier))
          (Functor.mapCocone
            (forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier))
            s)))
    ((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)
        y :
      (fun (X : Type u) ↦ X)
        (Cocone.pt (F :=
          F ⋙ forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier))
          (Functor.mapCocone
            (forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier))
            s)))
⊢ x = y
have 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)
  (h :
    Eq (α := (↑s.pt : Type u))
      ((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)
          ((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)) :
        (fun (X : Type u) ↦ X)
          (Cocone.pt (F :=
            F ⋙
              forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier))
            (Functor.mapCocone
              (forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                carrier))
              s)))
      ((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)
          ((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)) :
        (fun (X : Type u) ↦ X)
          (Cocone.pt (F :=
            F ⋙
              forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier))
            (Functor.mapCocone
              (forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                carrier))
              s)))),
  Eq (α := 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))
Tactic: obtain ⟨j, x', y', rfl, rfl⟩ :=
      Types.FilteredColimit.jointly_surjective_of_isColimit₂ hc x y
Cleared hypotheses: x, y, h