mathlib3

9ac7c0c8 - feat(data/finset/basic): `insert` and `erase` lemmas (#18729)

feat(data/finset/basic): `insert` and `erase` lemmas (#18729) Interaction of `insert` and `erase` with `inter`, `union` and `disjoint`. Co-authored-by: Eric Rodriguez <ericrboidi@gmail.com>