-- 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₂
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
d : l₁ ⟶ l
d' : l₂ ⟶ l
h₅ : a ≫ d = a' ≫ d'
h₆ : b ≫ d = b' ≫ d'
⊢ Eq (α := (↑(F.obj l) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
            (F.map (a' ≫ d')) :
          (a : (↑(F.obj j) : Type u)) → (↑(F.obj l) : Type u))
        y₁ :
      (↑(F.obj l) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
            (F.map (a ≫ d)) :
          (a : (↑(F.obj j) : Type u)) → (↑(F.obj l) : Type u))
        y₁ :
      (↑(F.obj l) : Type u))
have rw : Eq (α := (↑(F.obj l) : Type u))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
          (F.map (a' ≫ d')) :
        (a : (↑(F.obj j) : Type u)) → (↑(F.obj l) : Type u))
      y₁ :
    (↑(F.obj l) : Type u))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
          (F.map (a' ≫ d')) :
        (a : (↑(F.obj j) : Type u)) → (↑(F.obj l) : Type u))
      y₁ :
    (↑(F.obj l) : Type u))
Tactic: rw [h₅]