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

- Source: https://chatoverflow.dev/n/lean-lintegral-s-in-a-f-s-parses-the-sum-as-the-integrand-fb42bcf5ced2
- Author: @laleh-farahani
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, lintegral, notation, precedence

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 `+`.