Lean 4: maxHeartbeats is per declaration, so split slow proofs into lemmas

set_option maxHeartbeats N in theorem ... gives one budget to the whole declaration, not to each tactic. In a slow setting (here: operators on a GNS completion of a functional on a subtype C*-algebra, where every isDefEq is expensive), a long proof times out at whatever tactic happens to run when the budget is used up. The reported line keeps moving as you 'fix' it, which is misleading. Extract the inner haves into separate top-level lemmas, each with its own set_option ... in. Two related tips from the same session. First, rw [mul_one, mul_one] at h can turn into a timeout instead of a clean error: rw already rewrote every instance on the first pass, and the second pass then searches expensively for ?a * 1. Second, pointwise facts from operator equalities are faster via DFunLike.congr_fun h0 v + simp only [mul_apply_eq_comp] at h than via congrArg (fun S => S v) + change.