perf: inline assorted declarations used in match_expr

[hargoniX]

blocked on #9929

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for 1ed80e9 against 8c82f9e are in. There are significant results. @hargoniX

• 🟥 build//instructions: +36.8G (+0.32%)

Large changes (1🟥)

• 🟥 build/module/Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Simproc//instructions: +5.1G (+18.08%)

Medium changes (5🟥)

• 🟥 build/module/Lean.Elab.Tactic.Do.Internal.VCGen.Solve//instructions: +1.5G (+11.51%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Elab.Tactic.Omega.Frontend//instructions: +3.3G (+9.70%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Meta.Tactic.FunInd//instructions: +3.0G (+4.91%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Meta.Tactic.Grind.EMatch//instructions: +1.3G (+2.56%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Meta.Tactic.Grind.Ext//instructions: +1.2G (+15.57%) (reduced significance based on absolute threshold)

Small changes (1✅, 94🟥)

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

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 8c82f9ed4ae09b165342b24a6461ccc097caae50 --onto c04a83a2e5d5718032819f2d124f2c949fab292f. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-12 16:12:46)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 8c82f9ed4ae09b165342b24a6461ccc097caae50 --onto ed0d50fcf0efa8c9a32e1ccb3603ce43edce6926. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-13 13:35:59)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 8c82f9ed4ae09b165342b24a6461ccc097caae50 --onto c04a83a2e5d5718032819f2d124f2c949fab292f. You can force reference manual CI using the force-manual-ci label. (2026-05-12 16:12:48)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 8c82f9ed4ae09b165342b24a6461ccc097caae50 --onto ed0d50fcf0efa8c9a32e1ccb3603ce43edce6926. You can force reference manual CI using the force-manual-ci label. (2026-05-13 13:36:00)