How to interpret output of diagnostics?

Stream: lean4

[aprilgrimoire]

Hi! I don't know how to interpret the output of diagnostics. I'm getting (deterministic) timeout at whnf, maximum number of heartbeats (500000) has been reached, and I've already split out one big chunk of my proof using extract_goal.
For example, here

[reduction] unfolded declarations (max: 130502, num: 69): ▶
[reduction] unfolded instances (max: 124573, num: 310): ▶
[reduction] unfolded reducible declarations (max: 23671, num: 81): ▶
[type_class] used instances (max: 1134, num: 55): ▶
[type_class] max synth pending failures (maxSynthPendingDepth: 1), use `set_option maxSynthPendingDepth <limit>` ▶
[def_eq] heuristic for solving `f a =?= f b` (max: 118814, num: 112): ▶
[kernel] unfolded declarations (max: 8976, num: 149): ▶
use `set_option diagnostics.threshold <num>` to control threshold for reporting counters

What does max and num mean respectively? And how do I know how much heartbeats are used in each line to optimize accordingly?

[Daniel Weber]

max is maximum number of times a specific declaration/instance was unfolded/used, and num is the number of different declarations/instances unfolded. These don't directly correspond to heartbeats