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
case succ
m n✝ n : Nat
IH : ∀ {l : List (Fin n)}, List.Nodup l → List.length l ≤ n
l : List (Fin (Nat.succ n))
nodup : List.Nodup l
⊢ List.length l ≤ Nat.succ n
no goals