-- Module: Mathlib.Order.Category.PartOrdEmb
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
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' := ⋯ }
                    ⋯)) :
            (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' := ⋯ }
                    ⋯) ≫
                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))
⊢ 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)

Tactic:
ext x