perf: construct IntModule.OfNatModule.Q type manually

[leodemoura]

This PR optimizes the construction of the grind-relevant instances for the auxiliary grind type IntModule.OfNatModule.Q. It was a major bottleneck in Mathlib.

[leanprover-bot]

Reference manual CI status:

• ✅ Reference manual branch lean-pr-testing-14346 has successfully built against this PR. (2026-07-09 19:53:41) View Log
• 🟡 Reference manual branch lean-pr-testing-14346 build against this PR didn't complete normally. (2026-07-09 19:54:54) View Log

[cognivore]

🥳

[hargoniX]

!bench mathlib

[leanprover-radar]

Benchmark results for leanprover-community/mathlib4-nightly-testing@c3e2c88 against leanprover-community/mathlib4-nightly-testing@55b60c6 are in. There are significant results. @hargoniX

Warning

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

• Bench repo commit hashes for run main differ between commits.

• ✅ build//instructions: -109.3G (-0.07%)

Medium changes (13✅)

• ✅ build/module/Mathlib.Algebra.Polynomial.RuleOfSigns//instructions: -7.6G (-10.75%)
• ✅ build/module/Mathlib.Analysis.Calculus.LHopital//instructions: -7.6G (-21.59%)
• ✅ build/module/Mathlib.Analysis.Calculus.Taylor//instructions: -7.4G (-11.01%)
• ✅ build/module/Mathlib.Analysis.Normed.Lp.Finsupp//instructions: -4.0G (-24.78%)
• ✅ build/module/Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation//instructions: -8.9G (-6.60%)
• ✅ build/module/Mathlib.Data.Nat.Factorization.Divisors//instructions: -2.1G (-21.69%)
• ✅ build/module/Mathlib.MeasureTheory.Measure.Prokhorov//instructions: -4.8G (-8.09%)
• ✅ build/module/Mathlib.MeasureTheory.VectorMeasure.Variation.Basic//instructions: -6.3G (-14.22%)
• ✅ build/module/Mathlib.MeasureTheory.VectorMeasure.WithDensityVec//instructions: -5.8G (-8.38%)
• ✅ build/module/Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula//instructions: -4.4G (-10.55%)
• ✅ build/module/Mathlib.RingTheory.MvPowerSeries.GaussNorm//instructions: -4.0G (-10.42%)
• ✅ build/module/Mathlib.RingTheory.MvPowerSeries.Trunc//instructions: -9.1G (-24.57%)
• ✅ build/module/Mathlib.Topology.EMetricSpace.BoundedVariation//instructions: -10.7G (-9.84%)

Small changes (49✅)

Too many entries to display here. View the full report on radar instead.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-14346 has successfully built against this PR. (2026-07-09 20:48:42) View Log