chore(data/option,data/set): a few lemmas, golf (#8636)
* add `option.subsingleton_iff_is_empty` and an instance
`option.unique`;
* add `set.is_compl_range_some_none`, `set.compl_range_some`,
`set.range_some_inter_none`, `set.range_some_union_none`;
* split the proof of `set.pairwise_on_eq_iff_exists_eq` into
`set.nonempty.pairwise_on_eq_iff_exists_eq` and
`set.pairwise_on_eq_iff_exists_eq`.
Inspired by #8579
