mathlib

4a4a3a90 - chore(data/finset/basic): Golf and compress (#11987)

chore(data/finset/basic): Golf and compress (#11987) * Move the `lattice` instance earlier so that it can be used to prove lemmas * Golf proofs * Compress statements within the style guidelines