let n' : Fin (n + 1) := ⟨n, Nat.lt_succ_self n⟩
case succ
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → surj f
f : Fin (n + 1) → Fin (n + 1)
h : inj f
⊢ surj f
case succ
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, ⋯⟩
⊢ surj f