mathlib3

80dc445d - refactor(order/bounded_lattice): generalize le on with_{top,bot} (#10085)

refactor(order/bounded_lattice): generalize le on with_{top,bot} (#10085) Before, some lemmas assumed `preorder` even when they were true for just the underlying `le`. In the case of `with_bot`, the missing underlying `has_le` instance is defined. For both `with_{top,bot}`, a few lemmas are generalized accordingly.