mathlib3

feat(data/set/basic): define `set.subsingleton`

#1939

Merged