feat(data/finset/lattice): Distributivity lemmas (#18611)
Dualise a few existing lemmas, protect `finset.sup_eq_bot_iff`/`finset.inf_eq_top_iff`, move `map_finset_sup`/`map_finset_inf` from `order.hom.lattice` to `data.finset.lattice`, make binders semi-implicit in `finset.disjoint_sup_left` and friends to avoid overly explicit binders in a local assumption after rewriting.
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
