case intro
ι : Type ?u.373995
ι' : Type ?u.373998
α : Type u_1
β : Type ?u.374004
γ : Type ?u.374007
f : Filter α
inst✝ : IsCountablyGenerated f
u : ℕ → α
hx : NeBot (f ⊓ map u atTop)
B : ℕ → Set α
h : HasAntitoneBasis f B
⊢ ∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f
ι : Type ?u.373995
ι' : Type ?u.373998
α : Type u_1
β : Type ?u.374004
γ : Type ?u.374007
f : Filter α
inst✝ : IsCountablyGenerated f
u : ℕ → α
hx : NeBot (f ⊓ map u atTop)
⊢ ∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f
obtain ⟨B, h⟩ := f.exists_antitone_basis
case intro
ι : Type ?u.373995
ι' : Type ?u.373998
α : Type u_1
β : Type ?u.374004
γ : Type ?u.374007
f : Filter α
inst✝ : IsCountablyGenerated f
u : ℕ → α
hx : NeBot (f ⊓ map u atTop)
B : ℕ → Set α
h : HasAntitoneBasis f B
this : ∀ (N : ℕ), ∃ n, n ≥ N ∧ u n ∈ B N
⊢ ∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f
case intro
ι : Type ?u.373995
ι' : Type ?u.373998
α : Type u_1
β : Type ?u.374004
γ : Type ?u.374007
f : Filter α
inst✝ : IsCountablyGenerated f
u : ℕ → α
hx : NeBot (f ⊓ map u atTop)
B : ℕ → Set α
h : HasAntitoneBasis f B
⊢ ∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f
have : ∀ N, ∃ n ≥ N, u n ∈ B N := fun N =>
  Filter.inf_map_atTop_neBot_iff.mp hx _ (h.1.mem_of_mem trivial) N
