mathlib3

1d7f4798 - feat(data/set/basic): Add `set.nontrivial` predicate and API (#15867)

feat(data/set/basic): Add `set.nontrivial` predicate and API (#15867) Analogously to the existing `set.subsingleton`, we add `set.nontrivial` and the corresponding API. This allows for dot notation to be used for `set.nontrivial` (which is equivalent to ¬ `set.subsingleton`). We also make some small changes to `set.subsingleton`, mostly style tweaks, a rename, and a missing lemma. Co-authored-by: Wrenna Robson <34025592+linesthatinterlace@users.noreply.github.com>