feat: add E-matching diagnostics to grind

[leodemoura]

This PR adds the option grind.ematch.diagnostics, which tracks how E-matching theorem instances depend on each other. When enabled, grind records, for every new theorem instance, the set of previous instances whose generated terms participated in the match. This produces a hyper-graph {thm_1, ..., thm_n} => thm describing the provenance of each instantiation.

The hyper-graph is stored in Grind.Result so downstream tooling can inspect it. The trace class trace.grind.ematch.diagnostics.compact prints a compact textual view of the hyper-graph, restricted to constant-name origins. Example output:

  [grind.ematch.diagnostics.compact] ✅️ instances
    [inst] [] => th1
    [inst] [th1] => th3
    [inst] [th1] => th2
    [inst] [th2, th3] => th4
    [inst] [th4] => th5

The implementation stores an ematchDiagSource field on each ENode and threads a withEmatchDiagSource reader through fact assertion so that newly internalized terms inherit the origin of the instance that produced them. During E-matching, Choice collects the sources of every matched argument, and the resulting set becomes the predecessor set of the new instance.

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-04-24 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-04-28 21:54:10)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 9df737d49283c81413c7e000478ae5c6f5397f64 --onto 3fc99eef102549c743c6c63547983319bfae6f01. You can force reference manual CI using the force-manual-ci label. (2026-04-29 00:20:46)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-13558 has successfully built against this PR. (2026-04-28 22:51:14) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9df737d49283c81413c7e000478ae5c6f5397f64 --onto 3c6317b6d77a565b4217532d1190ac6955dba842. You can force Mathlib CI using the force-mathlib-ci label. (2026-04-29 00:20:45)