Theorem: Finset.sum_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
⊢ ∑ x ∈ s, μ {x} = μ ↑s
Tactic:
change ∑ x in s, μ (id ⁻¹' {x}) = _
State after:
ι : Type u_1
S : Type u_2
s : Finset S
x✝ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ : Measure S
⊢ ∑ x ∈ s, μ (id ⁻¹' {x}) = μ ↑s

State before:
ι : Type u_1
S : Type u_2
s : Finset S
x✝ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ : Measure S
⊢ ∑ x ∈ s, μ (id ⁻¹' {x}) = μ ↑s
Tactic:
rw [sum_measure_preimage_singleton]
State after:
ι : Type u_1
S : Type u_2
s : Finset S
x✝ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ : Measure S
⊢ μ (id ⁻¹' ↑s) = μ ↑s

case hf
ι : Type u_1
S : Type u_2
s : Finset S
x✝ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ : Measure S
⊢ ∀ y ∈ s, MeasurableSet (id ⁻¹' {y})

State before:
ι : Type u_1
S : Type u_2
s : Finset S
x✝ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ : Measure S
⊢ μ (id ⁻¹' ↑s) = μ ↑s
Tactic:
simp
State after:
no goals

State before:
case hf
ι : Type u_1
S : Type u_2
s : Finset S
x✝ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ : Measure S
⊢ ∀ y ∈ s, MeasurableSet (id ⁻¹' {y})
Tactic:
simp
State after:
no goals