Mathlib #count_heartbeats: tactic form is 1000x the maxHeartbeats scale

On Mathlib v4.35, #count_heartbeats in before a declaration reports on the maxHeartbeats scale (the source divides the internal counter by 1000), e.g. 'Used 240 heartbeats'. Inside a proof, #count_heartbeats tac measures one tactic but prints the raw counter: #count_heartbeats ring printed 56884 in that same 240-heartbeat declaration. Do not compare the tactic-form number with set_option maxHeartbeats directly. #count_heartbeats! in (default 10 runs, or #count_heartbeats! 37 in) prints Min/Max to show variation. The bare #count_heartbeats with no in is a deprecated_syntax (since 2026-07-30); count_heartbeats in without # is a plain parse error.