feat: add sanity checks to `register_sym_simp` (#13040)

This PR adds validation to the `register_sym_simp` command:

- Reject duplicate variant names
- Validate `pre`/`post` syntax by elaborating them via `elabSymSimproc`
  in a minimal `GrindTacticM` context, catching unknown theorem names
  and unknown theorem set references at registration time

Adds `withGrindTacticM` helper for running `GrindTacticM` from
`CommandElabM`,
and `validateOptionSimprocSyntax` for optional syntax validation.

Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>