English
If a ∈ s, then (insert a s).sym2 equals the union of the image of new pairs involving a with s and the old s.sym2; otherwise it reduces to the cons-case above.
Русский
Если a ∈ s, то (insert a s).sym2 равен объединению образа новых пар, содержащих a с s, и старого s.sym2.
LaTeX
$$If $a \in s$, then $(insert\ a\ s).sym2 = ((insert\ a\ s).image (\,\text{Sym2.mkMap}\ a) ).disjUnion s.sym2$$$
Lean4
theorem sym2_insert [DecidableEq α] (a : α) (s : Finset α) :
(insert a s).sym2 = ((insert a s).image fun b => s(a, b)) ∪ s.sym2 :=
by
obtain ha | ha := Decidable.em (a ∈ s)
· simp only [insert_eq_of_mem ha, right_eq_union, image_subset_iff]
simp_all
· simpa [map_eq_image] using sym2_cons a s ha
