-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
Goal:
X Y : NonemptyFinLinOrd
f : X ⟶ Y
I : NonemptyFinLinOrd :=
  of
    (↑(Set.image (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) X)
          (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
                (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
                (↑X.toLinOrd : Type u)) f) :
            (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
              (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y)
          ⊤) :
      Type u)
e : X ⟶ I :=
  ofHom
    {
      toFun := fun (x : (↑X.1 : Type u)) ↦
        Subtype.mk (p := fun (x : (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) Y) ↦
          Membership.mem (γ := Set ((fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) Y))
            (Set.image (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) X)
              (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
                    (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
                    (↑X.toLinOrd : Type u)) f) :
                (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
                  (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y)
              ⊤)
            x)
          ((ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
                (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
                (↑X.toLinOrd : Type u)) f :
              (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
                (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y)
            x)
          ⋯,
      monotone' := ⋯ }
m : I ⟶ Y :=
  ofHom
    {
      toFun :=
        fun
          (y :
            (↑(Set.image (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) X)
                  (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
                        (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
                        (↑X.toLinOrd : Type u)) f) :
                    (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
                      (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y)
                  ⊤) :
              Type u)) ↦
        (↑y : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y),
      monotone' := ⋯ }
y : (↑X.toLinOrd : Type u)
h : Membership.mem (γ := Set ((fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) X)) ⊤ y
⊢ ∃ (a : (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) X),
    Eq (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) I)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
              (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
              (↑X.toLinOrd : Type u)) e :
            (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
              (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) I)
          a :
        (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) I)
      (Subtype.mk (p := fun (x : (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) Y) ↦
          Membership.mem (γ := Set ((fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) Y))
            (Set.image (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) X)
              (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
                    (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
                    (↑X.toLinOrd : Type u)) f) :
                (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
                  (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y)
              ⊤)
            x)
          ((ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
                (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
                (↑X.toLinOrd : Type u)) f :
              (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
                (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y)
            y)
          ⋯ :
        { x : (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) Y //
          Membership.mem (γ := Set ((fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) Y))
            (Set.image (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) X)
              (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
                    (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
                    (↑X.toLinOrd : Type u)) f) :
                (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
                  (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y)
              ⊤)
            x })

Tactic:
⟨y, rfl⟩

Premises used: Exists.intro, rfl