Theorem: sum_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
⊢ ∑ x : S, μ {x} = μ univ
Tactic:
simp
State after:
no goals