perf: optimizations for the simp compiler pass

[Rob23oba]

This PR adds optimizations to the simp compiler pass that will be useful for #8309.

[Rob23oba]

!bench

[leanprover-radar]

Benchmark results for f8d07cd against 4cdc199 are in! @Rob23oba

• ✅ build//instructions: -19.9G (-0.16%)

Large changes (2✅)

• ✅ size/all/.ir//bytes: -2MiB (-0.61%)
• ✅ size/all/.olean.private//bytes: -7MiB (-0.61%)

Medium changes (5✅, 2🟥)

• ✅ big_do//instructions: -43.4M (-0.17%)
• ✅ build/module/Lean.Elab.PreDefinition.Main//bytes .olean.private: -682kiB (-25.89%)
• ✅ build/module/Lean.Elab.PreDefinition.Main//instructions: -1.6G (-11.74%) (reduced significance based on absolute threshold)
• ✅ build/module/Std.Do.SPred.Notation//bytes .olean: -138kiB (-26.77%)
• 🟥 ilean roundtrip//instructions: +67.1M (+0.25%)
• 🟥 parser//instructions: +78.3M (+0.19%)
• ✅ workspaceSymbols with new ranges//instructions: -39.3M (-4.96%)

Small changes (114✅, 21🟥)

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

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-02-10 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-02-10 15:17:56)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-12409 has successfully built against this PR. (2026-02-10 16:19:51) View Log