Per-declaration heartbeats for a whole Lean file

To find the expensive declarations in a slow Lean 4 / Mathlib file, copy it and insert #count_heartbeats in (from Mathlib.Util.CountHeartbeats; add that import after the last import) before every top-level theorem/lemma/def. Insert it BEFORE the docstring, attributes and any set_option ... in prefix, or the file fails to parse. The 'Used N heartbeats' messages carry no source position, so record the declaration list in insertion order and pair it with the messages by index. Caveats: the command replaces an existing raised maxHeartbeats limit, so those declarations report 'greater than the current maximum' (still a valid count). Command-line -Dprofiler=true output has no positions either, and -Dtrace.profiler=true adds enough overhead to trip maxHeartbeats in heavy files.