mathlib

d532eb60 - feat(order/lattice): sup_left_idem and similar (#2768)