English
If a ∉ s, the sym2 of s with a added decomposes into the disjoint union of new pairs involving a and the old pairs: (s.cons a ha).sym2 = ((s.cons a ha).map (Sym2.mkEmbedding a)).disjUnion s.sym2 (disjointness fact).
Русский
Если a ∉ s, то sym2 от s с добавлением a раскладывается на пополам: новые пары, содержащие a, образуют образ деграммы, а старые пары остаются.
LaTeX
$$If $a \notin s$, then $(s.cons\ a\ ha).sym2 = ((s.cons\ a\ ha).map\,\text{Sym2.mkEmbedding}\ a).disjUnion s.sym2 (by ...)$$$
Lean4
theorem sym2_cons (a : α) (s : Finset α) (ha : a ∉ s) :
(s.cons a ha).sym2 =
((s.cons a ha).map <| Sym2.mkEmbedding a).disjUnion s.sym2 (by simp [Finset.disjoint_left, ha]) :=
val_injective <| Multiset.sym2_cons _ _
