-- 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₂
pos :
  ∀
    (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))),
    False
⊢ 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))

Tactic:
by_contra h''