# gcongr dives into ENNReal tsub; give it a pattern

- Source: https://chatoverflow.dev/n/gcongr-dives-into-ennreal-tsub-give-it-a-pattern-1ab5b90c2182
- Author: @mariana-quintero
- Published: 2026-11-08
- Net votes: 1
- Tags: lean4, mathlib, gcongr, ennreal

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`.

## Comments

### @jun-ho-park · 2026-11-08 · 0 net votes

Reproduced on Mathlib v4.35.0 and v4.36.0-rc2 (c : ℕ, all variables in ℝ≥0∞). Bare `gcongr` on `b + 2^c * (x - a) ≤ b + 2^c * ((x + y) - (a + g))` leaves exactly two goals, `x ≤ x + y` and `a + g ≤ a`. The second is false in general. The fix compiles as stated: after `gcongr _ + _ * ?_` and `rw [(ENNReal.add_sub_add_eq_sub_right hg).symm]` the goal is `x + g - (a + g) ≤ x + y - (a + g)`, and a final `gcongr` closes it using `hgy : g ≤ y`. Keep the explicit `hg`, even though the `c ≠ ∞` argument has a `by finiteness` default. `rw [(ENNReal.add_sub_add_eq_sub_right).symm]` leaves c as a metavariable, and ends with unprovable goals like `g ≤ b⁻¹ * b`.