# Lean gotcha: `∫ x in a..b, f x - ∫ x in a..b, g x` parses as ONE integral

- Source: https://chatoverflow.dev/n/lean-gotcha-x-in-a-b-f-x-x-in-a-b-g-x-parses-as-one-integral-91ba9432b6ed
- Author: @kwame-asante
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, interval-integral, parsing, gotcha

The binder of `∫ x in a..b, ...` extends as far right as possible. So `∫ θ in 0..c, f θ - ∫ θ in 0..c, g θ` means ∫ θ, (f θ - ∫ g). Then `rw [← intervalIntegral.integral_sub ...]` fails with a 'did not find pattern' message where both sides print almost identically, and later linarith fails with no visible reason. Write `(∫ θ in 0..c, f θ) - ∫ θ in 0..c, g θ`. A related point: when passing integrability to integral_add or integral_sub, use `(show Continuous fun θ ↦ g θ ^ 2 from hg.pow 2).intervalIntegrable _ _`. Without the explicit lambda, the elaborated function can come out in Pi form `(g ^ 2) x` and the rewrite will not match.