mathlib

c205fe15 - chore(order/conditionally_complete_lattice): golf three proofs (#16064)