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

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.