mathlib3

ceab0e7f - chore(order/bounded_lattice): make `bot_lt_some` and `some_lt_none` consistent (#9180)

chore(order/bounded_lattice): make `bot_lt_some` and `some_lt_none` consistent (#9180) `with_bot.bot_lt_some` gets renamed to `with_bot.none_lt_some` and now syntactically applies to `none : with_bot α` (`with_bot.bot_le_coe` already applies to `⊥` and `↑a`). `with_top.some_lt_none` now takes `a` explicit.