no goals
ι : Type u_2
ι' : Type ?u.367980
α : Type u_1
β : Type ?u.367986
γ : Type ?u.367989
x : ι → α
f : Filter α
l : Filter ι
⊢ ¬Tendsto x l f ↔ ∃ s, s ∈ f ∧ ∃ᶠ (n : ι) in l, ¬x n ∈ s
simp only [tendsto_iff_forall_eventually_mem, not_forall, exists_prop, Filter.Frequently, not_not]