chore: make map_ofNat a simp lemma

[eric-wieser]

---

[github-actions]

PR summary 28e92f2640

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

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]

!bench

[leanprover-bot]

Here are the benchmark results for commit 28e92f2.
There were significant changes against commit b0890aa:

  Benchmark                                   Metric         Change
  =================================================================
- ~Mathlib.Algebra.Category.ModuleCat.Basic   instructions    49.8%

[github-actions]

File	Instructions	%
build	+379.947⬝10⁹	(+0.27%)
lint	+88.80⬝10⁹	(+1.22%)
Mathlib.Algebra.Category.ModuleCat.Basic	+25.494⬝10⁹	(+49.83%)

3 files, Instructions +3.0⬝10⁹

File	Instructions	%
Mathlib.RingTheory.Smooth.Kaehler	+3.569⬝10⁹	(+1.53%)
Mathlib.FieldTheory.AxGrothendieck	+3.533⬝10⁹	(+5.80%)
Mathlib.RingTheory.Kaehler.Basic	+3.410⬝10⁹	(+0.95%)

12 files, Instructions +2.0⬝10⁹

File	Instructions	%
Mathlib.RingTheory.TensorProduct.Basic	+2.980⬝10⁹	(+1.01%)
Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf	+2.905⬝10⁹	(+4.11%)
Mathlib.RingTheory.AdicCompletion.AsTensorProduct	+2.859⬝10⁹	(+1.45%)
Mathlib.Analysis.NormedSpace.Multilinear.Basic	+2.728⬝10⁹	(+0.98%)
Mathlib.LinearAlgebra.Dual	+2.375⬝10⁹	(+0.54%)
Mathlib.NumberTheory.ArithmeticFunction	+2.213⬝10⁹	(+2.84%)
Mathlib.AlgebraicGeometry.Spec	+2.182⬝10⁹	(+2.30%)
Mathlib.RingTheory.Flat.FaithfullyFlat	+2.134⬝10⁹	(+2.77%)
Mathlib.Condensed.Discrete.LocallyConstant	+2.69⬝10⁹	(+2.90%)
Mathlib.RingTheory.Kaehler.TensorProduct	+2.38⬝10⁹	(+1.07%)
Mathlib.RingTheory.Flat.Equalizer	+2.35⬝10⁹	(+0.91%)
Mathlib.Algebra.Exact	+2.20⬝10⁹	(+2.96%)

57 files, Instructions +1.0⬝10⁹

