mathlib

4a38f249 - chore(data/set/basic): Make `set.nonempty.ne_empty` an alias (#17382)

chore(data/set/basic): Make `set.nonempty.ne_empty` an alias (#17382) Make `nonempty.ne_empty` an alias of `ne_empty_iff_nonempty` and remove `empty_not_nonempty` in favor of `not_nonempty_empty`.