mathlib

0398787b - feat(data/finset/lattice): 3*2 lemmas about max/min and max'/min' (#15978)

feat(data/finset/lattice): 3*2 lemmas about max/min and max'/min' (#15978) The six lemmas in this PR show that * `finset.max` and `finset.max'` coincide (when and how they can); * the `finset.max'` of `s.erase x` is not `x`; * the `finset.max` of `s.erase x` is not `x`; and their `@[to_dual]` analogues.