[Merged by Bors] - feat(Data/ENat): add lemma ENat.iInf_eq_coe_iff

[IvanRenison]

Co-authored-by: SnirBroshi 26556598+SnirBroshi@users.noreply.github.com

---

Zulip thread

[github-actions]

PR summary 84a93e3a40

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ ciInf_eq_iff
+ csInf_eq_iff
+ iInf_eq_coe_iff

You can run this locally as follows

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

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

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

---

No changes to technical debt.

You can run this locally as

./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]

This looks good to me, but can you also add the dual versions of the general versions (with sup instead of inf)?

[IvanRenison]

@Vierkantor do you know where exactly should I add the duals?

[Vierkantor]

(Feel free to remove the awaiting-author label when you think you are done / are waiting for review feedback!)

I tried to dualize this myself, but it turns out argminOn doesn't have the argmaxOn counterpart, and so we'd need to redo the whole proof anyway. So this looks good to me for now, and later on @[to_dual] should automate the dualizing. In other words: this looks good to me.

I'm not sure if you had any other changes planned, and that's why you didn't remove the awaiting-author label yet. So:

bors d+

[mathlib-bors]

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

[IvanRenison]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

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