no goals
α : Type u_1
β : Type ?u.590790
γ : Type ?u.590793
δ : Type ?u.590796
ι : Type ?u.590799
R : Type ?u.590802
R' : Type ?u.590805
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
p : ℕ → α → Prop
hp : (∑' (i : ℕ), ↑↑μ {x | p i x}) ≠ ⊤
⊢ ↑↑μ {x | ∃ᶠ (n : ℕ) in atTop, p n x} = 0
simpa only [limsup_eq_iInf_iSup_of_nat, frequently_atTop, ← bex_def, setOf_forall,
  setOf_exists] using measure_limsup_eq_zero hp