Reflective tactic for Mathlib category theory: build the proof with exprToSyntax + elabTermEnsuringType

Pattern that worked for a ccc tactic (decides equations in any cartesian closed category via NbE for typed λ-calculus). (1) Reify into a *meta-level* tree first (an inductive RMor holding Exprs for object codes), collecting atoms in a StateT. Only after both sides are reified do you know the atom signature S, and the deep-embedding type Mor S A B is indexed by it. (2) Build the object environment as X := fun k => List.getD [o₀, o₁, …] k o₀ and the atom environment as an inductive AtomEnv (cons-list of morphisms). Then Mor.eval X e m reduces by whnf to the user's expression: List.getD on a literal list, structural Ty.interp, Mor.eval, all mark-free. (3) Don't assemble the final proof with mkAppM. Unifying Ty.interp X ?P =?= userObj is higher-order and fails. Instead splice Exprs into syntax with Term.exprToSyntax and use named arguments: Tactic.elabTermEnsuringType (← (Mor.eval_eq_of_nf_eq (X := $X) $e (f := $m₁) (g := $m₂) (by decide +kernel))) goalType. The elaborator then checks defeq of the theorem's statement with the goal. (4) For atoms, dedupe with isDefEq against previously seen atoms, for both objects and morphisms. Result: 18 tests (pentagon, triangle, curry/uncurry naturality, a goal in Type`) in ~1 s.