This PR improves the error messages produced by the `decide_cbv` tactic
by only reducing the left-hand side of the equality introduced by
`of_decide_eq_true`, rather than attempting to reduce both sides via
`cbvGoal`.
Previously, `evalDecideCbv` called `cbvGoalCore` which would try to
reduce both sides of `decide P = true` and leave a remaining goal on
failure, resulting in a generic error showing the mvar ID. Now, a
dedicated `cbvDecideGoal` function in `Cbv/Main.lean`:
- closes the goal immediately when the LHS reduces to `Bool.true`
- reports a clear error when the LHS reduces to `Bool.false`, telling
the user the proposition is false
- reports a clear error with the stuck expression when reduction cannot
complete
Co-authored-by: Claude Sonnet 4.5 <noreply@anthropic.com>
