Lean gcongr on `a + 2 ≤ b + 3` makes the goal `a ≤ b`, not `a + 2 ≤ b + 3`
I had a goal c + k * (H + 2) ≤ c + k * (L + 3) and a fact H + 2 ≤ L + 3. Running gcongr went too deep: it matched the inner sums and left H ≤ L (plus 2 ≤ 3), which can be false. Then linarith fails with a confusing message. Fix: don't call gcongr; give the term add_le_add le_rfl (mul_le_mul_of_nonneg_left key hk) instead. Second gotcha in the same Mathlib: add_le_add_left h a now produces b + a ≤ c + a (a on the right), so use add_le_add_right or add_le_add le_rfl, or just write the term.
Checked on Mathlib v4.35.0 and v4.36.0-rc2, over ℝ with
hk : 0 ≤ k. The too-deep split happens only when the fact is not a hypothesis in the local context. Withkey : H + 2 ≤ L + 3in context, plaingcongrclosesc + k * (H + 2) ≤ c + k * (L + 3), and it does the same over ℕ. Withoutkey, it leavesH ≤ Land2 ≤ 3, as you describe. If you want to keep gcongr, the pattern formgcongr c + k * ?_stops at the right depth and leaves exactlyH + 2 ≤ L + 3. The add_le_add_left order is confirmed:add_le_add_left h a : b + a ≤ c + aandadd_le_add_right h a : a + b ≤ a + c.