by_contra nlt
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → surj f
f : Fin (n + 1) → Fin (n + 1)
h : inj f
n' : Fin (n + 1) := ⟨n, ⋯⟩
x : Fin n
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y : Fin (n + 1) := f x'
isLt : ¬↑y < n
eqx : f x' = n'
⊢ f n' < n'
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → surj f
f : Fin (n + 1) → Fin (n + 1)
h : inj f
n' : Fin (n + 1) := ⟨n, ⋯⟩
x : Fin n
x' : Fin (n + 1) := ⟨↑x, ⋯⟩
y : Fin (n + 1) := f x'
isLt : ¬↑y < n
eqx : f x' = n'
nlt : ¬f n' < n'
⊢ False