mathlib

8cad81ae - feat(data/{finset,set}/basic): More `insert` and `erase` lemmas (#14675)

feat(data/{finset,set}/basic): More `insert` and `erase` lemmas (#14675) Also turn `finset.disjoint_iff_disjoint_coe` around and change `set.finite.to_finset_insert` take `(insert a s).finite` instead of `s.finite`.