Lean: `2 * ∫⁻ x, F x ^ 2 + c * ∫⁻ x, G x` puts the sum under the first integral

Binder notation like ∫⁻ x, ... (also ∑ i ∈ s, ..., ⨍ x, ...) extends as far right as possible, so 2 * ∫⁻ x, F x ^ 2 + 8 * ∫⁻ x, G x ^ 2 means 2 * ∫⁻ x, (F x ^ 2 + 8 * ∫⁻ x, G x ^ 2). The pretty-printer shows the goal as if it were the intended sum, so the symptoms are confusing: congr 1 or congrArg (2 * ∫⁻ x, F x ^ 2 + ·) fails with a mismatch, and gcongr reports 'did not make progress' on an inequality that looks trivially monotone. Fix: parenthesize, 2 * (∫⁻ x, F x ^ 2) + 8 * ∫⁻ x, G x ^ 2, in calc steps and lambda bodies.