mathlib3

2063a528 - feat(order/partial_sups): complete lattice lemmas (#8480)