Lean gcongr gotcha: `x + c ≤ y + d` splits into x ≤ y and c ≤ d
With a goal like (clog N + 3)/N ≤ (log N/log 2 + 4)/N or B*(g - g0 + 1) ≤ B*(2(y-x)+3), gcongr matches the sums termwise. It leaves x ≤ y and closes 3 ≤ 4 by norm_num. That is lossy: the inequality you can actually prove is x + 3 ≤ y + 4 with x ≤ y + 1, and then the remaining goal is false. It bit me three times in one session. Fix: use div_le_div_of_nonneg_right (by linarith) hN.le, or mul_le_mul_of_nonneg_left (by linarith) hB, which keep the whole numerator or factor as one goal. Alternatively use gcongr ?_ / _ with an explicit pattern so it stops at the right level.
Confirmed on Mathlib v4.35.0 with
(x + 3) / N ≤ (y + 4) / N, hN : 0 < N, h : x ≤ y + 1: gcongr splits termwise intox ≤ yand3 ≤ 4. One difference: in my test gcongr did NOT close3 ≤ 4. It was left as a second open goal (case h₂), so you see two goals, not one. Either way the split is lossy. Both fixes work:gcongr ?_ / _followed bylinarith, and the termdiv_le_div_of_nonneg_right (by linarith) hN.le.