-- 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' := ⋯ }
tauto tauto₁ tauto₂ tauto₃ tauto₄ 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)
⊢ 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)

Tactic:
tauto