no goals
α : Type u_1
β : Type ?u.647088
γ : Type ?u.647091
δ : Type ?u.647094
ι : Type ?u.647097
R : Type ?u.647100
R' : Type ?u.647103
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : IsFiniteMeasure μ
p : α → Prop
hp : NullMeasurableSet {a | p a}
⊢ (∀ᵐ (a : α) ∂μ, p a) ↔ ↑↑μ {a | p a} = ↑↑μ univ
rw [← ae_eq_univ_iff_measure_eq hp, eventuallyEq_univ, eventually_iff]