case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : OrderTopology α
inst✝¹ : OrderTopology β
t : Set α
x : α
inst✝ : IsCountablyGenerated (𝓝 x)
htx : IsLUB t x
not_mem : ¬x ∈ t
ht : Set.Nonempty t
v : ℕ → α
hvx : Tendsto v atTop (𝓝[Iic x] x)
hvt : ∀ (n : ℕ), v n ∈ t
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
α : Type u
β : Type v
γ : Type w
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : OrderTopology α
inst✝¹ : OrderTopology β
t : Set α
x : α
inst✝ : IsCountablyGenerated (𝓝 x)
htx : IsLUB t x
not_mem : ¬x ∈ t
ht : Set.Nonempty t
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
obtain ⟨v, hvx, hvt⟩ := exists_seq_forall_of_frequently (htx.frequently_mem ht)
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : OrderTopology α
inst✝¹ : OrderTopology β
t : Set α
x : α
inst✝ : IsCountablyGenerated (𝓝 x)
htx : IsLUB t x
not_mem : ¬x ∈ t
ht : Set.Nonempty t
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : OrderTopology α
inst✝¹ : OrderTopology β
t : Set α
x : α
inst✝ : IsCountablyGenerated (𝓝 x)
htx : IsLUB t x
not_mem : ¬x ∈ t
ht : Set.Nonempty t
v : ℕ → α
hvx : Tendsto v atTop (𝓝[Iic x] x)
hvt : ∀ (n : ℕ), v n ∈ t
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
replace hvx := hvx.mono_right nhdsWithin_le_nhds
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : OrderTopology α
inst✝¹ : OrderTopology β
t : Set α
x : α
inst✝ : IsCountablyGenerated (𝓝 x)
htx : IsLUB t x
not_mem : ¬x ∈ t
ht : Set.Nonempty t
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : OrderTopology α
inst✝¹ : OrderTopology β
t : Set α
x : α
inst✝ : IsCountablyGenerated (𝓝 x)
htx : IsLUB t x
not_mem : ¬x ∈ t
ht : Set.Nonempty t
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
have hvx' : ∀ {n}, v n < x := (htx.1 (hvt _)).lt_of_ne (ne_of_mem_of_not_mem (hvt _) not_mem)
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : OrderTopology α
inst✝¹ : OrderTopology β
t : Set α
x : α
inst✝ : IsCountablyGenerated (𝓝 x)
htx : IsLUB t x
not_mem : ¬x ∈ t
ht : Set.Nonempty t
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : OrderTopology α
inst✝¹ : OrderTopology β
t : Set α
x : α
inst✝ : IsCountablyGenerated (𝓝 x)
htx : IsLUB t x
not_mem : ¬x ∈ t
ht : Set.Nonempty t
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
have : ∀ k, ∀ᶠ l in atTop, v k < v l := fun k => hvx.eventually (lt_mem_nhds hvx')
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : OrderTopology α
inst✝¹ : OrderTopology β
t : Set α
x : α
inst✝ : IsCountablyGenerated (𝓝 x)
htx : IsLUB t x
not_mem : ¬x ∈ t
ht : Set.Nonempty t
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < N k
hvN : ∀ (k : ℕ), v k < v (N k)
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : OrderTopology α
inst✝¹ : OrderTopology β
t : Set α
x : α
inst✝ : IsCountablyGenerated (𝓝 x)
htx : IsLUB t x
not_mem : ¬x ∈ t
ht : Set.Nonempty t
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
choose N hN hvN using fun k => ((eventually_gt_atTop k).and (this k)).exists
case intro.intro.refine_1
α : Type u
β : Type v
γ : Type w
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : OrderTopology α
inst✝¹ : OrderTopology β
t : Set α
x : α
inst✝ : IsCountablyGenerated (𝓝 x)
htx : IsLUB t x
not_mem : ¬x ∈ t
ht : Set.Nonempty t
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < N k
hvN : ∀ (k : ℕ), v k < v (N k)
x✝ : ℕ
⊢ v ((N^[x✝]) 0) < v ((N^[x✝ + 1]) 0)

case intro.intro.refine_2
α : Type u
β : Type v
γ : Type w
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : OrderTopology α
inst✝¹ : OrderTopology β
t : Set α
x : α
inst✝ : IsCountablyGenerated (𝓝 x)
htx : IsLUB t x
not_mem : ¬x ∈ t
ht : Set.Nonempty t
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < N k
hvN : ∀ (k : ℕ), v k < v (N k)
x✝ : ℕ
⊢ (N^[x✝]) 0 < (N^[x✝ + 1]) 0
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : OrderTopology α
inst✝¹ : OrderTopology β
t : Set α
x : α
inst✝ : IsCountablyGenerated (𝓝 x)
htx : IsLUB t x
not_mem : ¬x ∈ t
ht : Set.Nonempty t
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < N k
hvN : ∀ (k : ℕ), v k < v (N k)
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
refine ⟨fun k => v ((N^[k]) 0), strictMono_nat_of_lt_succ fun _ => ?_, fun _ => hvx',
  hvx.comp (strictMono_nat_of_lt_succ fun _ => ?_).tendsto_atTop, fun _ => hvt _⟩
case intro.intro.refine_1
α : Type u
β : Type v
γ : Type w
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : OrderTopology α
inst✝¹ : OrderTopology β
t : Set α
x : α
inst✝ : IsCountablyGenerated (𝓝 x)
htx : IsLUB t x
not_mem : ¬x ∈ t
ht : Set.Nonempty t
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < N k
hvN : ∀ (k : ℕ), v k < v (N k)
x✝ : ℕ
⊢ v ((N^[x✝]) 0) < v (N ((N^[x✝]) 0))
case intro.intro.refine_1
α : Type u
β : Type v
γ : Type w
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : OrderTopology α
inst✝¹ : OrderTopology β
t : Set α
x : α
inst✝ : IsCountablyGenerated (𝓝 x)
htx : IsLUB t x
not_mem : ¬x ∈ t
ht : Set.Nonempty t
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < N k
hvN : ∀ (k : ℕ), v k < v (N k)
x✝ : ℕ
⊢ v ((N^[x✝]) 0) < v ((N^[x✝ + 1]) 0)
rw [iterate_succ_apply']
no goals
case intro.intro.refine_1
α : Type u
β : Type v
γ : Type w
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : OrderTopology α
inst✝¹ : OrderTopology β
t : Set α
x : α
inst✝ : IsCountablyGenerated (𝓝 x)
htx : IsLUB t x
not_mem : ¬x ∈ t
ht : Set.Nonempty t
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < N k
hvN : ∀ (k : ℕ), v k < v (N k)
x✝ : ℕ
⊢ v ((N^[x✝]) 0) < v (N ((N^[x✝]) 0))
exact hvN _
case intro.intro.refine_2
α : Type u
β : Type v
γ : Type w
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : OrderTopology α
inst✝¹ : OrderTopology β
t : Set α
x : α
inst✝ : IsCountablyGenerated (𝓝 x)
htx : IsLUB t x
not_mem : ¬x ∈ t
ht : Set.Nonempty t
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < N k
hvN : ∀ (k : ℕ), v k < v (N k)
x✝ : ℕ
⊢ (N^[x✝]) 0 < N ((N^[x✝]) 0)
case intro.intro.refine_2
α : Type u
β : Type v
γ : Type w
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : OrderTopology α
inst✝¹ : OrderTopology β
t : Set α
x : α
inst✝ : IsCountablyGenerated (𝓝 x)
htx : IsLUB t x
not_mem : ¬x ∈ t
ht : Set.Nonempty t
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < N k
hvN : ∀ (k : ℕ), v k < v (N k)
x✝ : ℕ
⊢ (N^[x✝]) 0 < (N^[x✝ + 1]) 0
rw [iterate_succ_apply']
no goals
case intro.intro.refine_2
α : Type u
β : Type v
γ : Type w
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : OrderTopology α
inst✝¹ : OrderTopology β
t : Set α
x : α
inst✝ : IsCountablyGenerated (𝓝 x)
htx : IsLUB t x
not_mem : ¬x ∈ t
ht : Set.Nonempty t
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < N k
hvN : ∀ (k : ℕ), v k < v (N k)
x✝ : ℕ
⊢ (N^[x✝]) 0 < N ((N^[x✝]) 0)
exact hN _