mathlib3

feat(*): a few more theorems about `unique` and `subsingleton`

#2230

Merged