File	Instructions	%
Mathlib.RingTheory.Unramified.Finite	+1.950⬝10⁹	(+2.11%)
Mathlib.Algebra.Polynomial.Module.AEval	+1.948⬝10⁹	(+2.15%)
Mathlib.Algebra.Lie.Weights.Basic	+1.869⬝10⁹	(+1.44%)
Mathlib.Analysis.InnerProductSpace.Projection	+1.867⬝10⁹	(+0.91%)
Mathlib.Topology.Algebra.Module.Basic	+1.849⬝10⁹	(+0.76%)
Mathlib.Analysis.Calculus.Deriv.Mul	+1.842⬝10⁹	(+1.56%)
Mathlib.LinearAlgebra.Multilinear.Basic	+1.824⬝10⁹	(+1.51%)
Mathlib.Algebra.Category.ModuleCat.Colimits	+1.809⬝10⁹	(+9.22%)
Mathlib.RingTheory.Kaehler.CotangentComplex	+1.747⬝10⁹	(+0.63%)
Mathlib.LinearAlgebra.PiTensorProduct	+1.723⬝10⁹	(+1.18%)
Mathlib.Condensed.Light.TopCatAdjunction	+1.717⬝10⁹	(+7.92%)
Mathlib.Topology.Homotopy.Path	+1.712⬝10⁹	(+4.04%)
Mathlib.LinearAlgebra.Matrix.ToLin	+1.712⬝10⁹	(+1.26%)
Mathlib.GroupTheory.HNNExtension	+1.690⬝10⁹	(+1.58%)
Mathlib.Analysis.Calculus.FDeriv.Mul	+1.587⬝10⁹	(+0.42%)
Mathlib.Analysis.RCLike.Basic	+1.584⬝10⁹	(+1.31%)
Mathlib.RingTheory.MatrixAlgebra	+1.546⬝10⁹	(+5.44%)
Mathlib.Topology.Connected.PathConnected	+1.537⬝10⁹	(+2.55%)
Mathlib.Condensed.TopCatAdjunction	+1.531⬝10⁹	(+8.03%)
Mathlib.Algebra.Lie.TraceForm	+1.524⬝10⁹	(+0.81%)
Mathlib.Analysis.InnerProductSpace.TwoDim	+1.521⬝10⁹	(+1.06%)
Mathlib.LinearAlgebra.DirectSum.Finsupp	+1.502⬝10⁹	(+2.99%)
Mathlib.Analysis.InnerProductSpace.PiL2	+1.490⬝10⁹	(+0.81%)
Mathlib.GroupTheory.Perm.Fin	+1.480⬝10⁹	(+10.17%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique	+1.480⬝10⁹	(+0.70%)
Mathlib.RingTheory.WittVector.Basic	+1.458⬝10⁹	(+3.10%)
Mathlib.Algebra.Lie.Weights.Killing	+1.434⬝10⁹	(+0.69%)
Mathlib.RingTheory.Localization.BaseChange	+1.401⬝10⁹	(+3.32%)
Mathlib.Algebra.Category.Ring.Colimits	+1.376⬝10⁹	(+4.43%)
Mathlib.Algebra.MvPolynomial.Basic	+1.362⬝10⁹	(+1.41%)
Mathlib.GroupTheory.ArchimedeanDensely	+1.352⬝10⁹	(+2.23%)
Mathlib.Algebra.Category.ModuleCat.Presheaf	+1.330⬝10⁹	(+0.50%)
Mathlib.LinearAlgebra.FreeProduct.Basic	+1.326⬝10⁹	(+2.83%)
Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation	+1.268⬝10⁹	(+1.88%)
Mathlib.Analysis.Calculus.FDeriv.Analytic	+1.264⬝10⁹	(+0.49%)
Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear	+1.258⬝10⁹	(+3.79%)
Mathlib.NumberTheory.Bernoulli	+1.249⬝10⁹	(+2.00%)
Mathlib.LinearAlgebra.RootSystem.Hom	+1.239⬝10⁹	(+1.30%)
Mathlib.LinearAlgebra.Prod	+1.209⬝10⁹	(+1.50%)
Mathlib.RingTheory.Derivation.Basic	+1.152⬝10⁹	(+1.34%)
Mathlib.LinearAlgebra.TensorProduct.Basis	+1.139⬝10⁹	(+3.61%)
Mathlib.Algebra.Module.CharacterModule	+1.115⬝10⁹	(+1.96%)
Mathlib.FieldTheory.RatFunc.Basic	+1.108⬝10⁹	(+0.47%)
Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries	+1.102⬝10⁹	(+1.06%)
Mathlib.RingTheory.Kaehler.Polynomial	+1.99⬝10⁹	(+0.78%)
Mathlib.Analysis.InnerProductSpace.JointEigenspace	+1.71⬝10⁹	(+4.96%)
Mathlib.Data.Finsupp.Basic	+1.57⬝10⁹	(+1.61%)
Mathlib.Topology.Algebra.Module.Alternating.Basic	+1.54⬝10⁹	(+1.83%)
Mathlib.RingTheory.IntegralClosure.IntegralRestrict	+1.46⬝10⁹	(+0.44%)
Mathlib.LinearAlgebra.Basis.Defs	+1.34⬝10⁹	(+1.66%)
Mathlib.Probability.Kernel.MeasureCompProd	+1.32⬝10⁹	(+6.87%)
Mathlib.Algebra.MvPolynomial.Equiv	+1.31⬝10⁹	(+2.47%)
Mathlib.LinearAlgebra.TensorProduct.DirectLimit	+1.29⬝10⁹	(+2.14%)
Mathlib.Algebra.MonoidAlgebra.Basic	+1.27⬝10⁹	(+2.17%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric	+1.26⬝10⁹	(+0.58%)
Mathlib.LinearAlgebra.CliffordAlgebra.Equivs	+1.25⬝10⁹	(+1.31%)
Mathlib.Algebra.Polynomial.Derivation	+1.14⬝10⁹	(+4.76%)

[kim-em]

What is this lemma meant to index on? It's discrimination tree key must be terrible.

[eric-wieser]

Ideally it would index on OfNat.ofNat; but I'm aware that's not currently how indexing works. I'll make a new PR adding a comment explaining why this is not a simp lemma.

[eric-wieser]

Done in #19410

[kim-em]

If I understand correctly this should be closed now. Please reopen if that's incorrect.