Commit 2024-06-01 02:58 3ecc0fed
View on Github →chore: deprecate bad lemmas about WithTop/WithBot (#13128)
Order/WithBot.lean
seems to frequently confuse WithBot.some
and Option.some
, and some of the lemmas are strange as a result.
By teaching cases
not to introduce Option.some
, we no longer need these weird lemmas.
This deprecates:
List.maximum_eq_none
→List.maximum_eq_bot
List.minimum_eq_none
→List.maximum_eq_top
WithBot.some_le_some
→WithBot.coe_le_coe
WithBot.some_lt_some
→WithBot.coe_lt_coe
WithBot.none_lt_some
→WithBot.bot_lt_coe
WithBot.not_lt_none
→WithBot.not_lt_bot
WithBot.none_le
→bot_le
WithTop.some_le_some
→WithTop.coe_le_coe
WithTop.some_lt_some
→WithTop.coe_lt_coe
WithTop.some_lt_none
→WithTop.coe_lt_top
WithTop.not_none_lt
→WithTop.not_top_lt
WithTop.le_none
→le_top
It's still occasionally possible to end up withOption.some a : WithTop A
, but when this happens you can rewrite bysome_eq_coe
first to fix it.