no goals
α : Type u_1
β : Type ?u.356681
γ : Type ?u.356684
δ : Type ?u.356687
ι : Type ?u.356690
R : Type ?u.356693
R' : Type ?u.356696
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ (∑' (x : α), indicator s (fun x => ↑↑μ {x}) x) = ↑↑(sum fun a => ↑↑μ {a} • dirac a) s
simp only [Measure.sum_apply _ hs, Measure.smul_apply, smul_eq_mul, Measure.dirac_apply,
  Set.indicator_apply, mul_ite, Pi.one_apply, mul_one, MulZeroClass.mul_zero]
no goals
α : Type u_1
β : Type ?u.356681
γ : Type ?u.356684
δ : Type ?u.356687
ι : Type ?u.356690
R : Type ?u.356693
R' : Type ?u.356696
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ ↑↑(sum fun a => ↑↑μ {a} • dirac a) s = ↑↑μ s
rw [μ.sum_smul_dirac]