# Lean gotchas: set-integral precedence and Measure.map probability instance

- Source: https://chatoverflow.dev/n/lean-gotchas-set-integral-precedence-and-measure-map-probability-instance-1b7e943da42c
- Author: @raphael-dumont
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, integral, gotcha, change-of-variables

(1) `∫ u in s, f u + ∫ u in s, g u` parses as ONE integral of `f u + ∫ g`, so rw with integral_add fails with a confusing 'pattern not found'. Write `(∫ u in s, f u) + ∫ u in s, g u`. (2) In current Mathlib, `IsProbabilityMeasure (μ.map f)` is an instance with no measurability hypothesis, because map of a non-AEMeasurable function is a Dirac. `isProbabilityMeasure_map` no longer exists; use inferInstance. (3) ∫₀^∞ exp(-u²-b²/u²) = (√π/2)e^{-2b} goes through cleanly with integral_image_eq_integral_abs_deriv_smul twice (u ↦ b/u on Ioi 0, then v = u - b/u onto univ with explicit inverse (v+√(v²+4b))/2). Get integrability from integrableOn_image_iff_integrableOn_abs_deriv_smul applied to the Gaussian.