English
If x ∉ xs, then the family {s(x,y) | y ∈ xs} is disjoint from xs.sym2 after mapping.
Русский
Если x ∉ xs, то множество s(x,y) по y ∈ xs и xs.sym2 развивает взаимно непересечение.
LaTeX
$$$$ x \\notin xs \\Rightarrow (\\mathrm{map}(\\lambda y. s(x,y)) xs) \\perp xs.sym2 $$$$
Lean4
theorem map_mk_disjoint_sym2 (x : α) (xs : List α) (h : x ∉ xs) : (map (fun y ↦ s(x, y)) xs).Disjoint xs.sym2 := by
induction xs with
| nil => simp
| cons x' xs ih =>
simp only [mem_cons, not_or] at h
rw [List.sym2, map_cons, map_cons, disjoint_cons_left, disjoint_append_right, disjoint_cons_right]
refine ⟨?_, ⟨?_, ?_⟩, ?_⟩
· refine not_mem_cons_of_ne_of_not_mem ?_ (not_mem_append ?_ ?_)
· simp [h.1]
· simp_rw [mem_map, not_exists, not_and]
intro x'' hx
simp_rw [Sym2.mk_eq_mk_iff, Prod.swap_prod_mk, Prod.mk.injEq, true_and]
rintro (⟨rfl, rfl⟩ | rfl)
· exact h.2 hx
· exact h.2 hx
· simp [mk_mem_sym2_iff, h.2]
· simp [h.1]
· intro z hx hy
rw [List.mem_map] at hx hy
obtain ⟨a, hx, rfl⟩ := hx
obtain ⟨b, hy, hx⟩ := hy
simp only [Sym2.eq, Sym2.rel_iff', Prod.mk.injEq, Ne.symm h.1, false_and, Prod.swap_prod_mk, false_or] at hx
obtain ⟨rfl, rfl⟩ := hx
exact h.2 hy
· exact ih h.2
