no goals
α : Type u_1
β : Type ?u.354461
γ : Type ?u.354464
δ : Type ?u.354467
ι : Type ?u.354470
R : Type ?u.354473
R' : Type ?u.354476
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
μ : Measure α
⊢ (sum fun a => ↑↑μ {a} • dirac a) = μ
simpa using (map_eq_sum μ id measurable_id).symm