feat(finset/lattice): sup' is to sup as max' is to max (#7087)
Introducing `finset.sup'`, modelled on `finset.max'` but having no need for a `linear_order`. I wanted this for functions so also provide `sup_apply` and `sup'_apply`. By using `cons` instead of `insert` the axiom of choice is avoided throughout and I have replaced the proofs of three existing lemmas (`sup_lt_iff`, `comp_sup_eq_sup_comp`, `sup_closed_of_sup_closed`) that didn't need it. I have removed `sup_subset` entirely as it was surely introduced in ignorance of `sup_mono`.
