have : inj f' := by
  intro x y eq
  let x' : Fin (n + 1) := ⟨x.val, Nat.lt_trans x.isLt (Nat.lt_succ_self n)⟩
  let y' : Fin (n + 1) := ⟨y.val, Nat.lt_trans y.isLt (Nat.lt_succ_self n)⟩
  if hx : f x' < n then
    if hy : f y' < n then
      simp [f', hx, hy] at eq
      have := h _ _ (Fin.eq_of_val_eq eq)
      simp at this
      exact Fin.eq_of_val_eq this
    else
      simp [f', hx, hy] at eq
      have := h _ _ (Fin.eq_of_val_eq eq)
      simp at this
      exact absurd (this ▸ x.isLt) (Nat.lt_irrefl _)
  else
    if hy : f y' < n then
      simp [f', hx, hy] at eq
      have := h _ _ (Fin.eq_of_val_eq eq)
      simp at this
      exact absurd (this.symm ▸ y.isLt) (Nat.lt_irrefl _)
    else
      have eqx := Fin.eq_of_not_lt hx
      have eqy := Fin.eq_of_not_lt hy
      have : f x' = f y' := by rw [eqx, eqy]
      have : x' = y' := h _ _ this
      have : x.val = y.val := by
        have : x'.val = y'.val := by rw [this]
        exact this
      exact Fin.eq_of_val_eq this
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
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⟩
this : inj f'
⊢ surj f