feat: make bv_decide available in sym mode

[hargoniX]

This PR makes bv_decide available from within sym => mode.

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for 4d5f955 against 945e78b are in. There are significant results. @hargoniX

• 🟥 build//instructions: +12.2G (+0.11%)

Small changes (6✅, 51🟥)

• 🟥 build/module/Init.Control.Lawful.MonadAttach//instructions: +4.5M (+0.93%)
• 🟥 build/module/Init.Control.Lawful.MonadLift//instructions: +3.7M (+0.76%)
• 🟥 build/module/Init.Data.Array.QSort//instructions: +3.7M (+0.75%)
• 🟥 build/module/Init.Data.Array.Sort//instructions: +3.9M (+0.75%)
• 🟥 build/module/Init.Data.Array//instructions: +3.8M (+0.71%)
• 🟥 build/module/Init.Data.FloatArray//instructions: +4.7M (+0.90%)
• 🟥 build/module/Init.Data.Int.DivMod//instructions: +3.1M (+0.65%)
• 🟥 build/module/Init.Data.Iterators.Combinators.FlatMap//instructions: +4.0M (+0.62%)
• 🟥 build/module/Init.Data.Iterators.Combinators//instructions: +4.0M (+0.81%)
• 🟥 build/module/Init.Data.Iterators.Lemmas.Combinators.Monadic//instructions: +3.6M (+0.72%)
• 🟥 build/module/Init.Data.Iterators.Lemmas.Producers//instructions: +4.0M (+0.81%)
• 🟥 build/module/Init.Data.Iterators.Lemmas//instructions: +4.5M (+0.86%)
• 🟥 build/module/Init.Data.List.Int//instructions: +3.5M (+0.86%)
• 🟥 build/module/Init.Data.List.Scan//instructions: +3.3M (+0.66%)
• 🟥 build/module/Init.Data.List.Sort//instructions: +3.6M (+0.75%)
• 🟥 build/module/Init.Data.List.SplitOn//instructions: +3.7M (+0.78%)
• 🟥 build/module/Init.Data.Nat.Internal//instructions: +3.5M (+0.86%)
• 🟥 build/module/Init.Data.Nat.Power2//instructions: +3.6M (+0.76%)
• 🟥 build/module/Init.Data.Nat.Sqrt//instructions: +4.0M (+1.00%)
• 🟥 build/module/Init.Data.Nat//instructions: +4.4M (+0.85%)
• and 37 more

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-08-04 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-04 13:06:42)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-08-04 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-08-04 13:06:44)