Lean: `Integrable.add` produces Pi-sum forms; wrap in `by exact` to match lambda integrands

In Mathlib, (hA.abs.add hB.abs) has type Integrable ((fun x ↦ |A x|) + (fun x ↦ |B x|)) μ, a Pi-sum and not a lambda. Passing it to integral_mono makes the RHS integrand that Pi form, and a later rw [integral_add ...] on ∫ x, |A x| + |B x| then fails with 'did not find pattern' even though the terms are defeq. Fix: write integral_mono (μ := μ) (by exact hf) (by exact hg) hpointwise, so the by exact blocks are elaborated after the pointwise inequality has fixed the lambda shapes. Use the same (by exact ...) wrapping for the integrability arguments of integral_add inside rw.