[Merged by Bors] - feat(ToIntervalMod): add missing lemmas

[urkud]

Cherry-picked from #33423, then added more lemmas as requested by @eric-wieser

---

feat(ToIntervalMod): add missing lemmas

[github-actions]

PR summary 73fe7bad3e

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ ExistsUnique.choose_eq_iff
+ self_sub_toIcoDiv_mul
+ self_sub_toIcoMod_eq_mul
+ self_sub_toIocDiv_mul
+ self_sub_toIocMod_eq_mul
+ toIcoDiv_add_intCast_mul
+ toIcoDiv_add_intCast_mul'
+ toIcoDiv_add_natCast_mul
+ toIcoDiv_add_natCast_mul'
+ toIcoDiv_add_nsmul
+ toIcoDiv_add_nsmul'
+ toIcoDiv_add_ofNat_mul
+ toIcoDiv_add_ofNat_mul'
+ toIcoDiv_eq_iff
+ toIcoDiv_intCast_mul_add
+ toIcoDiv_mul_sub_self
+ toIcoDiv_mul_sub_toIcoMod
+ toIcoDiv_natCast_mul_add
+ toIcoDiv_nsmul_add
+ toIcoDiv_ofNat_mul_add
+ toIcoDiv_sub_intCast_mul
+ toIcoDiv_sub_intCast_mul'
+ toIcoDiv_sub_natCast_mul
+ toIcoDiv_sub_natCast_mul'
+ toIcoDiv_sub_nsmul
+ toIcoDiv_sub_nsmul'
+ toIcoDiv_sub_ofNat_mul
+ toIcoDiv_sub_ofNat_mul'
+ toIcoMod_add_intCast_mul
+ toIcoMod_add_intCast_mul'
+ toIcoMod_add_natCast_mul
+ toIcoMod_add_natCast_mul'
+ toIcoMod_add_nsmul
+ toIcoMod_add_nsmul'
+ toIcoMod_add_ofNat_mul
+ toIcoMod_add_ofNat_mul'
+ toIcoMod_add_toIcoDiv_mul
+ toIcoMod_intCast_mul_add
+ toIcoMod_intCast_mul_add'
+ toIcoMod_natCast_mul_add
+ toIcoMod_natCast_mul_add'
+ toIcoMod_nsmul_add
+ toIcoMod_nsmul_add'
+ toIcoMod_ofNat_mul_add
+ toIcoMod_ofNat_mul_add'
+ toIcoMod_sub_intCast_mul
+ toIcoMod_sub_intCast_mul'
+ toIcoMod_sub_natCast_mul
+ toIcoMod_sub_natCast_mul'
+ toIcoMod_sub_nsmul
+ toIcoMod_sub_nsmul'
+ toIcoMod_sub_ofNat_mul
+ toIcoMod_sub_ofNat_mul'
+ toIcoMod_sub_self_eq_mul
+ toIocDiv_add_intCast_mul
+ toIocDiv_add_intCast_mul'
+ toIocDiv_add_natCast_mul
+ toIocDiv_add_natCast_mul'
+ toIocDiv_add_nsmul
+ toIocDiv_add_nsmul'
+ toIocDiv_add_ofNat_mul
+ toIocDiv_add_ofNat_mul'
+ toIocDiv_eq_iff
+ toIocDiv_intCast_mul_add
+ toIocDiv_mul_sub_self
+ toIocDiv_mul_sub_toIocMod
+ toIocDiv_natCast_mul_add
+ toIocDiv_nsmul_add
+ toIocDiv_ofNat_mul_add
+ toIocDiv_sub_intCast_mul
+ toIocDiv_sub_intCast_mul'
+ toIocDiv_sub_natCast_mul
+ toIocDiv_sub_natCast_mul'
+ toIocDiv_sub_nsmul
+ toIocDiv_sub_nsmul'
+ toIocDiv_sub_ofNat_mul
+ toIocDiv_sub_ofNat_mul'
+ toIocMod_add_intCast_mul
+ toIocMod_add_intCast_mul'
+ toIocMod_add_natCast_mul
+ toIocMod_add_natCast_mul'
+ toIocMod_add_nsmul
+ toIocMod_add_nsmul'
+ toIocMod_add_ofNat_mul
+ toIocMod_add_ofNat_mul'
+ toIocMod_add_toIocDiv_mul
+ toIocMod_intCast_mul_add
+ toIocMod_intCast_mul_add'
+ toIocMod_natCast_mul_add
+ toIocMod_natCast_mul_add'
+ toIocMod_nsmul_add
+ toIocMod_nsmul_add'
+ toIocMod_ofNat_mul_add
+ toIocMod_ofNat_mul_add'
+ toIocMod_sub_intCast_mul
+ toIocMod_sub_intCast_mul'
+ toIocMod_sub_natCast_mul
+ toIocMod_sub_natCast_mul'
+ toIocMod_sub_nsmul
+ toIocMod_sub_nsmul'
+ toIocMod_sub_ofNat_mul
+ toIocMod_sub_ofNat_mul'
+ toIocMod_sub_self_eq_mul

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).

[eric-wieser]

bors d+

Thanks!

[mathlib-bors]

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

[leanprover-community-mathlib4-bot]

As this PR is labelled auto-merge-after-CI, we are now sending it to bors:

bors merge

[mathlib-bors]

Build failed (retrying...):

• Post-Build Step

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Post-Build Step
• Lint style