mathlib3

7802ba77 - refactor(data/set/basic): review API of `set.nontrivial` (#16737)

refactor(data/set/basic): review API of `set.nontrivial` (#16737) * make `z` an explicit argument in `set.nontrivial.exists_ne`; * rename `set.nontrivial.iff_exists_lt` to `set.nontrivial_iff_exists_lt`; * protect lemmas `set.nontrivial.nonempty` and `set.nontrivial.ne_empty`.