no goals
α : Type u_1
β : Type ?u.548833
γ : Type ?u.548836
δ : Type ?u.548839
ι : Type ?u.548842
R : Type ?u.548845
R' : Type ?u.548848
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
⊢ ae μ = ⊥ ↔ μ = 0
rw [← empty_mem_iff_bot, mem_ae_iff, compl_empty, measure_univ_eq_zero]