case intro
ι : Type ?u.373995
ι' : Type ?u.373998
α : Type u_1
β : Type ?u.374004
γ : Type ?u.374007
f : Filter α
inst✝ : IsCountablyGenerated f
u : ℕ → α
hx : NeBot (f ⊓ map u atTop)
B : ℕ → Set α
h : HasAntitoneBasis f B
φ : ℕ → ℕ
hφ : ∀ (N : ℕ), φ N ≥ N ∧ u (φ N) ∈ B N
⊢ ∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f
case intro
ι : Type ?u.373995
ι' : Type ?u.373998
α : Type u_1
β : Type ?u.374004
γ : Type ?u.374007
f : Filter α
inst✝ : IsCountablyGenerated f
u : ℕ → α
hx : NeBot (f ⊓ map u atTop)
B : ℕ → Set α
h : HasAntitoneBasis f B
this : ∀ (N : ℕ), ∃ n, n ≥ N ∧ u n ∈ B N
⊢ ∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f
choose φ hφ using this
case intro.intro
ι : Type ?u.373995
ι' : Type ?u.373998
α : Type u_1
β : Type ?u.374004
γ : Type ?u.374007
f : Filter α
inst✝ : IsCountablyGenerated f
u : ℕ → α
hx : NeBot (f ⊓ map u atTop)
B : ℕ → Set α
h : HasAntitoneBasis f B
φ : ℕ → ℕ
hφ : ∀ (N : ℕ), φ N ≥ N ∧ u (φ N) ∈ B N
φ_ge : ∀ (x : ℕ), φ x ≥ x
φ_in : ∀ (x : ℕ), u (φ x) ∈ B x
⊢ ∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f
case intro
ι : Type ?u.373995
ι' : Type ?u.373998
α : Type u_1
β : Type ?u.374004
γ : Type ?u.374007
f : Filter α
inst✝ : IsCountablyGenerated f
u : ℕ → α
hx : NeBot (f ⊓ map u atTop)
B : ℕ → Set α
h : HasAntitoneBasis f B
φ : ℕ → ℕ
hφ : ∀ (N : ℕ), φ N ≥ N ∧ u (φ N) ∈ B N
⊢ ∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f
cases' forall_and.mp hφ with φ_ge φ_in
case intro.intro
ι : Type ?u.373995
ι' : Type ?u.373998
α : Type u_1
β : Type ?u.374004
γ : Type ?u.374007
f : Filter α
inst✝ : IsCountablyGenerated f
u : ℕ → α
hx : NeBot (f ⊓ map u atTop)
B : ℕ → Set α
h : HasAntitoneBasis f B
φ : ℕ → ℕ
hφ : ∀ (N : ℕ), φ N ≥ N ∧ u (φ N) ∈ B N
φ_ge : ∀ (x : ℕ), φ x ≥ x
φ_in : ∀ (x : ℕ), u (φ x) ∈ B x
lim_uφ : Tendsto (u ∘ φ) atTop f
⊢ ∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f
case intro.intro
ι : Type ?u.373995
ι' : Type ?u.373998
α : Type u_1
β : Type ?u.374004
γ : Type ?u.374007
f : Filter α
inst✝ : IsCountablyGenerated f
u : ℕ → α
hx : NeBot (f ⊓ map u atTop)
B : ℕ → Set α
h : HasAntitoneBasis f B
φ : ℕ → ℕ
hφ : ∀ (N : ℕ), φ N ≥ N ∧ u (φ N) ∈ B N
φ_ge : ∀ (x : ℕ), φ x ≥ x
φ_in : ∀ (x : ℕ), u (φ x) ∈ B x
⊢ ∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f
have lim_uφ : Tendsto (u ∘ φ) atTop f := h.tendsto φ_in
case intro.intro
ι : Type ?u.373995
ι' : Type ?u.373998
α : Type u_1
β : Type ?u.374004
γ : Type ?u.374007
f : Filter α
inst✝ : IsCountablyGenerated f
u : ℕ → α
hx : NeBot (f ⊓ map u atTop)
B : ℕ → Set α
h : HasAntitoneBasis f B
φ : ℕ → ℕ
hφ : ∀ (N : ℕ), φ N ≥ N ∧ u (φ N) ∈ B N
φ_ge : ∀ (x : ℕ), φ x ≥ x
φ_in : ∀ (x : ℕ), u (φ x) ∈ B x
lim_uφ : Tendsto (u ∘ φ) atTop f
lim_φ : Tendsto φ atTop atTop
⊢ ∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f
case intro.intro
ι : Type ?u.373995
ι' : Type ?u.373998
α : Type u_1
β : Type ?u.374004
γ : Type ?u.374007
f : Filter α
inst✝ : IsCountablyGenerated f
u : ℕ → α
hx : NeBot (f ⊓ map u atTop)
B : ℕ → Set α
h : HasAntitoneBasis f B
φ : ℕ → ℕ
hφ : ∀ (N : ℕ), φ N ≥ N ∧ u (φ N) ∈ B N
φ_ge : ∀ (x : ℕ), φ x ≥ x
φ_in : ∀ (x : ℕ), u (φ x) ∈ B x
lim_uφ : Tendsto (u ∘ φ) atTop f
⊢ ∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f
have lim_φ : Tendsto φ atTop atTop := tendsto_atTop_mono φ_ge tendsto_id
ι : Type ?u.373995
ι' : Type ?u.373998
α : Type u_1
β : Type ?u.374004
γ : Type ?u.374007
f : Filter α
inst✝ : IsCountablyGenerated f
u : ℕ → α
hx : NeBot (f ⊓ map u atTop)
B : ℕ → Set α
h : HasAntitoneBasis f B
φ : ℕ → ℕ
hφ : ∀ (N : ℕ), φ N ≥ N ∧ u (φ N) ∈ B N
φ_ge : ∀ (x : ℕ), φ x ≥ x
φ_in : ∀ (x : ℕ), u (φ x) ∈ B x
lim_uφ : Tendsto (u ∘ φ) atTop f
lim_φ : Tendsto φ atTop atTop
⊢ ∃ ψ, StrictMono ψ ∧ StrictMono (φ ∘ ψ)

