Commit 2025-02-12 11:53 f5fe9878

View on Github →

chore(Order/WithBot): golf, clean up (#21274)

Shorten proofs
Make the WithBot and WithTop sections analogous
Avoid relying on the defeq (WithTop α)ᵒᵈ = WithBot αᵒᵈ
Pull more implicit variables to variable statements
Stick to the convention that a b : α and x y : WithBot α

Estimated changes

Modified Mathlib/Order/Hom/Basic.lean

Modified Mathlib/Order/WithBot.lean

modified theorem WithBot.bot_lt_coe

modified theorem WithBot.coe_le_coe

modified theorem WithBot.coe_le_iff

modified theorem WithBot.coe_lt_coe

modified theorem WithBot.coe_max

modified theorem WithBot.coe_min

modified theorem WithBot.forall_le_iff_eq_bot

modified theorem WithBot.forall_lt_iff_eq_bot

modified theorem WithBot.ge_of_forall_gt_iff_ge

modified theorem WithBot.le_coe_iff

modified theorem WithBot.le_coe_unbot'

added theorem WithBot.le_def

modified theorem WithBot.le_ofDual_iff

modified theorem WithBot.le_of_forall_lt_iff_le

modified theorem WithBot.le_toDual_iff

modified theorem WithBot.le_unbot_iff

modified theorem WithBot.lt_coe_bot

modified theorem WithBot.lt_coe_iff

added theorem WithBot.lt_def

modified theorem WithBot.lt_iff_exists_coe

modified theorem WithBot.lt_ofDual_iff

modified theorem WithBot.lt_toDual_iff

modified theorem WithBot.lt_unbot_iff

modified theorem WithBot.map_le_iff

modified theorem WithBot.map_ofDual

modified theorem WithBot.map_toDual

modified theorem WithBot.not_coe_le_bot

modified theorem WithBot.ofDual_apply_bot

modified theorem WithBot.ofDual_apply_coe

modified theorem WithBot.ofDual_le_iff

modified theorem WithBot.ofDual_le_ofDual_iff

modified theorem WithBot.ofDual_lt_iff

modified theorem WithBot.ofDual_lt_ofDual_iff

modified theorem WithBot.ofDual_map

modified theorem WithBot.ofDual_symm_apply

modified theorem WithBot.some_lt_some

modified theorem WithBot.toDual_apply_bot

modified theorem WithBot.toDual_apply_coe

modified theorem WithBot.toDual_le_iff

modified theorem WithBot.toDual_le_toDual_iff

modified theorem WithBot.toDual_lt_iff

modified theorem WithBot.toDual_lt_toDual_iff

modified theorem WithBot.toDual_map

modified theorem WithBot.toDual_symm_apply

modified theorem WithBot.unbot'_le_iff

modified theorem WithBot.unbot'_lt_iff

modified theorem WithBot.unbot_le_iff

modified theorem WithBot.unbot_lt_iff

modified theorem WithTop.coe_le_coe

modified theorem WithTop.coe_le_iff

modified theorem WithTop.coe_lt_coe

modified theorem WithTop.coe_lt_iff

modified theorem WithTop.coe_lt_top

modified theorem WithTop.coe_max

modified theorem WithTop.coe_min

modified theorem WithTop.coe_top_lt

modified theorem WithTop.coe_untop'_le

modified theorem WithTop.forall_ge_iff_eq_top

modified theorem WithTop.forall_gt_iff_eq_top

modified theorem WithTop.ge_of_forall_gt_iff_ge

modified theorem WithTop.le_coe_iff

added theorem WithTop.le_def

modified theorem WithTop.le_ofDual_iff

modified theorem WithTop.le_of_forall_lt_iff_le

modified theorem WithTop.le_toDual_iff

modified theorem WithTop.le_untop'_iff

modified theorem WithTop.le_untop_iff

added theorem WithTop.lt_def

modified theorem WithTop.lt_iff_exists_coe

modified theorem WithTop.lt_ofDual_iff

modified theorem WithTop.lt_toDual_iff

modified theorem WithTop.lt_untop'_iff

modified theorem WithTop.lt_untop_iff

modified theorem WithTop.map_le_iff

modified theorem WithTop.not_top_le_coe

modified theorem WithTop.ofDual_le_iff

modified theorem WithTop.ofDual_le_ofDual_iff

modified theorem WithTop.ofDual_lt_iff

modified theorem WithTop.ofDual_lt_ofDual_iff

modified theorem WithTop.toDual_le_iff

modified theorem WithTop.toDual_le_toDual_iff

modified theorem WithTop.toDual_lt_iff

modified theorem WithTop.toDual_lt_toDual_iff

modified theorem WithTop.untop_le_iff

modified theorem WithTop.untop_lt_iff