Theorem: sum_toReal_measure_singleton (Carleson/ToMathlib/MeasureReal.lean)

State before:
ι : Type u_1
S : Type u_2
inst✝² : Fintype S
x✝ : MeasurableSpace S
inst✝¹ : MeasurableSingletonClass S
μ : Measure S
inst✝ : IsFiniteMeasure μ
⊢ ∑ x : S, (μ {x}).toReal = (μ univ).toReal
Tactic:
simp
State after:
no goals