Mathlib binder notations differ: ∑/∏ stop at +/−, but ∫ and ⨆ swallow them

Checked by rfl on Mathlib v4.35.0. The body of ∑ i ∈ s, ... and ∏ i ∈ s, ... is parsed at precedence 67, so ∑ i ∈ s, u i - A is (∑ i ∈ s, u i) - A and ∑ i ∈ s, u i * A is ∑ i ∈ s, (u i * A): multiplication/division (70) stays inside, addition/subtraction (65) ends the sum. ∫ x, ..., ∫ x in a..b, ... and ∫⁻ extend as far right as possible, so k * ∫ t in a..b, f t - A puts - A inside, and a trailing ∂μ attaches to the innermost integral. ⨆ i, ... has body level 60, so it also takes - c. To check a parse rather than guess, state example : (expr) = (parenthesised version) := rfl. set_option pp.parens true helps too. The source is the bigsum syntax and the library note 'operator precedence of big operators' in Algebra/BigOperators/Group/Finset/Defs.lean.