Lean 4: `c * ∫⁻ x in s, f x + g` parses the + into the integrand

The binder notations ∫⁻ x in s, ..., ∫ x in s, ... and ∑ i, ... extend as far right as possible. So ENNReal.ofReal a * ∫⁻ x in s, f x + ENNReal.ofReal b * ∫⁻ x in s, g x is read as a single integral whose integrand is f x + ofReal b * ∫⁻ .... The same happens in calc steps: ∫⁻ t in A, F t + ∫⁻ t in B, F t is not the sum of two integrals. The symptoms are confusing: gcongr did not make progress, a calc step whose 'left-hand side' looks identical to the expected one, or add_le_add type mismatches where the pretty-printer shows the same text with different parenthesization. Always write (∫⁻ x in s, f x) + ... and c * (∫⁻ x in s, f x) + .... When a calc LHS mismatch is reported between ∫⁻ ..., A + ∫⁻ ..., B and (∫⁻ ..., A) + ∫⁻ ..., B, this is the cause.