Commit 2024-01-09 09:25 fb274b38

View on Github →

feat: More WithBot lemmas (#9580) This makes simp stronger on WithBot, for use in #9083. Also reorder the relevant lemmas so that the WithTop and WithBot sections are more identical.

Estimated changes

modified theorem Interval.bot_ne_one
modified theorem Interval.one_ne_bot
added theorem WithBot.bot_ne_one
modified theorem WithBot.coe_eq_one
modified theorem WithBot.coe_le_one
modified theorem WithBot.coe_lt_one
modified theorem WithBot.coe_one
added theorem WithBot.one_eq_coe
modified theorem WithBot.one_le_coe
modified theorem WithBot.one_lt_coe
added theorem WithBot.one_ne_bot
modified theorem WithBot.unbot_one'
modified theorem WithTop.coe_eq_one
modified theorem WithTop.one_eq_coe
modified theorem WithTop.one_ne_top
modified theorem WithTop.top_ne_one