mathlib3

feat(data/set/basic): more lemmas about `set.nonempty`

#1780

Merged