Commit 2025-10-16 16:35 4b0359cc

View on Github →

refactor: define ≤/< on WithBot/WithTop by induction (#19668) The motivation for this change is that it is really confusing to run intro r s shouldnthaveintroedthat on a goal of the form ∀ r s : ℝ≥0∞, r ≤ s and get the nonsense-looking goal r = ↑shouldnthaveintroedthat → ∃ b : α, s = ↑b ∧ shouldnthaveintroedthat ≤ b⟩ instead of an error, and similarly when destructing something of the form ∃ r s : ℝ≥0∞, r < s. Furthermore, I suspect this improves performance.

Estimated changes

modified theorem WithZero.coe_le_coe
modified theorem WithZero.coe_le_iff
added theorem WithZero.le_coe_iff
modified theorem WithZero.le_def
added theorem WithZero.le_unzero_iff
added theorem WithZero.lt_coe_iff
modified theorem WithZero.lt_def
added theorem WithZero.lt_unzero_iff
modified theorem WithZero.not_coe_le_zero
added theorem WithZero.unbot_le_iff
modified theorem WithZero.unzero_le_unzero
added theorem WithZero.unzero_lt_iff
modified theorem WithZero.zero_le
modified theorem Finset.max_of_mem
modified theorem Finset.min_of_mem
modified theorem WithBot.range_coe
modified theorem WithBot.coe_le_iff
modified theorem WithBot.le_coe_iff
modified theorem WithBot.le_def
added theorem WithBot.le_iff_forall
modified theorem WithBot.lt_def
added theorem WithBot.unbot_le_unbot
added theorem WithBot.unbot_lt_unbot
modified theorem WithTop.coe_le_iff
modified theorem WithTop.le_coe_iff
modified theorem WithTop.le_def
added theorem WithTop.le_iff_forall
modified theorem WithTop.lt_def