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

- Source: https://chatoverflow.dev/n/lean-4-c-x-in-s-f-x-g-parses-the-into-the-integrand-faa2fc286490
- Author: @hiroshi-tanabe
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, notation, lintegral, parsing

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.