ι✝ : Type ?u.372453
ι' : Type ?u.372456
α✝ : Type ?u.372459
β : Type ?u.372462
γ : Type ?u.372465
α : Type u_1
ι : Type u_2
x : ι → α
f : Filter α
l : Filter ι
inst✝ : IsCountablyGenerated l
hxy : ∀ (ns : ℕ → ι), Tendsto ns atTop l → ∃ ms, Tendsto (fun n => x (ns (ms n))) atTop f
h : ¬Tendsto x l f
⊢ False
ι✝ : Type ?u.372453
ι' : Type ?u.372456
α✝ : Type ?u.372459
β : Type ?u.372462
γ : Type ?u.372465
α : Type u_1
ι : Type u_2
x : ι → α
f : Filter α
l : Filter ι
inst✝ : IsCountablyGenerated l
hxy : ∀ (ns : ℕ → ι), Tendsto ns atTop l → ∃ ms, Tendsto (fun n => x (ns (ms n))) atTop f
⊢ Tendsto x l f
by_contra h
case intro.intro
ι✝ : Type ?u.372453
ι' : Type ?u.372456
α✝ : Type ?u.372459
β : Type ?u.372462
γ : Type ?u.372465
α : Type u_1
ι : Type u_2
x : ι → α
f : Filter α
l : Filter ι
inst✝ : IsCountablyGenerated l
hxy : ∀ (ns : ℕ → ι), Tendsto ns atTop l → ∃ ms, Tendsto (fun n => x (ns (ms n))) atTop f
h : ¬Tendsto x l f
s : Set α
hs : s ∈ f
hfreq : ∃ᶠ (n : ι) in l, ¬x n ∈ s
⊢ False
ι✝ : Type ?u.372453
ι' : Type ?u.372456
α✝ : Type ?u.372459
β : Type ?u.372462
γ : Type ?u.372465
α : Type u_1
ι : Type u_2
x : ι → α
f : Filter α
l : Filter ι
inst✝ : IsCountablyGenerated l
hxy : ∀ (ns : ℕ → ι), Tendsto ns atTop l → ∃ ms, Tendsto (fun n => x (ns (ms n))) atTop f
h : ¬Tendsto x l f
⊢ False
obtain ⟨s, hs, hfreq⟩ : ∃ s ∈ f, ∃ᶠ n in l, x n ∉ s := by
  rwa [not_tendsto_iff_exists_frequently_nmem] at h
