Theorem: MeasureTheory.measureReal_biUnion_finset₀ (Carleson/ToMathlib/MeasureReal.lean)

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t : Set α
s : Finset ι
f : ι → Set α
hd : (↑s).Pairwise (AEDisjoint μ on f)
hm : ∀ b ∈ s, NullMeasurableSet (f b) μ
h : autoParam (∀ b ∈ s, μ (f b) ≠ ⊤) _auto✝
⊢ μ.real (⋃ b ∈ s, f b) = ∑ p ∈ s, μ.real (f p)
Tactic:
simp only [measureReal_def, measure_biUnion_finset₀ hd hm, ENNReal.toReal_sum h]
State after:
no goals