mathlib

e5acda42 - chore(order/conditionally_complete_lattice): drop an unneeded `nonempty` assumption (#10132)