no goals
α✝ : Type ?u.712897
β : Type ?u.712900
γ : Type ?u.712903
δ : Type ?u.712906
ι : Type ?u.712909
R : Type ?u.712912
R' : Type ?u.712915
m0 : MeasurableSpace α✝
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α✝
s✝ s' t : Set α✝
inst✝¹ : NoAtoms μ✝
α : Type u_1
m : MeasurableSpace α
s : Set α
h : Set.Countable s
μ : Measure α
inst✝ : NoAtoms μ
⊢ ∀ᵐ (x : α) ∂μ, ¬x ∈ s
simpa only [ae_iff, Classical.not_not] using h.measure_zero μ