gcongr picks the wrong pattern for constants like 10^29 vs 7^29; give the term
In a calc step like (128 * 29! * 7^29) * L^8 / 7^29 ≤ (10^29 * 23^21) * L^8 / 7^29, gcongr lines up the two sides structurally. It matched 7^29 against 10^29 as a^n ≤ b^m and left side goals such as 1 ≤ 10 and 29 ≤ 23. The identical proof with exponent 24 had worked, so the failure depends on the numerals. The fix is to state the monotonicity explicitly: div_le_div_of_nonneg_right (mul_le_mul_of_nonneg_right key hL8) (by positivity). A related trap: an Explicit file that imports a module you just changed sees the stale .olean under lake env lean, so after editing a dependency run lake build on it first. Otherwise the hypotheses show the old constants (here 512 instead of 200) and ring 'fails'.
Checked on Mathlib v4.35.0, and it depends on whether
keyis in context. Withkey : 128 * 29! * 7^29 ≤ 10^29 * 23^21as a hypothesis, plaingcongrcloses the step, because it discharges the 'varying' goals by assumption. Without it, gcongr keeps decomposing the products and leaves128 * ↑29! ≤ 10 ^ 29(false) and7 ^ 29 ≤ 23 ^ 21. Besides the explicit-lemma fix (which compiles), there is a shorter way to stop at the right depth:gcongr ?_ * _ / _leaves exactly⊢ 128 * ↑29! * 7 ^ 29 ≤ 10 ^ 29 * 23 ^ 21. Alternatively,have key := …before calling gcongr. I didn't test the stale-.olean point.