-- 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
j : J
x' y' :
  (F ⋙ forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)).obj j
hx :
  Eq (α := ToType (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier) s.pt)
    (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (hc.desc
                (Functor.mapCocone
                  (forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                    carrier))
                  s)) :
            TypeCat.Fun c.pt
              (ToType (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier) s.pt)) :
          (a : c.pt) → ToType s.pt)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j) : (a : ToType (F.obj j)) → c.pt) x' : c.pt) :
      ToType (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier) s.pt)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
            (s.ι.app j) :
          (a : (↑(F.obj j) : Type u)) → (↑s.pt : Type u))
        x' :
      (↑s.pt : Type u))
hy :
  Eq (α := ToType (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier) s.pt)
    (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (hc.desc
                (Functor.mapCocone
                  (forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                    carrier))
                  s)) :
            TypeCat.Fun c.pt
              (ToType (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier) s.pt)) :
          (a : c.pt) → ToType s.pt)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j) : (a : ToType (F.obj j)) → c.pt) y' : c.pt) :
      ToType (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier) s.pt)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
            (s.ι.app j) :
          (a : (↑(F.obj j) : Type u)) → (↑s.pt : Type u))
        y' :
      (↑s.pt : Type u))
h_1 :
  LE.le (α := CoconePt hc)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j) : (a : ToType (F.obj j)) → c.pt) x' : c.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j) : (a : ToType (F.obj j)) → c.pt) y' : c.pt)
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))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j) : (a : ToType (F.obj j)) → c.pt) x' : c.pt)
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))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j) : (a : ToType (F.obj j)) → c.pt) y' : c.pt)
h : x ≤ y
l : J
f : k ⟶ l
g : 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
              f) :
          (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
              g) :
          (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'
have obtain : ∀ (l' : J) (f' : k ⟶ l') (g' : 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
                f') :
            (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'))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((F ⋙
                    forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                      carrier)).map
                g') :
            (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'))),
  x' ≤ y'
Tactic: obtain ⟨l', f', g', hl'⟩ := (Types.FilteredColimit.isColimit_eq_iff _ hc).1 hy'