English
Deduplicating the Sym2-image commutes with taking deduplication on the base list: dedup of xs.sym2 equals dedup of xs, then sym2.
Русский
Устранение повторяющихся элементов в xs.sym2 совпадает с симметрическим образом после снятия повторов в xs: xs.sym2.dedup = xs.dedup.sym2.
LaTeX
$$$$ xs.sym2.dedup = xs.dedup.sym2 $$$$
Lean4
protected theorem sym2 {xs : List α} (h : xs.Nodup) : xs.sym2.Nodup := by
induction xs with
| nil => simp only [List.sym2, nodup_nil]
| cons x xs ih =>
rw [List.sym2]
specialize ih h.of_cons
rw [nodup_cons] at h
refine Nodup.append (Nodup.cons ?notmem (h.2.map ?inj)) ih ?disj
case disj =>
intro z hz hz'
simp only [mem_cons, mem_map] at hz
obtain ⟨_, (rfl | _), rfl⟩ := hz <;> simp [left_mem_of_mk_mem_sym2 hz'] at h
case notmem =>
intro h'
simp only [h.1, mem_map, Sym2.eq_iff, true_and, or_self, exists_eq_right] at h'
case inj =>
intro a b
simp only [Sym2.eq_iff, true_and]
rintro (rfl | ⟨rfl, rfl⟩) <;> rfl
