perf: simplify cbv ite/dite simprocs by reducing Decidable instance directly

[wkrozowski]

This PR changes the approach in simpIteCbv and simpDIteCbv, by replacing call to Decidable.decide
with reducing and direct pattern matching on the Decidable instance for isTrue/isFalse. This produces simpler proof terms.

[wkrozowski]

!bench

[leanprover-radar]

Benchmark results for 317a97c against f31f508 are in! @wkrozowski

• ✅ build//instructions: -2.1G (-0.02%)

Large changes (2✅)

• ✅ elab/cbv_decide//instructions: -23.8G (-27.27%)
• ✅ elab/cbv_merge_sort//instructions: -13.0G (-37.78%)

Medium changes (1🟥)

• 🟥 build/module/Lean.Meta.Tactic.Cbv.ControlFlow//bytes .olean.server: +2kiB (+46.69%)

Small changes (2✅, 1🟥)

• 🟥 build/module/Init.Sym.Lemmas//instructions: +42.2M (+2.21%)
• ✅ build/module/Lean.Meta.Tactic.Cbv.ControlFlow//bytes .olean.private: -50kiB (-10.43%)
• ✅ build/module/Lean.Meta.Tactic.Cbv.ControlFlow//instructions: -2.0G (-32.56%) (reduced significance based on *//lines)

[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 f31f50836d032d6c237272a3b2e733a92a3ee619 --onto ed0fd1e933239beaa7aaa12598f961c260062ab6. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-24 19:21:40)

[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 f31f50836d032d6c237272a3b2e733a92a3ee619 --onto 8038a8b8904f89ad9542c8eda11379f8f006eab1. You can force reference manual CI using the force-manual-ci label. (2026-02-24 19:21:42)