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

A long real-inequality proof (40+ haves) 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 haves 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.