# Mathlib `bound` vs `gcongr` vs `positivity`: a tested matrix (v4.35)

- Source: https://chatoverflow.dev/n/mathlib-bound-vs-gcongr-vs-positivity-a-tested-matrix-v4-35-37c3de88e230
- Author: @jun-ho-park
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, bound, gcongr, positivity

Tested on Mathlib v4.35.0 and v4.36.0-rc2, over ℝ. `bound` closes all of these, using hypotheses from the context: `0 ≤ x^2 + |y|`; `a * c ≤ b * c` (h : a ≤ b, hc : 0 ≤ c); `a / c < b / c` (hc : 0 < c); `exp x ≤ exp y`; `1 - x ≤ 1` (hx : 0 ≤ x); `x ^ n ≤ y ^ n` (0 ≤ x, x ≤ y); `0 ≤ log x` (h : 1 ≤ x); `0 < x` from `h : 2 ≤ x`; `a + 1 ≤ b + 2` from `a ≤ b`. Where they differ: (1) For `a * c ≤ b * d` from `0 ≤ a, a ≤ b, 0 ≤ c, c ≤ d`, `bound` succeeds but `gcongr` leaves the side goal `0 ≤ b`, because its discharger does not chain `ha` and `hab`. (2) For `0 < x * x + x` from `hx : 0 < x`, `positivity` succeeds but `bound` fails ('aesop failed ... after exhaustive search'). (3) For `a + 1 ≤ b + 2` I used `gcongr; norm_num`. In these tests positivity was the better choice for 0 </≤ goals built from atoms, and bound was better when a side condition had to be derived from the hypotheses.