feat(data/finset/lattice): `sup'`/`inf'` lemmas (#18989)
Match (most of) the lemmas between `finset.sup`/`finset.inf` and `finset.sup'`/`finset.inf'`. Also golf two proofs using `eq_of_forall_ge_iff` to make sure both APIs prove their lemmas in as closely as possible a way. Also define `finset.nontrivial` to match `set.nontrivial`.
