Implement `grind_propagator` for downstream / mathlib use

The grind_propagator command is declared as syntax in src/Init/Grind/Propagator.lean:19, but there is no macro_rules and the comment says -- TODO: not implemented yet. Only builtin_grind_propagator is implemented, and it's intended for use inside lean4 core.

In practice this means downstream users (e.g. mathlib) currently have no working command-level way to register a grind propagator. Concretely:

1. grind_propagator — parses but has no elab; using it does nothing.
2. builtin_grind_propagator from a mathlib module-mode file — the macro emits a non-meta _regBuiltin._declare (via declareBuiltin) that references the propagator function. Under the new module system this either fails at compile time ("non-meta declaration cannot access meta declaration") or compiles but crashes the interpreter at module-load time with LEAN ASSERTION VIOLATION ... fn_body_tag(...) != fn_body_kind::Unreachable, because the propagator's IR body is Unreachable. The registration goes through but the propagator can't be invoked.
3. Calling registerBuiltinUpwardPropagator directly from an initialize block (passing the propagator function as an argument) — works, and is what we ended up doing.

We hit this writing a grind propagator on CategoryTheory.CategoryStruct.comp to normalize morphism composition without the Catalan-blowup of e-matching Category.assoc. The propagator + helpers live in Mathlib/CategoryTheory/Tactic/GrindCatNorm.lean (mathlib branch grind_cat_assoc).

Request: implement grind_propagator so it works from downstream module-mode files — likely as a macro_rules that expands to an initialize calling registerBuiltinUpwardPropagator / registerBuiltinDownwardPropagator, rather than going through declareBuiltin. If the "builtin"/"non-builtin" distinction is meant to remain meaningful, the docstring should also explain which form mathlib-style downstream code should use.

cc @leodemoura

Start in src/Init/Grind/Propagator.lean at the grind_propagator syntax and compare it with builtin_grind_propagator. Use Mathlib/CategoryTheory/Tactic/GrindCatNorm.lean and its initialize-based registration as the downstream example. Done means a propagator registers and can be invoked from a downstream module-mode file, with the builtin distinction documented if it remains relevant.