English
For any Finset s and element a, erase s a is equal to s \\\\ {a}.
Русский
Для любого Finset s и элемента a, erase s a равно s \\\\ {a}.
LaTeX
$$$ \\forall (s : Finset \\alpha) (a : \\alpha), erase s a = s \\\\{ a \\}$$$
Lean4
theorem erase_sdiff_erase (hab : a ≠ b) (hb : b ∈ s) : s.erase a \ s.erase b = { b } := by ext;
aesop
-- TODO: Do we want to delete this lemma and `Finset.disjUnion_singleton`,
-- or instead add `Finset.union_singleton`/`Finset.singleton_union`?