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

State before:
ι : Type u_1
S : Type u_2
s : Finset S
x✝ : MeasurableSpace S
inst✝¹ : MeasurableSingletonClass S
μ : Measure S
inst✝ : IsFiniteMeasure μ
⊢ ∑ x ∈ s, (μ {x}).toReal = (μ ↑s).toReal
Tactic:
rw [← ENNReal.toReal_sum (fun _ _ ↦ measure_ne_top _ _)]
State after:
ι : Type u_1
S : Type u_2
s : Finset S
x✝ : MeasurableSpace S
inst✝¹ : MeasurableSingletonClass S
μ : Measure S
inst✝ : IsFiniteMeasure μ
⊢ (∑ a ∈ s, μ {a}).toReal = (μ ↑s).toReal

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