[Merged by Bors] - feat(Mathlib/Order/SuccPred/Limit): more WithTop lemmas about IsMin/CovBy/IsSuccLimit

[SnirBroshi]

---

Continues the work from #38244

We should probably also have such lemmas for WithTopBot/WithBotTop, but that's for another day

[github-actions]

PR summary 8a2749e633

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ _root_.WithTop.isPredLimit_coe_iff
+ _root_.WithTop.isPredLimit_iff
+ _root_.WithTop.isSuccLimit_coe_iff
+ _root_.WithTop.isSuccLimit_iff_of_isSuccArchimedean
+ _root_.WithTop.isSuccPrelimit_coe_iff
+ _root_.WithTop.isSuccPrelimit_iff_of_isSuccArchimedean
+ eq_bot_of_isEmpty
+ isMax_coe_iff
+ isMax_iff
+ isSuccPrelimit_iff_of_orderBot
+ not_coe_wcovBy_top
+ not_covBy_of_denselyOrdered
+ not_isMax_top
+ not_top_covBy
+ not_top_wcovBy_coe
+ top_wcovBy_iff
+ wcovBy_top_iff

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 8a2749e).

• +34 new declarations
• −1 removed declarations

+Order.isPredPrelimit_iff_of_orderTop
+Order.isSuccPrelimit_iff_of_orderBot
+WithBot.bot_covBy_iff
+WithBot.bot_wcovBy_iff
-WithBot.covBy_bot_iff
+WithBot.eq_bot_of_isEmpty
+WithBot.isMax_coe_iff
+WithBot.isMax_iff
+WithBot.isPredLimit_coe_iff
+WithBot.isPredLimit_iff_of_isPredArchimedean
+WithBot.isPredPrelimit_coe_iff
+WithBot.isPredPrelimit_iff_of_isPredArchimedean
+WithBot.isSuccLimit_coe_iff
+WithBot.isSuccLimit_iff
+WithBot.not_bot_covBy
+WithBot.not_bot_wcovBy
+WithBot.not_isMax_top
+WithBot.not_wcovBy_bot
+WithTop.eq_top_of_isEmpty
+WithTop.isMin_coe_iff
+WithTop.isMin_iff
+WithTop.isPredLimit_coe_iff
+WithTop.isPredLimit_iff
+WithTop.isSuccLimit_coe_iff
+WithTop.isSuccLimit_iff_of_isSuccArchimedean
+WithTop.isSuccPrelimit_coe_iff
+WithTop.isSuccPrelimit_iff_of_isSuccArchimedean
+WithTop.not_coe_wcovBy_top
+WithTop.not_isMin_bot
+WithTop.not_top_covBy
+WithTop.not_top_wcovBy_coe
+WithTop.wcovBy_top_iff
+not_covBy_of_denselyOrdered
+top_wcovBy_iff
+wcovBy_bot_iff

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 8a2749e633
Reference commit d7f2dbea7d

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/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).

[Vierkantor]

Thanks for the PR! What is the motivation: simply filling out API or do you have a specific goal in mind?

[SnirBroshi]

I needed API for succ limits in ENat for #33501, which led to #Is there code for X? > WithTop succ limits and then #38244, and this fills out more of the API.

I often find myself needing such "casting" lemmas for predicates, e.g. we're also missing them for IsLowerSet and IsCompactElement which I'll probably PR soon.

[Vierkantor]

Thanks! 🎉

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Build
• ci (staging) / Test and lint
• ci (staging) / Lint style
• ci (staging) / Post-Build Step
• ci (staging) / Post-CI job