feat: add cbv at location syntax

[wkrozowski]

This PR adds at location syntax to the cbv tactic, matching the interface of simp at. Previously cbv could only reduce the goal target; now it supports cbv at h, cbv at h |-, and cbv at *.

cbvGoal is rewritten to use Sym.preprocessMVar followed by cbvCore within a single SymM context, sharing the term table across all hypotheses and the target. The old cbvGoalCore (which reduced one side of an equation goal at a time) is replaced by a general approach that reduces arbitrary goal types and hypothesis types, with special handling for True targets and False hypotheses. cbvDecideGoal is updated to use the extracted cbvCore as well.

🤖 Generated with Claude Code

[wkrozowski]

!bench

[leanprover-radar]

Benchmark results for 19bc692 against 03a5db3 are in! @wkrozowski

Warning

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

• Bench repo commit hashes for run build differ between commits.

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

Medium changes (1✅)

• ✅ elab/cbv_system_f//instructions: -7.5G (-5.23%)

Small changes (1✅, 2🟥)

• 🟥 build/module/Lean.Elab.Tactic.Cbv//instructions: +115.2M (+7.10%) (reduced significance based on *//lines)
• 🟥 build/module/Lean.Meta.Tactic.Cbv.Main//instructions: +224.5M (+3.76%) (reduced significance based on *//lines)
• ✅ compiled/const_fold//instructions: -18.2M (-0.21%)

[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 03a5db34c77db5266d21af56469ba43c9965d341 --onto cda84702e9b31165f1f83c657b532f36f34e0bd0. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-03 12:50:51)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1f04bf4fd13b62962f054513c2560ba66ae43366 --onto cda84702e9b31165f1f83c657b532f36f34e0bd0. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-03 16:09:32)

[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 03a5db34c77db5266d21af56469ba43c9965d341 --onto cda84702e9b31165f1f83c657b532f36f34e0bd0. You can force reference manual CI using the force-manual-ci label. (2026-03-03 12:50:52)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 1f04bf4fd13b62962f054513c2560ba66ae43366 --onto cda84702e9b31165f1f83c657b532f36f34e0bd0. You can force reference manual CI using the force-manual-ci label. (2026-03-03 16:09:34)

[wkrozowski]

!bench

[leanprover-radar]

Benchmark results for b46b95a against 1f04bf4 are in! @wkrozowski

• 🟥 build//instructions: +319.8M (+0.00%)

Medium changes (1✅)

• ✅ elab/cbv_system_f//instructions: -7.5G (-5.28%)

Small changes (2🟥)

• 🟥 build/module/Lean.Elab.Tactic.Cbv//instructions: +119.8M (+7.40%) (reduced significance based on *//lines)
• 🟥 build/module/Lean.Meta.Tactic.Cbv.Main//instructions: +225.3M (+3.77%) (reduced significance based on *//lines)