[Merged by Bors] - refactor: add an ofNat() elaborator

[eric-wieser]

ofNat(n) is a shorthand for no_index (OfNat.ofNat n).

Its purpose is:

• To make it easier to remember to write the no_index
• To add a place to put a hoverable docstrings explaining the complexities
• To make it easier to remove the no_indexes in future if DiscrTrees stops needing them around ofNat (DiscrTree doesn't match lemmas with OfNat.ofNat * to nat literal keys leanprover/lean4#2867).

This is not exhaustive, but is a step in the right direction.
For now, I only target (some of) the declarations with a See note [no_index around OfNat.ofNat].

Some theorem statements have been corrected in passing.

This exposed two Lean bugs relating to not using Expr.consumeMData:

• fix: ignore no_index around OfNat.ofNat in norm_cast leanprover/lean4#6438
• Int.reduceNeg simproc produces invalid proofs leanprover/lean4#6467

These are made more likely by this PR adding no_index to the RHS of equalities, but were already possible to trigger by using simp [<- _] on existing theorems with no_index on the LHS.

---

• depends on: [Merged by Bors] - chore: deprecate Nat.cast_eq_ofNat #20168

[github-actions]

PR summary 555c7f825c

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
There are 5066 files with changed transitive imports taking up over 214557 characters: this is too many to display!
You can run scripts/import_trans_difference.sh all locally to see the whole output.

---

Declarations diff

-++- ceil_ofNat
-++- floor_ofNat

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-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - chore: deprecate Nat.cast_eq_ofNat #20168
  By Dependent Issues (🤖). Happy coding!

[grunweg]

Thanks for doing this clean-up! The diff does what is says. Somebody who knows this corner of mathlib needs to judge if this change is good.

[grunweg]

So, this is one example of fixing a theorem statement, right (as a no_index is also put on the RHS), right?

[eric-wieser]

Arguably this doesn't change the statement, only the indexing of the statement. The corrections I was referring to in the description are the ones where a missing OfNat.ofNat is added.

[grunweg]

Flagging: this is a change of theorem statement.

[mattrobball]

bors delegate+

Consider whether you want to wait until the next version release to clean up some of the workarounds. If not, please make a cleanup PR after it lands and ping me.

Either way, please merge current master before adding to the queue. Thanks.

[mathlib-bors]

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

[eric-wieser]

Consider whether you want to wait until the next version release to clean up some of the workarounds.

I think there is going to be a long tail of workarounds as we propagate this and discover more missing consumeMDatas, so I don't think we should wait.

[leanprover-community-mathlib4-bot]

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

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded!

And happy new year! 🎉

• Build
• Lint style