ι✝ : Type ?u.370301
ι' : Type ?u.370304
α : Type ?u.370307
β : Type ?u.370310
γ : Type ?u.370313
ι : Type u_1
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
this : (∀ᶠ (n : ι) in l, p n) ↔ ¬∃ᶠ (n : ι) in l, ¬p n
⊢ (∀ᶠ (n : ι) in l, p n) ↔ ∀ (x : ℕ → ι), Tendsto x atTop l → ∀ᶠ (n : ℕ) in atTop, p (x n)
ι✝ : Type ?u.370301
ι' : Type ?u.370304
α : Type ?u.370307
β : Type ?u.370310
γ : Type ?u.370313
ι : Type u_1
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
⊢ (∀ᶠ (n : ι) in l, p n) ↔ ∀ (x : ℕ → ι), Tendsto x atTop l → ∀ᶠ (n : ℕ) in atTop, p (x n)
have : (∀ᶠ n in l, p n) ↔ ¬∃ᶠ n in l, ¬p n := by
  rw [not_frequently]
  simp_rw [not_not]
ι✝ : Type ?u.370301
ι' : Type ?u.370304
α : Type ?u.370307
β : Type ?u.370310
γ : Type ?u.370313
ι : Type u_1
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
this : (∀ᶠ (n : ι) in l, p n) ↔ ¬∃ᶠ (n : ι) in l, ¬p n
⊢ (¬∃ x, Tendsto x atTop l ∧ ∃ᶠ (n : ℕ) in atTop, ¬p (x n)) ↔
    ∀ (x : ℕ → ι), Tendsto x atTop l → ∀ᶠ (n : ℕ) in atTop, p (x n)
ι✝ : Type ?u.370301
ι' : Type ?u.370304
α : Type ?u.370307
β : Type ?u.370310
γ : Type ?u.370313
ι : Type u_1
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
this : (∀ᶠ (n : ι) in l, p n) ↔ ¬∃ᶠ (n : ι) in l, ¬p n
⊢ (∀ᶠ (n : ι) in l, p n) ↔ ∀ (x : ℕ → ι), Tendsto x atTop l → ∀ᶠ (n : ℕ) in atTop, p (x n)
rw [this, frequently_iff_seq_frequently]
ι✝ : Type ?u.370301
ι' : Type ?u.370304
α : Type ?u.370307
β : Type ?u.370310
γ : Type ?u.370313
ι : Type u_1
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
this : (∀ᶠ (n : ι) in l, p n) ↔ ¬∃ᶠ (n : ι) in l, ¬p n
⊢ (∀ (x : ℕ → ι), Tendsto x atTop l → ¬∃ᶠ (n : ℕ) in atTop, ¬p (x n)) ↔
    ∀ (x : ℕ → ι), Tendsto x atTop l → ∀ᶠ (n : ℕ) in atTop, p (x n)
ι✝ : Type ?u.370301
ι' : Type ?u.370304
α : Type ?u.370307
β : Type ?u.370310
γ : Type ?u.370313
ι : Type u_1
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
this : (∀ᶠ (n : ι) in l, p n) ↔ ¬∃ᶠ (n : ι) in l, ¬p n
⊢ (¬∃ x, Tendsto x atTop l ∧ ∃ᶠ (n : ℕ) in atTop, ¬p (x n)) ↔
    ∀ (x : ℕ → ι), Tendsto x atTop l → ∀ᶠ (n : ℕ) in atTop, p (x n)
push_neg
no goals
ι✝ : Type ?u.370301
ι' : Type ?u.370304
α : Type ?u.370307
β : Type ?u.370310
γ : Type ?u.370313
ι : Type u_1
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
this : (∀ᶠ (n : ι) in l, p n) ↔ ¬∃ᶠ (n : ι) in l, ¬p n
⊢ (∀ (x : ℕ → ι), Tendsto x atTop l → ¬∃ᶠ (n : ℕ) in atTop, ¬p (x n)) ↔
    ∀ (x : ℕ → ι), Tendsto x atTop l → ∀ᶠ (n : ℕ) in atTop, p (x n)
simp_rw [not_frequently, not_not]
ι✝ : Type ?u.370301
ι' : Type ?u.370304
α : Type ?u.370307
β : Type ?u.370310
γ : Type ?u.370313
ι : Type u_1
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
⊢ (∀ᶠ (n : ι) in l, p n) ↔ ∀ᶠ (x : ι) in l, ¬¬p x
ι✝ : Type ?u.370301
ι' : Type ?u.370304
α : Type ?u.370307
β : Type ?u.370310
γ : Type ?u.370313
ι : Type u_1
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
⊢ (∀ᶠ (n : ι) in l, p n) ↔ ¬∃ᶠ (n : ι) in l, ¬p n
rw [not_frequently]
no goals
ι✝ : Type ?u.370301
ι' : Type ?u.370304
α : Type ?u.370307
β : Type ?u.370310
γ : Type ?u.370313
ι : Type u_1
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
⊢ (∀ᶠ (n : ι) in l, p n) ↔ ∀ᶠ (x : ι) in l, ¬¬p x
simp_rw [not_not]