feat(CategoryTheory): add a grind propagator that normalizes morphism composition

[kim-em]

This PR adds a grind upward propagator on CategoryTheory.CategoryStruct.comp that, every time grind internalizes a composition f ≫ g, pushes the equality f ≫ g = (right-associated form with syntactic identity factors removed) back into the e-graph.

The motivation is the Catalan blow-up of e-matching on Category.assoc: a chain of length n lets e-matching generate all Catalan(n − 1) parenthesizations as e-graph terms. Mathlib already has the runaway documented at Mathlib/CategoryTheory/Iso.lean:146. The propagator commits to a single canonical representative per fresh composition; the normalized form is a fixed point, so it never re-fires on the form it produces — the e-graph grows by O(1) terms per user-visible composition instead of Catalan-many.

Notes:

• The @[grind =] / @[grind _=_] attributes are removed from Category.id_comp, Category.comp_id, Category.assoc because the propagator subsumes them and they would re-introduce the blow-up.
• uliftCategory in Category/Basic.lean now provides its three category axioms explicitly, since the cat_disch autoparam used to rely on the e-matching tags above and Category/Basic.lean runs before the propagator file is loaded.
• The propagator is registered via initialize calling registerBuiltinUpwardPropagator directly. The builtin_grind_propagator macro can't be used downstream in module-mode mathlib (see Implement grind_propagator for downstream / mathlib use leanprover/lean4#13805) and grind_propagator (the user-facing form) is not yet implemented in lean4.
• The normalizer is hand-written rather than reusing Meta.Simp.main, which has no IR body and crashes the interpreter when invoked from a module-mode downstream file.

Tests in MathlibTest/CategoryTheory/GrindCatNorm.lean cover associativity, identity removal, mixed cases, hypotheses flowing through the normalizer, reducible-alias morphism types, and a long-chain heart-beat guard.

Filed upstream tracking issue: leanprover/lean4#13805

🤖 Prepared with Claude Code

[github-actions]

PR summary 998032a1c1

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Tactic.GrindCatNorm (new file)	273

---

Declarations diff

+ MorAlias
+ catCompPropagatorImpl

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.