-- 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
s : Cocone F
j : J
x' y' :
  (F ⋙ forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)).obj j
h :
  Eq (α := (↑s.pt : Type u))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (hc.desc
              (Functor.mapCocone
                (forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                  carrier))
                s)) :
          (a : (fun (X : Type u) ↦ X) c.pt) → (fun (X : Type u) ↦ X) ((forget PartOrdEmb).mapCocone s).pt)
        ((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' :
          (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) j)) :
      (fun (X : Type u) ↦ X)
        (Cocone.pt (F :=
          F ⋙ forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier))
          (Functor.mapCocone
            (forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier))
            s)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (hc.desc
              (Functor.mapCocone
                (forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                  carrier))
                s)) :
          (a : (fun (X : Type u) ↦ X) c.pt) → (fun (X : Type u) ↦ X) ((forget PartOrdEmb).mapCocone s).pt)
        ((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' :
          (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) j)) :
      (fun (X : Type u) ↦ X)
        (Cocone.pt (F :=
          F ⋙ forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier))
          (Functor.mapCocone
            (forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier))
            s)))
obtain :
  ∀
    (h :
      Eq (α := (↑s.pt : Type u))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (hc.desc
                  (Functor.mapCocone
                    (forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                      carrier))
                    s)) :
              (a : (fun (X : Type u) ↦ X) c.pt) → (fun (X : Type u) ↦ X) ((forget PartOrdEmb).mapCocone s).pt)
            ((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' :
              (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) j)) :
          (fun (X : Type u) ↦ X)
            (Cocone.pt (F :=
              F ⋙
                forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                  carrier))
              (Functor.mapCocone
                (forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                  carrier))
                s)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (hc.desc
                  (Functor.mapCocone
                    (forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                      carrier))
                    s)) :
              (a : (fun (X : Type u) ↦ X) c.pt) → (fun (X : Type u) ↦ X) ((forget PartOrdEmb).mapCocone s).pt)
            ((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' :
              (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) j)) :
          (fun (X : Type u) ↦ X)
            (Cocone.pt (F :=
              F ⋙
                forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                  carrier))
              (Functor.mapCocone
                (forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                  carrier))
                s)))),
    Eq (α := CoconePt hc)
      ((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' :
        (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) j))
      ((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' :
        (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) j))
⊢ Eq (α := CoconePt hc)
    ((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' :
      (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) j))
    ((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' :
      (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) j))

Tactic:
obtain rfl := (s.ι.app j).injective
      (((ConcreteCategory.congr_hom (hc.fac ((forget _).mapCocone s) j) x').symm.trans h).trans
        (ConcreteCategory.congr_hom (hc.fac ((forget _).mapCocone s) j) y'))

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Functor.mapCocone, CategoryTheory.Limits.Cocone.ι, PartOrdEmb.Hom.injective, CategoryTheory.forget, CategoryTheory.ConcreteCategory.congr_hom, Eq.symm, CategoryTheory.NatTrans.app, rfl, Eq.trans