-- Lean 4 proof step from Mathlib.Order.Category.PartOrdEmb (hypothesis)
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
j : J
x y : (↑(F.1 j) : Type u)
k : J
x' y' : (↑(F.obj k) : Type u)
hx :
  Eq (α := c.pt) ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app k) : (a : ToType (F.obj k)) → c.pt) x' : c.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j) : (a : ToType (F.obj j)) → c.pt) x : c.pt)
hy :
  Eq (α := c.pt) ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app k) : (a : ToType (F.obj k)) → c.pt) y' : c.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j) : (a : ToType (F.obj j)) → c.pt) y : c.pt)
l₁ : J
a₁ : k ⟶ l₁
b₁ : j ⟶ l₁
hl₁ :
  Eq (α := ToType (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier) (F.obj l₁))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
            (F.map a₁) :
          (a : (↑(F.obj k) : Type u)) → (↑(F.obj l₁) : Type u))
        x' :
      (↑(F.obj l₁) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
            (F.map b₁) :
          (a : (↑(F.obj j) : Type u)) → (↑(F.obj l₁) : Type u))
        x :
      (↑(F.obj l₁) : Type u))
l₂ : J
a₂ : k ⟶ l₂
b₂ : j ⟶ l₂
hl₂ :
  Eq (α := ToType (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier) (F.obj l₂))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
            (F.map a₂) :
          (a : (↑(F.obj k) : 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 b₂) :
          (a : (↑(F.obj j) : Type u)) → (↑(F.obj l₂) : Type u))
        y :
      (↑(F.obj l₂) : Type u))
m : J
d : l₁ ⟶ m
h :
  LE.le (α := (↑(F.obj m) : 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 k) : Type u)) → (↑(F.obj m) : Type u))
        x' :
      (↑(F.obj m) : 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 k) : Type u)) → (↑(F.obj m) : Type u))
        y' :
      (↑(F.obj m) : Type u))
d' : l₂ ⟶ m
h₁ : a₁ ≫ d = a₂ ≫ d'
h₂ : b₁ ≫ d = b₂ ≫ d'
⊢ LE.le (α := (↑(F.obj m) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
            (F.map (b₁ ≫ d)) :
          (a : (↑(F.obj j) : Type u)) → (↑(F.obj m) : Type u))
        x :
      (↑(F.obj m) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
            (F.map (b₂ ≫ d')) :
          (a : (↑(F.obj j) : Type u)) → (↑(F.obj m) : Type u))
        y :
      (↑(F.obj m) : Type u))
have h₃ : LE.le (α := (↑(F.obj m) : 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 k) : Type u)) → (↑(F.obj m) : Type u))
      x' :
    (↑(F.obj m) : 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 k) : Type u)) → (↑(F.obj m) : Type u))
      y' :
    (↑(F.obj m) : Type u))
Tactic: conv_rhs at h => rw [h₁]
Cleared hypotheses: h, h₁, h₂