let f' (x : Fin n) : Fin n :=
  let x' : Fin (n + 1) := ⟨x.val, Nat.lt_trans x.isLt (Nat.lt_succ_self n)⟩
  let y := f x'
  if isLt : y.val < n then
    ⟨y.val, isLt⟩
  else
    have eqx : f x' = n' := Fin.eq_of_not_lt isLt
    have isLt : f n' < n' := by
      by_contra nlt
      have eqn : f n' = n' := Fin.eq_of_not_lt nlt
      have : f x' = f n' := by rw [eqx, eqn]
      have : x' = n' := h _ _ this
      have : x.val = n := by
        have : x'.val = n'.val := by rw [this]
        exact this
      exact Nat.lt_irrefl _ (this ▸ x.isLt)
    ⟨f ⟨n, Nat.lt_succ_self n⟩, isLt⟩
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
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, ⋯⟩
f' : Fin n → Fin n :=
  fun x =>
    let x' := ⟨↑x, ⋯⟩;
    let y := f x';
    if isLt : ↑y < n then ⟨↑y, isLt⟩
    else
      let_fun eqx := ⋯;
      let_fun isLt := ⋯;
      ⟨↑(f ⟨n, ⋯⟩), isLt⟩
⊢ surj f