-- 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
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
hx :
  Eq (α :=
    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)
            (c.ι.app j ≫
              hc.desc
                (Functor.mapCocone
                  (forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                    carrier))
                  s)) :
          (a : (F ⋙ forget PartOrdEmb).obj j) → ((forget PartOrdEmb).mapCocone s).pt)
        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 _ types TypeCat.Fun _ _ _ _ _
              (NatTrans.app
                (Cocone.ι
                  (Functor.mapCocone
                    (forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                      carrier))
                    s))
                j) :
            TypeCat.Fun
              ((F ⋙
                    forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                      carrier)).obj
                j)
              (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))) :
          (a : (F ⋙ forget PartOrdEmb).obj j) → ((forget PartOrdEmb).mapCocone s).pt)
        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))
hy :
  Eq (α :=
    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)
            (c.ι.app j ≫
              hc.desc
                (Functor.mapCocone
                  (forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                    carrier))
                  s)) :
          (a : (F ⋙ forget PartOrdEmb).obj j) → ((forget PartOrdEmb).mapCocone s).pt)
        y' :
      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 _ types TypeCat.Fun _ _ _ _ _
              (NatTrans.app
                (Cocone.ι
                  (Functor.mapCocone
                    (forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                      carrier))
                    s))
                j) :
            TypeCat.Fun
              ((F ⋙
                    forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                      carrier)).obj
                j)
              (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))) :
          (a : (F ⋙ forget PartOrdEmb).obj j) → ((forget PartOrdEmb).mapCocone s).pt)
        y' :
      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))
⊢ LE.le (α := (↑s.pt : Type u))
      (({
              toFun :=
                (⇑(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),
              inj' := ⋯ } :
            (a : CoconePt hc) → (↑s.pt : Type u))
          ((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)) :
        (↑s.pt : Type u))
      (({
              toFun :=
                (⇑(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),
              inj' := ⋯ } :
            (a : CoconePt hc) → (↑s.pt : Type u))
          ((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)) :
        (↑s.pt : Type u)) ↔
    LE.le (α := 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))
have simp : ∀
  (hx :
    Eq (α := ToType (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier) s.pt)
      (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                (hc.desc
                  (Functor.mapCocone
                    (forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                      carrier))
                    s)) :
              TypeCat.Fun c.pt
                (ToType (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier) s.pt)) :
            (a : c.pt) → ToType s.pt)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j) : (a : ToType (F.obj j)) → c.pt) x' : c.pt) :
        ToType (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier) s.pt)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
              (s.ι.app j) :
            (a : (↑(F.obj j) : Type u)) → (↑s.pt : Type u))
          x' :
        (↑s.pt : Type u)))
  (hy :
    Eq (α := ToType (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier) s.pt)
      (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                (hc.desc
                  (Functor.mapCocone
                    (forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                      carrier))
                    s)) :
              TypeCat.Fun c.pt
                (ToType (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier) s.pt)) :
            (a : c.pt) → ToType s.pt)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j) : (a : ToType (F.obj j)) → c.pt) y' : c.pt) :
        ToType (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier) s.pt)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
              (s.ι.app j) :
            (a : (↑(F.obj j) : Type u)) → (↑s.pt : Type u))
          y' :
        (↑s.pt : Type u))),
  LE.le (α := (↑s.pt : Type u))
      (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                (hc.desc
                  (Functor.mapCocone
                    (forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                      carrier))
                    s)) :
              TypeCat.Fun c.pt
                (ToType (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier) s.pt)) :
            (a : c.pt) → ToType s.pt)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j) : (a : ToType (F.obj j)) → c.pt) x' : c.pt) :
        ToType (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier) s.pt)
      (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                (hc.desc
                  (Functor.mapCocone
                    (forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC :=
                      carrier))
                    s)) :
              TypeCat.Fun c.pt
                (ToType (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier) s.pt)) :
            (a : c.pt) → ToType s.pt)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j) : (a : ToType (F.obj j)) → c.pt) y' : c.pt) :
        ToType (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier) s.pt) ↔
    LE.le (α := CoconePt hc)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j) : (a : ToType (F.obj j)) → c.pt) x' : c.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j) : (a : ToType (F.obj j)) → c.pt) y' : c.pt)
Tactic: simp only [Functor.mapCocone_pt, Functor.comp_obj, Functor.const_obj_obj,
      CategoryTheory.comp_apply, Functor.mapCocone_ι_app, ConcreteCategory.hom_ofHom,
      TypeCat.Fun.coe_mk, Function.Embedding.coeFn_mk] at hx hy ⊢
Cleared hypotheses: hx, hy