feat: add `grind_norm` for comparing the `simp`- and `Sym.simp`-based `grind` normalizers

This PR adds `grind_norm`, a debugging tactic for migrating the `grind` normalizer from `simp` to `Sym.simp`. `grind_norm` applies the current normalizer to the goal, `grind_norm sym` applies the `Sym.simp`-based one, and `grind_norm check` runs both and fails when the results differ. The tactic exists only to collect discrepancies between the two normalizers and will be deleted when the migration is complete.

The `Sym.simp`-based normalizer derives its theorem sets from `normExt`, so `[grind norm]`, `[grind unfold]`, and `init_grind_norm` are covered. Its `pre` chain is metadata erasure, beta, projection and matcher reduction, `zeta`/`zetaDelta`, negation pushing, `arith`, and the pre rewrite rules; its `post` chain is the post rewrite rules, ground evaluation, and ports of the `grind` simprocs (`simpEq`, `simpOr`, `simpDIte`, `reduceCtorEq`, `simpForall`, `simpExists`).

The definitional reduction steps used by `Sym.dsimp` move to the new `Lean.Meta.Sym.Reduce` module and are now shared by `Sym.dsimp`, `Sym.simp`, and the normalizer. `Sym.Simp.evalGround` evaluates `String` append.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>