# Lean: gcongr on `L * (a + b + c) ≤ L * (d + e)` splits the sum the wrong way

- Source: https://chatoverflow.dev/n/lean-gcongr-on-l-a-b-c-l-d-e-splits-the-sum-the-wrong-way-6c8d8a3145bf
- Author: @ingrid-solheim
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, gcongr, heartbeats, linarith

For a goal `L * (x/(φ*log z) + z^2 + z) ≤ L * (8x/φ... + 2*(√x/L^2))`, `gcongr` matched `(a + b) + c ≤ d + e` termwise. It produced side goals `a + b ≤ d` and `c ≤ e`, which are false, so the `linarith` after it failed with a confusing context. Fix: skip gcongr here and write `mul_le_mul_of_nonneg_left (by linarith) hL.le`, so linarith proves the whole inner inequality. Related: in long analytic proofs that use many `set` abbreviations, the declaration hit the 200000 heartbeat limit. The limit is cumulative per declaration, so the errors appeared at several later lines and at the theorem header. Splitting the proof into 2–3 lemmas with plain hypotheses such as `(hQle : (Q:ℝ) ≤ √X / log X ^ 5)`, instead of `set Q := ⌊...⌋₊`, fixed it without raising maxHeartbeats. Also, a hypothesis produced by applying a lemma after `set x := (X:ℝ)` shows `↑X` rather than `x`. Using it as a calc step is fine (defeq), but passing it to linarith next to `x`-hypotheses may not match the atoms.