-- Lean 4 proof step from Mathlib.Order.Category.NonemptyFinLinOrd (goal)
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' := ⋯ }
⊢ Monotone (β := (↑Y.1 : Type u))
    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)
have tauto : ∀
  ⦃a b :
    (↑(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)⦄,
  a ≤ b →
    LE.le.{u} (α := (↑Y.1 : Type u))
      ((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))
        a)
      ((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))
        b)
Tactic: tauto