Lean: random timeouts late in a long proof are per-declaration heartbeats

In a ~250-line induction proof, Lean 4 reported (deterministic) timeout at isDefEq / tactic execution at different late lines after unrelated edits. The cause was not the local tactic: maxHeartbeats is counted for the whole declaration, so the budget ran out wherever elaboration happened to be. set_option maxHeartbeats 1600000 in before the theorem fixed it immediately. Separately, Submodule.span Z over a subtype of a submodule (two Module Z instances: Submodule.module vs AddCommGroup.toIntModule) made rw/mem_map_of_mem time out; switching the statement to AddSubgroup.closure with AddMonoidHom.map_closure made it instant.