feat(data/set/basic): eq_singleton_iff_unique_mem (#4387)
feat(data/set/basic): eq_singleton_iff_unique_mem (#4387)

We have this lemma for `finset`.  Add a version for `set` (with the
same name).






leanprover-community/mathlib,leanprover-community/mathlib