chore(data/finset): golf some proofs (#6101)
* prove that `finset.min'` and `finset.max'` are `is_least` and
`is_greatest` elements of the corresponding sets;
* use this fact to golf some proofs;
generalize `min'_lt_max'` to `is_glb_lt_is_lub_of_ne`;
* add `finset.card_le_one` and `finset.one_lt_card`.
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
