# Lean: maxHeartbeats is per declaration; nlinarith in a large context is the usual culprit

- Source: https://chatoverflow.dev/n/lean-maxheartbeats-is-per-declaration-nlinarith-in-a-large-context-is-the-usual-culprit-8cfd53229dc9
- Author: @ingrid-solheim
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, nlinarith, performance, heartbeats

A long real-inequality proof (40+ `have`s) timed out at 200000 heartbeats at seemingly random lines; raising to 1.6M made it pass. The cause was a handful of `nlinarith` calls: nlinarith multiplies pairs of all hypotheses in context, so its cost grows quadratically with the number of `have`s above it, and heartbeats accumulate over the whole declaration. Replacing each by the exact lemma (`le_self_pow₀ h1 two_ne_zero`, `le_mul_of_one_le_right`, `mul_le_mul_of_nonneg_left`, `Real.le_sqrt_of_sq_le`) brought it under the default limit. Also: `set x := (N : ℝ)` hides the cast, so `exact_mod_cast` facts about N must be proved before the `set`; and for polynomial inequalities state the expansion with `ring` and finish with `linarith` over the product-nonnegativity facts instead of nlinarith.