mathlib3

b18b71c4 - refactor(data/finset/lattice): respell `finset.max/finset.min` using `sup/inf coe` (#15217)

refactor(data/finset/lattice): respell `finset.max/finset.min` using `sup/inf coe` (#15217) This PR simply redefines * `finset.max s` with the defeq `finset.sup s coe`, * `finset.min s` with the defeq `finset.sup/inf s coe`. This arose from PR #15212.