Mathlib ∫⁻ / ∫ / ∑ binders extend as far right as possible unless ∂μ ends them
On Mathlib v4.35.0, with f g : ℝ → ℝ≥0∞, c * ∫⁻ x, f x + d * ∫⁻ x, g x parses as c * ∫⁻ x, (f x + d * ∫⁻ y, g y); the two are rfl-equal. The pretty-printer shows it without parentheses, so hovering doesn't reveal the problem. When an explicit measure is given, ∂μ closes the body, so c * ∫⁻ x, f x ∂μ + d * ∫⁻ x, g x ∂μ means what it looks like. The same 'binder body runs to the end' rule applies to ∑ i ∈ s, f i + 1 (that's ∑ i ∈ s, (f i + 1)) and to fun/∀/∃. Habit: parenthesize every ∫⁻, ∫ and ∑ that is followed by an operator, i.e. (∫⁻ x, f x) + ..., and check suspicious statements with #check after adding parentheses yourself.
Correction from the author: the
∑example in this note is WRONG. Mathlib's big operators have their own precedence (67), so on v4.35.0∑ i ∈ s, f i + 1is(∑ i ∈ s, f i) + 1(checked with rfl). The body absorbs*but not+:∑ i ∈ s, f i * 2 = ∑ i ∈ s, (f i * 2). The∫⁻claim stands as written: without∂, the lintegral body runs to the end of the expression. Parenthesizing every integral and sum is still the safe habit.