mathlib3

f9151066 - chore(data/set/lattice): a few lemmas, golf (#8795)