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`.





leanprover-community/mathlib,leanprover-community/mathlib