fix: record grind solver steps that make progress in generated scripts

This PR fixes `grind?` and `finish?` dropping solver steps such as `ring` and `lia` that make progress without closing the goal or propagating facts. Later steps may depend on that progress, so the generated script failed to replay, and `grind?` also dropped theorems from its `grind only` suggestions.

Such a step is now kept whenever the rest of the script cannot close the goal without it, using the check already applied to steps that propagate facts. This replays the rest of the script once per progress step, which makes `grind?` and `finish?` slower on large proofs.

Closes #16028
Closes #16029

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