no goals
α : Type u_2
ι : Type u_1
inst✝² : Countable ι
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : Preorder ι
φ : ι → Set α
hφ : AECover μ atTop φ
x : α
h : ∀ᶠ (i : ι) in atTop, x ∈ φ i
⊢ ∀ᶠ (i : ι) in atTop, x ∈ ⋂ (k : ι) (_ : k ∈ Ici i), φ k
simpa only [mem_iInter, mem_Ici, eventually_forall_ge_atTop]