mathlib

e5b8d09b - feat(data/finset/lattice): add three*2 lemmas about `finset.max/min` (#15212)

feat(data/finset/lattice): add three*2 lemmas about `finset.max/min` (#15212) The three lemmas are * `mem_le_max: ↑a ≤ s.max`, * `max_mono : s.max ≤ t.max`, * `max_le : s.max ≤ M`, and * `min_le_coe_of_mem : s.min`, * `min_mono : t.min ≤ s.min`, * `le_min : m ≤ s.min`. ~~I feel that I did not get the hang of `finset.max`: probably a lot of golfing is possible, at least for `max_mono`!~~ Luckily, Eric looked at the PR and now the proofs have been shortened! I also golfed `le_max_of_mem` and `min_le_of_mem`.