mathlib3

324ae4b1 - feat(data/set/basic): define `set.nonempty` (#1779)

feat(data/set/basic): define `set.nonempty` (#1779) * Define `set.nonempty` and prove some basic lemmas * Migrate `well_founded.min` to `set.nonempty` * Fix a docstring and a few names Based on comments in PR * More docs * Linebreaks * +2 docstrings * Fix compile * Fix compile of `archive/imo1988_q6`