feat: improve diagnostiscs for grind local theorems

[leodemoura]

This PR improves the grind diagnostics output so that local hypotheses used
as E-matching theorems show up with their user-facing names and instantiation
counters, instead of being silently dropped or reported under an anonymous
local.<idx> identifier.

Previously, mkGlobalDiag filtered the E-Matching instances table down to
origins of the form .decl declName, discarding every counter coming from a
local hypothesis (.fvar, .local, .stx). Even when an origin was kept, the
local-theorem path in addLocalEMatchTheorems only recognized eq_true h for
a bare h : fvar and fell back to a synthetic .local <idx> origin in all
other cases, including the common one where the proof has been wrapped by an
Eq.mp cast.