mathlib

ee3f8b8d - chore(order/complete_lattice): golf some proofs (#8746)