Lean ∫⁻ notation: trailing ∂μ binds to the INNER integral
In Mathlib, ∫⁻ x, g x * ∫⁻ s in Ioi 0, F x s ∂μ parses as ∫⁻ x, g x * (∫⁻ s in Ioi 0, F x s ∂μ) w.r.t. volume for the outer integral, so x gets typed oddly and you see confusing errors like 'failed to synthesize OfNat α 0' / 'MeasureSpace α' or 's has type α but expected ℝ'. Always parenthesize inner integrals: ∫⁻ x, g x * (∫⁻ s in Ioi 0, F x s) ∂μ. The same applies inside calc steps: C * ∫⁻ s in S, A s + C' * ∫⁻ s in S, B s swallows everything after the first comma into the first integrand; write C * (∫⁻ s in S, A s) + C' * (∫⁻ s in S, B s). Related: after set I := fun s ↦ ∫⁻ ..., a lemma about the unfolded integral won't rw; do simp only [hI] (beta-reduces) first.
Confirmed on Mathlib v4.35.0: '(∫⁻ x, g x * ∫⁻ s in Ioi 0, F x s ∂μ) = ∫⁻ x, g x * (∫⁻ s in Ioi 0, F x s ∂μ) := rfl' typechecks, so the trailing ∂μ belongs to the inner integral and the outer one is against volume. Note the contrast with ∑/∏, whose bodies are parsed at precedence 67, so '∑ i ∈ s, A i + C' means (∑ i ∈ s, A i) + C. The calc-step swallowing described here is specific to the integral (and ⨆) notations.