[Merged by Bors] - refactor: define ≤/< on WithBot/WithTop by induction

[YaelDillies]

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.

---

• depends on: [Merged by Bors] - chore: rename the fact that (∀ a < a₁, a ≤ a₂) ↔ a₁ ≤ a₂ in a dense order #20317
• depends on: [Merged by Bors] - chore(Data/List/MinMax): fix lemma names #20318
• depends on: [Merged by Bors] - chore(Order/WithBot): golf, clean up #21274
• depends on: [Merged by Bors] - chore(Algebra/Order/Monoid/Unbundled/WithTop): golf, clean up #22109

[github-actions]

PR summary f1634b790d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ LE
+ _root_.IsMax.withZero
+ instance (priority := 10) instLE : LE (WithBot α) where le := WithBot.LE
+ instance (priority := 10) instLE : LE (WithTop α) where le a b := WithBot.LE (α := αᵒᵈ) b a
+ instance (priority := 10) instLT : LT (WithBot α)
+ instance (priority := 10) instLT : LT (WithTop α)
+ instance (priority := 10) instLT : LT (WithZero α) := WithBot.instLT
+ instance (priority := 10) le : LE (WithZero α) := WithBot.instLE
+ instance : LE (Interval α) := WithBot.instLE
+ instance : OrderBot (Interval α) := WithBot.instOrderBot
+ le_unzero_iff
+ lt_coe_iff
+ lt_iff_exists_coe
+ lt_unzero_iff
+ nonpos_iff_eq_zero
+ pos_iff_ne_zero
+ unbot_le_iff
+ unbot_le_unbot
+ unbot_lt_unbot
+ unzero_lt_iff
++ le_iff_forall
++- instOrderBot
++- instPreorder
++--+- le_def
+-+ instBoundedOrder
+-+ instPartialOrder
+-+-+ le_coe_iff
+-+-+- coe_le_iff
- instance (priority := 10) le : LE (WithBot α)
- instance (priority := 10) le : LE (WithTop α)
- instance (priority := 10) le : LE (WithZero α)
- instance (priority := 10) lt : LT (WithBot α)
- instance (priority := 10) lt : LT (WithTop α)
- instance (priority := 10) lt : LT (WithZero α)
- instance : LE (Interval α) := WithBot.le
- instance : OrderBot (Interval α) := WithBot.orderBot
- orderBot
- orderTop
- partialOrder
- preorder
-+--++ lt_def

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.

[JovanGerb]

How does this PR interact with the recent push by @kim-em to make WithBot and WithTop be the same inductive? Given what you said in your last message, I think it would be fitting to have the ≤ relation also be a shared inductive.

[YaelDillies]

How does this PR interact with the recent push by @kim-em to make WithBot and WithTop be the same inductive? Given what you said in your last message, I think it would be fitting to have the ≤ relation also be a shared inductive.

I was thinking the same, in fact. It's not my favorite solution, but I'll try it

[Vierkantor]

I'm marking this PR as awaiting-author until you implement the shared inductive ≤ relation. Feel free to remove the label if you don't think this is a good idea anymore.

[JovanGerb]

Wouldn't le_iff_forall be a more sensible name compared to le_iff_exists?

[b-mehta]

This looks pretty undesirable to me: the test was meant to be showing that finiteness is suggested on this goal, and now tauto_set is suggested to show finiteness of 1?

[JovanGerb]

In my opinion, hint is quite broken. It only suggests one thing and it doesn't have a way of telling which suggesting is better that which other suggestion.

[YaelDillies]

Yes, unfortunately this test is not very deterministic and so I can't do much about it

[Vierkantor]

I like the change! Now that most of the build issues and conflict with other PRs appear fixed, let's get this merged.

bors d+

[mathlib-bors]

✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[YaelDillies]

bors merge

[mathlib-bors]

Build failed:

• Post-Build Step

[YaelDillies]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style
• Post-Build Step

[JovanGerb]

@YaelDillies, I'm a bit confused why you defined ≤ as an inductive predicate, but < using match. Are you going to define < as an inductive predicate in a future PR?

[YaelDillies]

Indeed that was an accident. I have just opened #30848 to fix it.