English
If xs is without duplicates, then xs.sym n is without duplicates for every n.
Русский
Если xs не содержит повторов, то xs.sym n не содержит повторов для каждого n.
LaTeX
$$$ xs.Nodup \rightarrow (xs.sym n).Nodup $$$
Lean4
protected theorem sym (n : ℕ) {xs : List α} (h : xs.Nodup) : (xs.sym n).Nodup :=
match n, xs with
| 0, _ => by simp [List.sym]
| n + 1, [] => by simp [List.sym]
| n + 1, x :: xs => by
rw [List.sym]
refine Nodup.append (Nodup.map ?inj (Nodup.sym n h)) (Nodup.sym (n + 1) h.of_cons) ?disj
case inj =>
intro z z'
simp
case disj =>
intro z hz hz'
rw [mem_map] at hz
obtain ⟨z, _hz, rfl⟩ := hz
have := first_mem_of_cons_mem_sym hz'
simp only [nodup_cons, this, not_true_eq_false, false_and] at h
