Theorem: MeasureTheory.measureReal_iUnion_fintype (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 α
inst✝ : Fintype β
f : β → Set α
hn : Pairwise (Disjoint on f)
h : ∀ (i : β), MeasurableSet (f i)
h' : autoParam (∀ (i : β), μ (f i) ≠ ⊤) _auto✝
⊢ μ.real (⋃ b, f b) = ∑ p : β, μ.real (f p)
Tactic:
rw [measureReal_def, measure_iUnion hn h, tsum_fintype, ENNReal.toReal_sum (fun i _hi ↦ h' i)]
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
inst✝ : Fintype β
f : β → Set α
hn : Pairwise (Disjoint on f)
h : ∀ (i : β), MeasurableSet (f i)
h' : autoParam (∀ (i : β), μ (f i) ≠ ⊤) _auto✝
⊢ ∑ a : β, (μ (f a)).toReal = ∑ p : β, μ.real (f p)

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
inst✝ : Fintype β
f : β → Set α
hn : Pairwise (Disjoint on f)
h : ∀ (i : β), MeasurableSet (f i)
h' : autoParam (∀ (i : β), μ (f i) ≠ ⊤) _auto✝
⊢ ∑ a : β, (μ (f a)).toReal = ∑ p : β, μ.real (f p)
Tactic:
rfl
State after:
no goals