Commit 2022-07-10 15:28 e5b8d09b

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.