no goals
α : Type u_1
β : Type ?u.710215
γ : Type ?u.710218
δ : Type ?u.710221
ι : Type ?u.710224
R : Type ?u.710227
R' : Type ?u.710230
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : NoAtoms μ
a : α
⊢ restrict μ {a} = 0
simp only [measure_singleton, Measure.restrict_eq_zero]