有限集合上の自己単射は全射

/-- `f : Fin n → Fin n` という単射関数は全射でもある -/
example (n : Nat) (f : Fin n → Fin n) (finj : Function.Injective f) : Function.Surjective f := by
  -- 任意に `y : Fin n` が与えられたとする。
  intro y

  -- もし仮に `y` に原像があるならば示すことはない。
  -- そこで `y` に原像がないと仮定して矛盾を導くことにする。
  by_cases hpre : ∃ x, f x = y
  case pos => assumption
  case neg =>
    exfalso

    -- `f` のすべての値を並べた長さ `n` のリストを作る。
    let image := List.ofFn f

    -- `f` の単射性から `image` には重複がない。
    have himage_nodup : image.Nodup := by
      dsimp [List.Nodup]
      rw [List.pairwise_iff_getElem]
      intro i j hi hj hij h
      grind only [= List.getElem_ofFn]

    -- 原像がないと仮定したので、`y` は `image` に含まれない。
    have hnotmem : y ∉ image := by
      grind only [= List.mem_ofFn]

    -- よって `y :: image` にも重複はない。
    have hconsnodup : (y :: image).Nodup :=
      List.nodup_cons.mpr ⟨hnotmem, himage_nodup⟩

    -- `y :: image` の全要素は、`Fin n` の全要素を並べたリストに含まれる。
    have hsubset : y :: image ⊆ List.ofFn (fun i : Fin n => i) := by
      intro z hz
      exact List.mem_ofFn.mpr ⟨z, rfl⟩

    -- 左辺の長さは `n + 1`、右辺の長さは `n` なので、これは矛盾。
    have hlen := hconsnodup.length_le_of_subset hsubset
    simp [image] at hlen
    omega

The issue provides a Lean proof example but does not name a repository file, section, or requested change. First locate the relevant example source and clarify whether this proof should be added or revised. Done means the intended example is integrated in the appropriate place and the project checks pass.