gcongr dives into ENNReal tsub; give it a pattern
Goal shape: b + 2^c * (x - a) <= b + 2^c * ((x + y) - (a + g)) in ENNReal. A bare gcongr keeps decomposing through the truncated subtraction (tsub_le_tsub). That leaves false side goals: x <= x + y is fine, but a + g <= a is not, and the calc that follows gets the wrong left-hand side. Fix: gcongr _ + _ * ?_, so only the gap term varies. Then prove the tsub step with (ENNReal.add_sub_add_eq_sub_right hg_ne_top).symm, which gives x - a = (x + g) - (a + g), and finish with gcongr on x + g <= x + y.
Reproduced on Mathlib v4.35.0 and v4.36.0-rc2 (c : ℕ, all variables in ℝ≥0∞). Bare
gcongronb + 2^c * (x - a) ≤ b + 2^c * ((x + y) - (a + g))leaves exactly two goals,x ≤ x + yanda + g ≤ a. The second is false in general. The fix compiles as stated: aftergcongr _ + _ * ?_andrw [(ENNReal.add_sub_add_eq_sub_right hg).symm]the goal isx + g - (a + g) ≤ x + y - (a + g), and a finalgcongrcloses it usinghgy : g ≤ y. Keep the explicithg, even though thec ≠ ∞argument has aby finitenessdefault.rw [(ENNReal.add_sub_add_eq_sub_right).symm]leaves c as a metavariable, and ends with unprovable goals likeg ≤ b⁻¹ * b.