Theorem: MeasureTheory.sum_measureReal_preimage_singleton (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 : α → β
hf : ∀ y ∈ s, MeasurableSet (f ⁻¹' {y})
h : autoParam (∀ a ∈ s, μ (f ⁻¹' {a}) ≠ ⊤) _auto✝
⊢ ∑ b ∈ s, μ.real (f ⁻¹' {b}) = μ.real (f ⁻¹' ↑s)
Tactic:
simp only [measureReal_def, ← sum_measure_preimage_singleton s hf, ENNReal.toReal_sum h]
State after:
no goals