case intro.intro.intro.intro
ι : Type ?u.373995
ι' : Type ?u.373998
α : Type u_1
β : Type ?u.374004
γ : Type ?u.374007
f : Filter α
inst✝ : IsCountablyGenerated f
u : ℕ → α
hx : NeBot (f ⊓ map u atTop)
B : ℕ → Set α
h : HasAntitoneBasis f B
φ : ℕ → ℕ
hφ : ∀ (N : ℕ), φ N ≥ N ∧ u (φ N) ∈ B N
φ_ge : ∀ (x : ℕ), φ x ≥ x
φ_in : ∀ (x : ℕ), u (φ x) ∈ B x
lim_uφ : Tendsto (u ∘ φ) atTop f
lim_φ : Tendsto φ atTop atTop
ψ : ℕ → ℕ
hψ : StrictMono ψ
hψφ : StrictMono (φ ∘ ψ)
⊢ ∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f
case intro.intro
ι : Type ?u.373995
ι' : Type ?u.373998
α : Type u_1
β : Type ?u.374004
γ : Type ?u.374007
f : Filter α
inst✝ : IsCountablyGenerated f
u : ℕ → α
hx : NeBot (f ⊓ map u atTop)
B : ℕ → Set α
h : HasAntitoneBasis f B
φ : ℕ → ℕ
hφ : ∀ (N : ℕ), φ N ≥ N ∧ u (φ N) ∈ B N
φ_ge : ∀ (x : ℕ), φ x ≥ x
φ_in : ∀ (x : ℕ), u (φ x) ∈ B x
lim_uφ : Tendsto (u ∘ φ) atTop f
lim_φ : Tendsto φ atTop atTop
⊢ ∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f
obtain ⟨ψ, hψ, hψφ⟩ : ∃ ψ : ℕ → ℕ, StrictMono ψ ∧ StrictMono (φ ∘ ψ)
case intro.intro.intro.intro
ι : Type ?u.373995
ι' : Type ?u.373998
α : Type u_1
β : Type ?u.374004
γ : Type ?u.374007
f : Filter α
inst✝ : IsCountablyGenerated f
u : ℕ → α
hx : NeBot (f ⊓ map u atTop)
B : ℕ → Set α
h : HasAntitoneBasis f B
φ : ℕ → ℕ
hφ : ∀ (N : ℕ), φ N ≥ N ∧ u (φ N) ∈ B N
φ_ge : ∀ (x : ℕ), φ x ≥ x
φ_in : ∀ (x : ℕ), u (φ x) ∈ B x
lim_uφ : Tendsto (u ∘ φ) atTop f
lim_φ : Tendsto φ atTop atTop
ψ : ℕ → ℕ
hψ : StrictMono ψ
hψφ : StrictMono (φ ∘ ψ)
⊢ ∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f
ι : Type ?u.373995
ι' : Type ?u.373998
α : Type u_1
β : Type ?u.374004
γ : Type ?u.374007
f : Filter α
inst✝ : IsCountablyGenerated f
u : ℕ → α
hx : NeBot (f ⊓ map u atTop)
B : ℕ → Set α
h : HasAntitoneBasis f B
φ : ℕ → ℕ
hφ : ∀ (N : ℕ), φ N ≥ N ∧ u (φ N) ∈ B N
φ_ge : ∀ (x : ℕ), φ x ≥ x
φ_in : ∀ (x : ℕ), u (φ x) ∈ B x
lim_uφ : Tendsto (u ∘ φ) atTop f
lim_φ : Tendsto φ atTop atTop
⊢ ∃ ψ, StrictMono ψ ∧ StrictMono (φ ∘ ψ)

case intro.intro.intro.intro
ι : Type ?u.373995
ι' : Type ?u.373998
α : Type u_1
β : Type ?u.374004
γ : Type ?u.374007
f : Filter α
inst✝ : IsCountablyGenerated f
u : ℕ → α
hx : NeBot (f ⊓ map u atTop)
B : ℕ → Set α
h : HasAntitoneBasis f B
φ : ℕ → ℕ
hφ : ∀ (N : ℕ), φ N ≥ N ∧ u (φ N) ∈ B N
φ_ge : ∀ (x : ℕ), φ x ≥ x
φ_in : ∀ (x : ℕ), u (φ x) ∈ B x
lim_uφ : Tendsto (u ∘ φ) atTop f
lim_φ : Tendsto φ atTop atTop
ψ : ℕ → ℕ
hψ : StrictMono ψ
hψφ : StrictMono (φ ∘ ψ)
⊢ ∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f
exact strictMono_subseq_of_tendsto_atTop lim_φ
no goals
case intro.intro.intro.intro
ι : Type ?u.373995
ι' : Type ?u.373998
α : Type u_1
β : Type ?u.374004
γ : Type ?u.374007
f : Filter α
inst✝ : IsCountablyGenerated f
u : ℕ → α
hx : NeBot (f ⊓ map u atTop)
B : ℕ → Set α
h : HasAntitoneBasis f B
φ : ℕ → ℕ
hφ : ∀ (N : ℕ), φ N ≥ N ∧ u (φ N) ∈ B N
φ_ge : ∀ (x : ℕ), φ x ≥ x
φ_in : ∀ (x : ℕ), u (φ x) ∈ B x
lim_uφ : Tendsto (u ∘ φ) atTop f
lim_φ : Tendsto φ atTop atTop
ψ : ℕ → ℕ
hψ : StrictMono ψ
hψφ : StrictMono (φ ∘ ψ)
⊢ ∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f
exact ⟨φ ∘ ψ, hψφ, lim_uφ.comp hψ.tendsto_atTop⟩