feat(data/set/basic): define `set.subsingleton` (#1939)
* feat(data/set/basic): define `set.subsingleton`
Also rename `nonempty.of_subset` to `nonempty.mono`
* Add a missing lemma
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
