-- 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
x y : 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
h₁ : x₁ ≤ y₁
k : J
y₂ x₂ : (↑(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
hx₂ :
  (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₂ =
    x
h₂ : y₂ ≤ x₂
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₁))
        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 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₁))
⊢ ∃ (l : J) (a : j ⟶ l) (b : k ⟶ l) (x₃ : (↑(F.obj l) : Type u)) (y₃ : (↑(F.obj l) : Type u)),
    x₃ =
        (ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
              (F.map a) :
            (a : (↑(F.obj j) : Type u)) → (↑(F.obj l) : Type u))
          x₁ ∧
      x₃ =
          (ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
                (F.map b) :
              (a : (↑(F.obj k) : Type u)) → (↑(F.obj l) : Type u))
            x₂ ∧
        y₃ =
            (ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                  carrier) (F.map a) :
                (a : (↑(F.obj j) : Type u)) → (↑(F.obj l) : Type u))
              y₁ ∧
          y₃ =
            (ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                  carrier) (F.map b) :
                (a : (↑(F.obj k) : Type u)) → (↑(F.obj l) : Type u))
              y₂
have obtain : ∀ (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₂))),
  ∃ (l : J) (a : j ⟶ l) (b : k ⟶ l) (x₃ : (↑(F.obj l) : Type u)) (y₃ : (↑(F.obj l) : Type u)),
    x₃ =
        (ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
              (F.map a) :
            (a : (↑(F.obj j) : Type u)) → (↑(F.obj l) : Type u))
          x₁ ∧
      x₃ =
          (ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
                (F.map b) :
              (a : (↑(F.obj k) : Type u)) → (↑(F.obj l) : Type u))
            x₂ ∧
        y₃ =
            (ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                  carrier) (F.map a) :
                (a : (↑(F.obj j) : Type u)) → (↑(F.obj l) : Type u))
              y₁ ∧
          y₃ =
            (ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                  carrier) (F.map b) :
                (a : (↑(F.obj k) : Type u)) → (↑(F.obj l) : Type u))
              y₂
Tactic: obtain ⟨l₂, a', b', h₄⟩ :=
        (Types.FilteredColimit.isColimit_eq_iff _ hc (xi := y₁) (xj := y₂)).1
          (hy₁.trans hy₂.symm)