perf: partially evaluate bv_decide simprocs to avoid instance synthesis

[hargoniX]

This PR avoids invoking TC synthesis and other inference mechanisms in the simprocs of bv_decide. This can give significant speedups on problems that pressure these simprocs.

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for 0d8df47 against 118160b are in! @hargoniX

Major changes (1)

• ✅ bv_decide_rewriter.lean//instructions: -831.8M (-4.4%)

Minor changes (2)

• ✅ bv_decide_realworld//instructions: -139.9M (-0.5%)
• 🟥 channel.lean//instructions: +1.2G (+3.2%)

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 118160bf07575337957e93232a31b9b1d1a7ac28 --onto 0708024c4649f11da1276d8b6d4345972a9dc57c. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-17 12:09:56)

[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 118160bf07575337957e93232a31b9b1d1a7ac28 --onto 0708024c4649f11da1276d8b6d4345972a9dc57c. You can force reference manual CI using the force-manual-ci label. (2025-12-17 12:09:58)