-- 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 x_1 : J
f : x ⟶ x_1
⊢ Eq (α :=
    F.obj x ⟶
      Functor.obj
        (Functor.obj (Functor.const J) { carrier := CoconePt hc, str := instPartialOrderCoconePt hc : PartOrdEmb.{u} })
        x_1)
    (F.map f ≫
        ofHom
          (RelEmbedding.mk (r := fun (x1 x2 : (↑(F.1 x_1) : Type u)) ↦ x1 ≤ x2) (s := fun (x1 x2 : CoconePt hc) ↦
            x1 ≤ x2)
            {
              toFun :=
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app x_1)) :
                  (a : (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj x_1)) →
                    (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj x_1)),
              inj' := ⋯ }
            ⋯) :
      F.obj x ⟶
        Functor.obj
          (Functor.obj (Functor.const J)
            { carrier := CoconePt hc, str := instPartialOrderCoconePt hc : PartOrdEmb.{u} })
          x_1)
    (ofHom
          (RelEmbedding.mk (r := fun (x1 x2 : (↑(F.1 x) : Type u)) ↦ x1 ≤ x2) (s := fun (x1 x2 : CoconePt hc) ↦ x1 ≤ x2)
            {
              toFun :=
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app x)) :
                  (a : (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj x)) →
                    (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj x)),
              inj' := ⋯ }
            ⋯) ≫
        CategoryTheory.Functor.map
          (Functor.obj (Functor.const J)
            { carrier := CoconePt hc, str := instPartialOrderCoconePt hc : PartOrdEmb.{u} })
          f :
      F.obj x ⟶
        Functor.obj
          (Functor.obj (Functor.const J)
            { carrier := CoconePt hc, str := instPartialOrderCoconePt hc : PartOrdEmb.{u} })
          x_1)
have hf : ∀ (x_2 : (↑(F.obj x) : Type u)),
  Eq (α :=
    (↑(Functor.obj
          (Functor.obj (Functor.const J)
            { carrier := CoconePt hc, str := instPartialOrderCoconePt hc : PartOrdEmb.{u} })
          x_1) :
      Type u))
    ((Hom.hom
            (F.map f ≫
              ofHom
                (RelEmbedding.mk (r := fun (x1 x2 : (↑(F.1 x_1) : Type u)) ↦ x1 ≤ x2) (s := fun (x1 x2 : CoconePt hc) ↦
                  x1 ≤ x2)
                  {
                    toFun :=
                      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app x_1)) :
                        (a : (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj x_1)) →
                          (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj x_1)),
                    inj' := sorry }
                  sorry)) :
          (a : (↑(F.obj x) : Type u)) →
            (↑(((Functor.const J).obj { carrier := CoconePt hc, str := instPartialOrderCoconePt hc }).obj x_1) :
              Type u))
        x_2 :
      (↑(Functor.obj
            (Functor.obj (Functor.const J)
              { carrier := CoconePt hc, str := instPartialOrderCoconePt hc : PartOrdEmb.{u} })
            x_1) :
        Type u))
    ((Hom.hom
            (ofHom
                (RelEmbedding.mk (r := fun (x1 x2 : (↑(F.1 x) : Type u)) ↦ x1 ≤ x2) (s := fun (x1 x2 : CoconePt hc) ↦
                  x1 ≤ x2)
                  {
                    toFun :=
                      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app x)) :
                        (a : (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj x)) →
                          (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj x)),
                    inj' := sorry }
                  sorry) ≫
              CategoryTheory.Functor.map
                (Functor.obj (Functor.const J)
                  { carrier := CoconePt hc, str := instPartialOrderCoconePt hc : PartOrdEmb.{u} })
                f) :
          (a : (↑(F.obj x) : Type u)) →
            (↑(((Functor.const J).obj { carrier := CoconePt hc, str := instPartialOrderCoconePt hc }).obj x_1) :
              Type u))
        x_2 :
      (↑(Functor.obj
            (Functor.obj (Functor.const J)
              { carrier := CoconePt hc, str := instPartialOrderCoconePt hc : PartOrdEmb.{u} })
            x_1) :
        Type u))
Tactic: ext x