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

(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.