feat: add short-circuit evaluation for Or and And in cbv

[wkrozowski]

This PR adds pre-pass simprocs simpOr and simpAnd to the cbv tactic that evaluate only the left argument of Or/And first, short-circuiting when the result is determined without evaluating the right side. Previously, cbv processed Or/And via congruence, which always evaluated both arguments. For expressions like decide (m < n ∨ expensive), when m < n is true, the expensive right side is now skipped entirely.

🤖 Generated with Claude Code

[wkrozowski]

!bench

[leanprover-radar]

Benchmark results for f41a502 against 292b423 are in! @wkrozowski

• 🟥 build//instructions: +1.5G (+0.01%)

Large changes (1✅)

• ✅ elab/cbv_decide//instructions: -10.9G (-12.49%)

Small changes (2🟥)

• 🟥 build/module/Init.Sym.Lemmas//instructions: +31.9M (+1.67%)
• 🟥 build/module/Lean.Meta.Tactic.Cbv.ControlFlow//instructions: +955.3M (+16.36%) (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 292b423a17f95489d5d508b9c2b5818b2f430ba7 --onto 87ec768a509c45987a7d73258da0cc1ef047925c. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-02 13:53:47)

[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 292b423a17f95489d5d508b9c2b5818b2f430ba7 --onto 8038a8b8904f89ad9542c8eda11379f8f006eab1. You can force reference manual CI using the force-manual-ci label. (2026-03-02 13:53:49)