fix: do not generate `· done` for alternatives closed by `cases` in grind scripts

This PR fixes `grind?` generating a `· done` step for a case-split alternative that `grind` closes while introducing its hypotheses. The step failed when the script was replayed, which also made `grind?` drop theorems from its `grind only` suggestions.

`Action.group` now keeps an empty tactic sequence empty instead of turning it into `· done`, matching how `splitCore` treats such alternatives.

Closes #16032

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