case intro.intro.intro.intro
ι✝ : Type ?u.372453
ι' : Type ?u.372456
α✝ : Type ?u.372459
β : Type ?u.372462
γ : Type ?u.372465
α : Type u_1
ι : Type u_2
x : ι → α
f : Filter α
l : Filter ι
inst✝ : IsCountablyGenerated l
hxy : ∀ (ns : ℕ → ι), Tendsto ns atTop l → ∃ ms, Tendsto (fun n => x (ns (ms n))) atTop f
h : ¬Tendsto x l f
s : Set α
hs : s ∈ f
hfreq : ∃ᶠ (n : ι) in l, ¬x n ∈ s
y : ℕ → ι
hy_tendsto : Tendsto y atTop l
hy_freq : ∀ (n : ℕ), ¬x (y n) ∈ s
⊢ False
case intro.intro
ι✝ : Type ?u.372453
ι' : Type ?u.372456
α✝ : Type ?u.372459
β : Type ?u.372462
γ : Type ?u.372465
α : Type u_1
ι : Type u_2
x : ι → α
f : Filter α
l : Filter ι
inst✝ : IsCountablyGenerated l
hxy : ∀ (ns : ℕ → ι), Tendsto ns atTop l → ∃ ms, Tendsto (fun n => x (ns (ms n))) atTop f
h : ¬Tendsto x l f
s : Set α
hs : s ∈ f
hfreq : ∃ᶠ (n : ι) in l, ¬x n ∈ s
⊢ False
obtain ⟨y, hy_tendsto, hy_freq⟩ := exists_seq_forall_of_frequently hfreq
case intro.intro.intro.intro
ι✝ : Type ?u.372453
ι' : Type ?u.372456
α✝ : Type ?u.372459
β : Type ?u.372462
γ : Type ?u.372465
α : Type u_1
ι : Type u_2
x : ι → α
f : Filter α
l : Filter ι
inst✝ : IsCountablyGenerated l
h : ¬Tendsto x l f
s : Set α
hs : s ∈ f
hfreq : ∃ᶠ (n : ι) in l, ¬x n ∈ s
y : ℕ → ι
hy_tendsto : Tendsto y atTop l
hy_freq : ∀ (n : ℕ), ¬x (y n) ∈ s
hxy : ∃ ms, Tendsto (fun n => x (y (ms n))) atTop f
⊢ False
case intro.intro.intro.intro
ι✝ : Type ?u.372453
ι' : Type ?u.372456
α✝ : Type ?u.372459
β : Type ?u.372462
γ : Type ?u.372465
α : Type u_1
ι : Type u_2
x : ι → α
f : Filter α
l : Filter ι
inst✝ : IsCountablyGenerated l
hxy : ∀ (ns : ℕ → ι), Tendsto ns atTop l → ∃ ms, Tendsto (fun n => x (ns (ms n))) atTop f
h : ¬Tendsto x l f
s : Set α
hs : s ∈ f
hfreq : ∃ᶠ (n : ι) in l, ¬x n ∈ s
y : ℕ → ι
hy_tendsto : Tendsto y atTop l
hy_freq : ∀ (n : ℕ), ¬x (y n) ∈ s
⊢ False
specialize hxy y hy_tendsto
case intro.intro.intro.intro.intro
ι✝ : Type ?u.372453
ι' : Type ?u.372456
α✝ : Type ?u.372459
β : Type ?u.372462
γ : Type ?u.372465
α : Type u_1
ι : Type u_2
x : ι → α
f : Filter α
l : Filter ι
inst✝ : IsCountablyGenerated l
h : ¬Tendsto x l f
s : Set α
hs : s ∈ f
hfreq : ∃ᶠ (n : ι) in l, ¬x n ∈ s
y : ℕ → ι
hy_tendsto : Tendsto y atTop l
hy_freq : ∀ (n : ℕ), ¬x (y n) ∈ s
ms : ℕ → ℕ
hms_tendsto : Tendsto (fun n => x (y (ms n))) atTop f
⊢ False
case intro.intro.intro.intro
ι✝ : Type ?u.372453
ι' : Type ?u.372456
α✝ : Type ?u.372459
β : Type ?u.372462
γ : Type ?u.372465
α : Type u_1
ι : Type u_2
x : ι → α
f : Filter α
l : Filter ι
inst✝ : IsCountablyGenerated l
h : ¬Tendsto x l f
s : Set α
hs : s ∈ f
hfreq : ∃ᶠ (n : ι) in l, ¬x n ∈ s
y : ℕ → ι
hy_tendsto : Tendsto y atTop l
hy_freq : ∀ (n : ℕ), ¬x (y n) ∈ s
hxy : ∃ ms, Tendsto (fun n => x (y (ms n))) atTop f
⊢ False
obtain ⟨ms, hms_tendsto⟩ := hxy
case intro.intro.intro.intro.intro
ι✝ : Type ?u.372453
ι' : Type ?u.372456
α✝ : Type ?u.372459
β : Type ?u.372462
γ : Type ?u.372465
α : Type u_1
ι : Type u_2
x : ι → α
f : Filter α
l : Filter ι
inst✝ : IsCountablyGenerated l
h : ¬Tendsto x l f
s : Set α
hs : s ∈ f
hfreq : ∃ᶠ (n : ι) in l, ¬x n ∈ s
y : ℕ → ι
hy_tendsto : Tendsto y atTop l
hy_freq : ∀ (n : ℕ), ¬x (y n) ∈ s
ms : ℕ → ℕ
hms_tendsto : s ∈ map (fun n => x (y (ms n))) atTop
⊢ False
case intro.intro.intro.intro.intro
ι✝ : Type ?u.372453
ι' : Type ?u.372456
α✝ : Type ?u.372459
β : Type ?u.372462
γ : Type ?u.372465
α : Type u_1
ι : Type u_2
x : ι → α
f : Filter α
l : Filter ι
inst✝ : IsCountablyGenerated l
h : ¬Tendsto x l f
s : Set α
hs : s ∈ f
hfreq : ∃ᶠ (n : ι) in l, ¬x n ∈ s
y : ℕ → ι
hy_tendsto : Tendsto y atTop l
hy_freq : ∀ (n : ℕ), ¬x (y n) ∈ s
ms : ℕ → ℕ
hms_tendsto : Tendsto (fun n => x (y (ms n))) atTop f
⊢ False
specialize hms_tendsto hs
case intro.intro.intro.intro.intro
ι✝ : Type ?u.372453
ι' : Type ?u.372456
α✝ : Type ?u.372459
β : Type ?u.372462
γ : Type ?u.372465
α : Type u_1
ι : Type u_2
x : ι → α
f : Filter α
l : Filter ι
inst✝ : IsCountablyGenerated l
h : ¬Tendsto x l f
s : Set α
hs : s ∈ f
hfreq : ∃ᶠ (n : ι) in l, ¬x n ∈ s
y : ℕ → ι
hy_tendsto : Tendsto y atTop l
hy_freq : ∀ (n : ℕ), ¬x (y n) ∈ s
ms : ℕ → ℕ
hms_tendsto : (fun n => x (y (ms n))) ⁻¹' s ∈ atTop
⊢ False
case intro.intro.intro.intro.intro
ι✝ : Type ?u.372453
ι' : Type ?u.372456
α✝ : Type ?u.372459
β : Type ?u.372462
γ : Type ?u.372465
α : Type u_1
ι : Type u_2
x : ι → α
f : Filter α
l : Filter ι
inst✝ : IsCountablyGenerated l
h : ¬Tendsto x l f
s : Set α
hs : s ∈ f
hfreq : ∃ᶠ (n : ι) in l, ¬x n ∈ s
y : ℕ → ι
hy_tendsto : Tendsto y atTop l
hy_freq : ∀ (n : ℕ), ¬x (y n) ∈ s
ms : ℕ → ℕ
hms_tendsto : s ∈ map (fun n => x (y (ms n))) atTop
⊢ False
rw [mem_map] at hms_tendsto
case intro.intro.intro.intro.intro
ι✝ : Type ?u.372453
ι' : Type ?u.372456
α✝ : Type ?u.372459
β : Type ?u.372462
γ : Type ?u.372465
α : Type u_1
ι : Type u_2
x : ι → α
f : Filter α
l : Filter ι
inst✝ : IsCountablyGenerated l
h : ¬Tendsto x l f
s : Set α
hs : s ∈ f
hfreq : ∃ᶠ (n : ι) in l, ¬x n ∈ s
y : ℕ → ι
hy_tendsto : Tendsto y atTop l
hy_freq : ∀ (n : ℕ), ¬x (y n) ∈ s
ms : ℕ → ℕ
hms_tendsto : (fun n => x (y (ms n))) ⁻¹' s ∈ atTop
hms_freq : ∀ (n : ℕ), ¬x (y (ms n)) ∈ s
⊢ False
case intro.intro.intro.intro.intro
ι✝ : Type ?u.372453
ι' : Type ?u.372456
α✝ : Type ?u.372459
β : Type ?u.372462
γ : Type ?u.372465
α : Type u_1
ι : Type u_2
x : ι → α
f : Filter α
l : Filter ι
inst✝ : IsCountablyGenerated l
h : ¬Tendsto x l f
s : Set α
hs : s ∈ f
hfreq : ∃ᶠ (n : ι) in l, ¬x n ∈ s
y : ℕ → ι
hy_tendsto : Tendsto y atTop l
hy_freq : ∀ (n : ℕ), ¬x (y n) ∈ s
ms : ℕ → ℕ
hms_tendsto : (fun n => x (y (ms n))) ⁻¹' s ∈ atTop
⊢ False
have hms_freq : ∀ n : ℕ, x (y (ms n)) ∉ s := fun n => hy_freq (ms n)
case intro.intro.intro.intro.intro
ι✝ : Type ?u.372453
ι' : Type ?u.372456
α✝ : Type ?u.372459
β : Type ?u.372462
γ : Type ?u.372465
α : Type u_1
ι : Type u_2
x : ι → α
f : Filter α
l : Filter ι
inst✝ : IsCountablyGenerated l
h : ¬Tendsto x l f
s : Set α
hs : s ∈ f
hfreq : ∃ᶠ (n : ι) in l, ¬x n ∈ s
y : ℕ → ι
hy_tendsto : Tendsto y atTop l
hy_freq : ∀ (n : ℕ), ¬x (y n) ∈ s
ms : ℕ → ℕ
hms_tendsto : (fun n => x (y (ms n))) ⁻¹' s ∈ atTop
hms_freq : ∀ (n : ℕ), ¬x (y (ms n)) ∈ s
h_empty : (fun n => x (y (ms n))) ⁻¹' s = ∅
⊢ False
case intro.intro.intro.intro.intro
ι✝ : Type ?u.372453
ι' : Type ?u.372456
α✝ : Type ?u.372459
β : Type ?u.372462
γ : Type ?u.372465
α : Type u_1
ι : Type u_2
x : ι → α
f : Filter α
l : Filter ι
inst✝ : IsCountablyGenerated l
h : ¬Tendsto x l f
s : Set α
hs : s ∈ f
hfreq : ∃ᶠ (n : ι) in l, ¬x n ∈ s
y : ℕ → ι
hy_tendsto : Tendsto y atTop l
hy_freq : ∀ (n : ℕ), ¬x (y n) ∈ s
ms : ℕ → ℕ
hms_tendsto : (fun n => x (y (ms n))) ⁻¹' s ∈ atTop
hms_freq : ∀ (n : ℕ), ¬x (y (ms n)) ∈ s
⊢ False
have h_empty : (fun n : ℕ => x (y (ms n))) ⁻¹' s = ∅ := by
  ext1 n
  simp only [Set.mem_preimage, Set.mem_empty_iff_false, iff_false_iff]
  exact hms_freq n
