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 with Option.some a : WithTop A, but when this happens you can rewrite by some_eq_coe first to fix it.

Estimated changes

added theorem List.maximum_eq_bot
modified theorem List.maximum_eq_none
modified theorem List.minimum_eq_none
added theorem List.minimum_eq_top
modified theorem WithBot.bot_lt_coe
modified theorem WithBot.coe_le_coe
modified theorem WithBot.coe_lt_coe
modified theorem WithBot.none_le
modified theorem WithBot.none_lt_some
modified theorem WithBot.not_lt_none
modified theorem WithBot.some_le_some
modified theorem WithBot.some_lt_some
modified theorem WithTop.coe_strictMono
modified theorem WithTop.le_none
modified theorem WithTop.not_none_lt
modified theorem WithTop.some_lt_none
modified theorem WithTop.some_lt_some