mathlib3

62d532a7 - feat(data/finset): erase is partially injective (#6737)

feat(data/finset): erase is partially injective (#6737) Show that erase is partially injective, ie that if `s.erase x = s.erase y` and `x` is in `s`, then `x = y`.