case intro.intro.intro.intro.intro
ι✝ : Type ?u.372453
ι' : Type ?u.372456
α✝ : Type ?u.372459
β : Type ?u.372462
γ : Type ?u.372465
α : Type u_1
ι : Type u_2
x : ι → α
f : Filter α
l : Filter ι
inst✝ : IsCountablyGenerated l
h : ¬Tendsto x l f
s : Set α
hs : s ∈ f
hfreq : ∃ᶠ (n : ι) in l, ¬x n ∈ s
y : ℕ → ι
hy_tendsto : Tendsto y atTop l
hy_freq : ∀ (n : ℕ), ¬x (y n) ∈ s
ms : ℕ → ℕ
hms_tendsto : ∅ ∈ atTop
hms_freq : ∀ (n : ℕ), ¬x (y (ms n)) ∈ s
h_empty : (fun n => x (y (ms n))) ⁻¹' s = ∅
⊢ False
case intro.intro.intro.intro.intro
ι✝ : Type ?u.372453
ι' : Type ?u.372456
α✝ : Type ?u.372459
β : Type ?u.372462
γ : Type ?u.372465
α : Type u_1
ι : Type u_2
x : ι → α
f : Filter α
l : Filter ι
inst✝ : IsCountablyGenerated l
h : ¬Tendsto x l f
s : Set α
hs : s ∈ f
hfreq : ∃ᶠ (n : ι) in l, ¬x n ∈ s
y : ℕ → ι
hy_tendsto : Tendsto y atTop l
hy_freq : ∀ (n : ℕ), ¬x (y n) ∈ s
ms : ℕ → ℕ
hms_tendsto : (fun n => x (y (ms n))) ⁻¹' s ∈ atTop
hms_freq : ∀ (n : ℕ), ¬x (y (ms n)) ∈ s
h_empty : (fun n => x (y (ms n))) ⁻¹' s = ∅
⊢ False
rw [h_empty] at hms_tendsto
no goals
case intro.intro.intro.intro.intro
ι✝ : Type ?u.372453
ι' : Type ?u.372456
α✝ : Type ?u.372459
β : Type ?u.372462
γ : Type ?u.372465
α : Type u_1
ι : Type u_2
x : ι → α
f : Filter α
l : Filter ι
inst✝ : IsCountablyGenerated l
h : ¬Tendsto x l f
s : Set α
hs : s ∈ f
hfreq : ∃ᶠ (n : ι) in l, ¬x n ∈ s
y : ℕ → ι
hy_tendsto : Tendsto y atTop l
hy_freq : ∀ (n : ℕ), ¬x (y n) ∈ s
ms : ℕ → ℕ
hms_tendsto : ∅ ∈ atTop
hms_freq : ∀ (n : ℕ), ¬x (y (ms n)) ∈ s
h_empty : (fun n => x (y (ms n))) ⁻¹' s = ∅
⊢ False
exact empty_not_mem atTop hms_tendsto
no goals
ι✝ : Type ?u.372453
ι' : Type ?u.372456
α✝ : Type ?u.372459
β : Type ?u.372462
γ : Type ?u.372465
α : Type u_1
ι : Type u_2
x : ι → α
f : Filter α
l : Filter ι
inst✝ : IsCountablyGenerated l
hxy : ∀ (ns : ℕ → ι), Tendsto ns atTop l → ∃ ms, Tendsto (fun n => x (ns (ms n))) atTop f
h : ¬Tendsto x l f
⊢ ∃ s, s ∈ f ∧ ∃ᶠ (n : ι) in l, ¬x n ∈ s
rwa [not_tendsto_iff_exists_frequently_nmem] at h
case h
ι✝ : Type ?u.372453
ι' : Type ?u.372456
α✝ : Type ?u.372459
β : Type ?u.372462
γ : Type ?u.372465
α : Type u_1
ι : Type u_2
x : ι → α
f : Filter α
l : Filter ι
inst✝ : IsCountablyGenerated l
h : ¬Tendsto x l f
s : Set α
hs : s ∈ f
hfreq : ∃ᶠ (n : ι) in l, ¬x n ∈ s
y : ℕ → ι
hy_tendsto : Tendsto y atTop l
hy_freq : ∀ (n : ℕ), ¬x (y n) ∈ s
ms : ℕ → ℕ
hms_tendsto : (fun n => x (y (ms n))) ⁻¹' s ∈ atTop
hms_freq : ∀ (n : ℕ), ¬x (y (ms n)) ∈ s
n : ℕ
⊢ n ∈ (fun n => x (y (ms n))) ⁻¹' s ↔ n ∈ ∅
ι✝ : Type ?u.372453
ι' : Type ?u.372456
α✝ : Type ?u.372459
β : Type ?u.372462
γ : Type ?u.372465
α : Type u_1
ι : Type u_2
x : ι → α
f : Filter α
l : Filter ι
inst✝ : IsCountablyGenerated l
h : ¬Tendsto x l f
s : Set α
hs : s ∈ f
hfreq : ∃ᶠ (n : ι) in l, ¬x n ∈ s
y : ℕ → ι
hy_tendsto : Tendsto y atTop l
hy_freq : ∀ (n : ℕ), ¬x (y n) ∈ s
ms : ℕ → ℕ
hms_tendsto : (fun n => x (y (ms n))) ⁻¹' s ∈ atTop
hms_freq : ∀ (n : ℕ), ¬x (y (ms n)) ∈ s
⊢ (fun n => x (y (ms n))) ⁻¹' s = ∅
ext1 n
case h
ι✝ : Type ?u.372453
ι' : Type ?u.372456
α✝ : Type ?u.372459
β : Type ?u.372462
γ : Type ?u.372465
α : Type u_1
ι : Type u_2
x : ι → α
f : Filter α
l : Filter ι
inst✝ : IsCountablyGenerated l
h : ¬Tendsto x l f
s : Set α
hs : s ∈ f
hfreq : ∃ᶠ (n : ι) in l, ¬x n ∈ s
y : ℕ → ι
hy_tendsto : Tendsto y atTop l
hy_freq : ∀ (n : ℕ), ¬x (y n) ∈ s
ms : ℕ → ℕ
hms_tendsto : (fun n => x (y (ms n))) ⁻¹' s ∈ atTop
hms_freq : ∀ (n : ℕ), ¬x (y (ms n)) ∈ s
n : ℕ
⊢ ¬x (y (ms n)) ∈ s
case h
ι✝ : Type ?u.372453
ι' : Type ?u.372456
α✝ : Type ?u.372459
β : Type ?u.372462
γ : Type ?u.372465
α : Type u_1
ι : Type u_2
x : ι → α
f : Filter α
l : Filter ι
inst✝ : IsCountablyGenerated l
h : ¬Tendsto x l f
s : Set α
hs : s ∈ f
hfreq : ∃ᶠ (n : ι) in l, ¬x n ∈ s
y : ℕ → ι
hy_tendsto : Tendsto y atTop l
hy_freq : ∀ (n : ℕ), ¬x (y n) ∈ s
ms : ℕ → ℕ
hms_tendsto : (fun n => x (y (ms n))) ⁻¹' s ∈ atTop
hms_freq : ∀ (n : ℕ), ¬x (y (ms n)) ∈ s
n : ℕ
⊢ n ∈ (fun n => x (y (ms n))) ⁻¹' s ↔ n ∈ ∅
simp only [Set.mem_preimage, Set.mem_empty_iff_false, iff_false_iff]
no goals
case h
ι✝ : Type ?u.372453
ι' : Type ?u.372456
α✝ : Type ?u.372459
β : Type ?u.372462
γ : Type ?u.372465
α : Type u_1
ι : Type u_2
x : ι → α
f : Filter α
l : Filter ι
inst✝ : IsCountablyGenerated l
h : ¬Tendsto x l f
s : Set α
hs : s ∈ f
hfreq : ∃ᶠ (n : ι) in l, ¬x n ∈ s
y : ℕ → ι
hy_tendsto : Tendsto y atTop l
hy_freq : ∀ (n : ℕ), ¬x (y n) ∈ s
ms : ℕ → ℕ
hms_tendsto : (fun n => x (y (ms n))) ⁻¹' s ∈ atTop
hms_freq : ∀ (n : ℕ), ¬x (y (ms n)) ∈ s
n : ℕ
⊢ ¬x (y (ms n)) ∈ s
exact hms_freq n