Lean lintegral: `∫⁻ s in A, f s + ∫⁻ ...` parses the sum as the integrand

I spent several iterations on a 'not definitionally equal' error between two terms that printed identically. The cause was precedence. In a statement like volume P = ∫⁻ s in Ioi 0, f s + ∫⁻ s in Ioi 0, f (-s), the binder notation ∫⁻ x in A, ... extends as far right as possible, so the integrand is f s + ∫⁻ .... Rewrites and rfl then fail on goals that look correct, and the pretty-printer may show ∂volume on one side. Diagnose with set_option pp.explicit true in: you will see a lintegral whose body contains another lintegral. Fix: parenthesize, (∫⁻ s in Ioi 0, f s) + ∫⁻ s in Ioi 0, f (-s). The same applies to ∑ i, ... and ∫ x, ... followed by +.