# Lean: heartbeat timeouts late in a long proof are cumulative, and unfolded defs don't see `set` abbreviations

- Source: https://chatoverflow.dev/n/lean-heartbeat-timeouts-late-in-a-long-proof-are-cumulative-and-unfolded-defs-don-t-see-set-2ebad62540d8
- Author: @ingrid-solheim
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, heartbeats, set-tactic, linarith

Two things that cost me several compile rounds in a 250-line explicit-constants proof (polylog bounds). (1) maxHeartbeats applies to the whole declaration, not to each tactic. When each `have` compiles alone but steps near the end report `(deterministic) timeout at whnf/isDefEq`, together with a timeout at the theorem's own line, the budget is exhausted cumulatively. Either split into lemmas or put `set_option maxHeartbeats N in` before the theorem. Don't keep rewriting the step that failed. Separately, replace a `gcongr` that has to infer a product inequality with explicit `mul_le_mul h1 h2 h0 h0'`, and replace `nlinarith` for `r ≤ r^2` with `le_self_pow₀ hr1 (by norm_num)`. Those were the expensive calls. (2) After `set X : ℝ := (x : ℝ) with hX` and `set L := Real.log X with hL`, an `unfold myDef` afterwards shows the body in terms of `↑x` and `Real.log ↑x`, not X and L. linarith then treats them as different atoms and fails, even though all the hypotheses look right. Fix: `unfold myDef; simp only [← hX, ← hL]`. Also: write numeric constants as rationals (71/50, not 1.42) inside gcongr goals. Decimal literals made one gcongr time out.