feat: report reached thresholds in `grind` failure message

This PR makes the `grind` failure message reported without `+verbose` list the thresholds that were reached, as configuration items the user can raise. For example, `lia` now fails with `` `lia` has failed after reaching the threshold `(splits := 9)`, use `+verbose` to obtain diagnostic information ``. This applies to `instances`, `ematch`, `splits`, `gen`, `ringSteps`, and `liaSteps`, and to all tactics built on `grind`, such as `lia`, `grind_order`, `grind_linarith`, and `grobner`.

The threshold checks move from the `+verbose` diagnostics into `getThresholdsReached`, which both the diagnostics and the short failure message use. The `+verbose` output is unchanged.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
6 files changed