-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
A B : SimplexCategory
f : A ⟶ B
hf :
  IsIso (X :=
    Functor.obj
      (forget SimplexCategory (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
        fun (X : SimplexCategory) ↦ Fin (X.len + 1)))
      A)
    (CategoryTheory.Functor.map
      (forget SimplexCategory (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
        fun (X : SimplexCategory) ↦ Fin (X.len + 1)))
      f)
y₁ y₂ : Fin (B.len + 1)
h : y₁ ≤ y₂
h' : y₁ < y₂
h'' :
  ¬LE.le (α := Fin (A.len + 1))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (inv
                (CategoryTheory.Functor.map
                  (forget SimplexCategory (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1))
                    (CC := fun (X : SimplexCategory) ↦ Fin (X.len + 1)))
                  f)) :
            (a : (fun (X : Type) ↦ X) ((forget SimplexCategory).obj B)) →
              (fun (X : Type) ↦ X) ((forget SimplexCategory).obj A))
          y₁ :
        (fun (X : Type) ↦ X)
          (Functor.obj
            (forget SimplexCategory (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)))
            A))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (inv
                (CategoryTheory.Functor.map
                  (forget SimplexCategory (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1))
                    (CC := fun (X : SimplexCategory) ↦ Fin (X.len + 1)))
                  f)) :
            (a : (fun (X : Type) ↦ X) ((forget SimplexCategory).obj B)) →
              (fun (X : Type) ↦ X) ((forget SimplexCategory).obj A))
          y₂ :
        (fun (X : Type) ↦ X)
          (Functor.obj
            (forget SimplexCategory (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)))
            A))
⊢ LE.le (α := Fin (B.len + 1))
    ((Hom.toOrderHom f : (a : Fin (A.len + 1)) → Fin (B.len + 1))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (inv
                (CategoryTheory.Functor.map
                  (forget SimplexCategory (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1))
                    (CC := fun (X : SimplexCategory) ↦ Fin (X.len + 1)))
                  f)) :
            (a : (fun (X : Type) ↦ X) ((forget SimplexCategory).obj B)) →
              (fun (X : Type) ↦ X) ((forget SimplexCategory).obj A))
          y₂) :
      Fin (B.len + 1))
    ((Hom.toOrderHom f : (a : Fin (A.len + 1)) → Fin (B.len + 1))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (inv
                (CategoryTheory.Functor.map
                  (forget SimplexCategory (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1))
                    (CC := fun (X : SimplexCategory) ↦ Fin (X.len + 1)))
                  f)) :
            (a : (fun (X : Type) ↦ X) ((forget SimplexCategory).obj B)) →
              (fun (X : Type) ↦ X) ((forget SimplexCategory).obj A))
          y₁) :
      Fin (B.len + 1))

Tactic:
f.toOrderHom.monotone (le_of_not_ge h'')

Premises used: OrderHom.monotone, le_of_not_ge, SimplexCategory.Hom.toOrderHom