feat: shorten `grind` failure message without `+verbose` (#16073)

This PR shortens the error message reported when `grind` fails without
`+verbose`. Instead of printing the failing goal, the message is now ``
`<tactic>` has failed, use `+verbose` to obtain diagnostic information
``, where `<tactic>` is the tactic the user invoked (e.g., `lia`,
`grind_order`, `grind_linarith`, `grobner`, `sym`) rather than always
`grind`. With `+verbose`, the goal and diagnostics are still reported,
and the header also names the invoked tactic.

`Grind.Result` now records the `identity` of the tactic running `grind`,
and the new `Result.toErrorMessageData` builds the failure message.
`finish`, `finish?`, and `grind?` pass their own names. The `unsolved
goals` error reported by `done` in interactive `grind => …` mode is
unchanged and still prints the remaining goals.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>