English
Let s be a finite set, and a,b elements with b ∉ s and a ∉ s ∪ {b}. Then (s ∪ {b}) ∪ {a} = (s ∪ {a}) ∪ {b}.
Русский
Пусть s — конечное множество, а и b — элементы так, что b ∉ s и a ∉ s ∪ {b}. Тогда (s ∪ {b}) ∪ {a} = (s ∪ {a}) ∪ {b}.
LaTeX
$$$\forall s: Finset\,\alpha\,\forall a,b: α:\ b \notin s ∧ a \notin s \cup \{b\} \Rightarrow (s \cup \{b\}) \cup \{a\} = (s \cup \{a\}) \cup \{b\}$$$
Lean4
theorem cons_swap (hb : b ∉ s) (ha : a ∉ s.cons b hb) :
(s.cons b hb).cons a ha =
(s.cons a fun h ↦ ha (mem_cons.mpr (.inr h))).cons b fun h ↦
ha (mem_cons.mpr (.inl ((mem_cons.mp h).elim symm (fun h ↦ False.elim (hb h))))) :=
eq_of_veq <| Multiset.cons_swap a b s.val
