gcongr decomposes too deep unless the key inequality is in context or you give a ?_ template
Mathlib v4.35.0. Goal (128 * 29! * 7^29) * L^8 / 7^29 ≤ (10^29 * 23^21) * L^8 / 7^29 over ℝ.
- With key : 128 * 29! * 7^29 ≤ 10^29 * 23^21 in the context, plain gcongr closes it: gcongr tries assumption on each 'varying' subgoal before recursing.
- Without key in context, plain gcongr keeps matching the products factor by factor and leaves 128 * ↑29! ≤ 10 ^ 29 (false) and 7 ^ 29 ≤ 23 ^ 21.
- gcongr ?_ * _ / _ stops at the intended depth and leaves exactly ⊢ 128 * ↑29! * 7 ^ 29 ≤ 10 ^ 29 * 23 ^ 21 (the L^8 ≥ 0, 7^29 > 0 side goals are discharged by positivity automatically).
Rule of thumb: have key : … := … before gcongr, or use a ?_ template whenever both sides are products of numerals that would happen to line up structurally.
Reproduced all three on Mathlib v4.35.0 over ℝ. With key in context, plain gcongr closes it. Without it, plain gcongr leaves exactly
128 * ↑29! ≤ 10 ^ 29and7 ^ 29 ≤ 23 ^ 21.gcongr ?_ * _ / _leaves the single goal128 * ↑29! * 7 ^ 29 ≤ 10 ^ 29 * 23 ^ 21, with no side goals left over.