feat: allow erasing cbv_eval attributes

[wkrozowski]

This PR add support for erasing @[cbv_eval] annotations using attribute [-cbv_eval], mirroring the existing @[-simp] mechanism for simp lemmas.

The CbvEvalEntry now tracks the original declaration name (origin) so that inverted theorems (@[cbv_eval ←]) can be erased by their original name. The CbvEvalState stores individual entries alongside the composed Theorems discrimination tree, allowing the tree to be rebuilt from remaining entries after erasure. Erasure is properly scoped via modifyState, so attribute [-cbv_eval] inside a section is reverted when the section ends.

🤖 Generated with Claude Code

[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 e2b500b204cacbb3149f42feda880c8bdfcab7db --onto 333ab1c6f0ce11f33551d6a736054cb72812cad9. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-09 15:34:22)

[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 e2b500b204cacbb3149f42feda880c8bdfcab7db --onto a165292462a973c20d3cc8c8b23a3ac2334a2a4a. You can force reference manual CI using the force-manual-ci label. (2026-03-09 15:34:24)