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

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.