induction n with
| zero =>
  have : l = [] := by cases l; rfl; exact Fin.elim0 ‹_›
  cases this; exact Nat.le.refl
| succ n IH =>
  if hn : Fin.last n ∈ l then
    let l' := l.erase <| Fin.last n
    have : l'.length = l.length.pred := List.length_erase_of_mem hn
    have : l.length = l'.length + 1 := Eq.symm <| by
      rewrite [this]
      exact Nat.succ_pred_eq_of_pos <| List.length_pos_of_mem hn
    rewrite [this]; refine Nat.succ_le_succ ?_
    have : last n ∉ l' := List.not_mem_erase_of_nodup _ nodup
    let ⟨l'',hl''⟩ := restrict_of_not_mem_last this
    rewrite [hl'', List.length_map]
    refine IH <| List.nodup_of_nodup_map (f:=castSucc) ?_
    rewrite [← hl'']
    exact nodup.erase _
  else
    let ⟨l',hl'⟩ := restrict_of_not_mem_last hn
    cases hl'; rewrite [List.length_map]
    refine trans (IH ?_) (n.le_succ)
    exact List.nodup_of_nodup_map nodup
m n : Nat
l : List (Fin n)
nodup : List.Nodup l
⊢ List.length l ≤ n
no goals