α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
⊢ ∃ xs, Monotone xs ∧ Tendsto xs atTop atTop
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
⊢ ∃ xs, Monotone xs ∧ Tendsto xs atTop atTop
haveI h_ne_bot : (atTop : Filter α).NeBot := atTop_neBot
case intro
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
⊢ ∃ xs, Monotone xs ∧ Tendsto xs atTop atTop
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
⊢ ∃ xs, Monotone xs ∧ Tendsto xs atTop atTop
obtain ⟨ys, h⟩ := exists_seq_tendsto (atTop : Filter α)
case intro
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
⊢ ∃ xs, Monotone xs ∧ Tendsto xs atTop atTop
case intro
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
⊢ ∃ xs, Monotone xs ∧ Tendsto xs atTop atTop
let xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) Finset.nonempty_range_succ ys
case intro
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
h_mono : Monotone xs
⊢ ∃ xs, Monotone xs ∧ Tendsto xs atTop atTop
case intro
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
⊢ ∃ xs, Monotone xs ∧ Tendsto xs atTop atTop
have h_mono : Monotone xs := by
  intro i j hij
  rw [Finset.sup'_le_iff]
  intro k hk
  refine' Finset.le_sup'_of_le _ _ le_rfl
  rw [Finset.mem_range] at hk⊢
  exact hk.trans_le (add_le_add_right hij _)
case intro
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
h_mono : Monotone xs
⊢ Tendsto xs atTop atTop
case intro
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
h_mono : Monotone xs
⊢ ∃ xs, Monotone xs ∧ Tendsto xs atTop atTop
refine' ⟨xs, h_mono, _⟩
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
i j : ℕ
hij : i ≤ j
⊢ xs i ≤ xs j
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
⊢ Monotone xs
intro i j hij
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
i j : ℕ
hij : i ≤ j
⊢ ∀ (b : ℕ), b ∈ Finset.range (i + 1) → ys b ≤ xs j
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
i j : ℕ
hij : i ≤ j
⊢ xs i ≤ xs j
rw [Finset.sup'_le_iff]
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
i j : ℕ
hij : i ≤ j
k : ℕ
hk : k ∈ Finset.range (i + 1)
⊢ ys k ≤ xs j
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
i j : ℕ
hij : i ≤ j
⊢ ∀ (b : ℕ), b ∈ Finset.range (i + 1) → ys b ≤ xs j
intro k hk
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
i j : ℕ
hij : i ≤ j
k : ℕ
hk : k ∈ Finset.range (i + 1)
⊢ k ∈ Finset.range (j + 1)
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
i j : ℕ
hij : i ≤ j
k : ℕ
hk : k ∈ Finset.range (i + 1)
⊢ ys k ≤ xs j
refine' Finset.le_sup'_of_le _ _ le_rfl
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
i j : ℕ
hij : i ≤ j
k : ℕ
hk : k < i + 1
⊢ k < j + 1
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
i j : ℕ
hij : i ≤ j
k : ℕ
hk : k ∈ Finset.range (i + 1)
⊢ k ∈ Finset.range (j + 1)
rw [Finset.mem_range] at hk⊢
no goals
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
i j : ℕ
hij : i ≤ j
k : ℕ
hk : k < i + 1
⊢ k < j + 1
exact hk.trans_le (add_le_add_right hij _)
case intro
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
h_mono : Monotone xs
⊢ ∀ (b : α), ∃ a, b ≤ xs a
case intro
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
h_mono : Monotone xs
⊢ Tendsto xs atTop atTop
refine' tendsto_atTop_atTop_of_monotone h_mono _
case intro
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
h_mono : Monotone xs
this : ∀ (a : α), ∃ n, a ≤ ys n
⊢ ∀ (b : α), ∃ a, b ≤ xs a
case intro
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
h_mono : Monotone xs
⊢ ∀ (b : α), ∃ a, b ≤ xs a
have : ∀ a : α, ∃ n : ℕ, a ≤ ys n := by
  rw [tendsto_atTop_atTop] at h
  intro a
  obtain ⟨i, hi⟩ := h a
  exact ⟨i, hi i le_rfl⟩
case intro
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
h_mono : Monotone xs
this : ∀ (a : α), ∃ n, a ≤ ys n
a : α
⊢ ∃ a_1, a ≤ xs a_1
case intro
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
h_mono : Monotone xs
this : ∀ (a : α), ∃ n, a ≤ ys n
⊢ ∀ (b : α), ∃ a, b ≤ xs a
intro a
case intro.intro
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
h_mono : Monotone xs
this : ∀ (a : α), ∃ n, a ≤ ys n
a : α
i : ℕ
hi : a ≤ ys i
⊢ ∃ a_1, a ≤ xs a_1
case intro
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
h_mono : Monotone xs
this : ∀ (a : α), ∃ n, a ≤ ys n
a : α
⊢ ∃ a_1, a ≤ xs a_1
obtain ⟨i, hi⟩ := this a
case intro.intro
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
h_mono : Monotone xs
this : ∀ (a : α), ∃ n, a ≤ ys n
a : α
i : ℕ
hi : a ≤ ys i
⊢ ys i ≤ xs i
case intro.intro
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
h_mono : Monotone xs
this : ∀ (a : α), ∃ n, a ≤ ys n
a : α
i : ℕ
hi : a ≤ ys i
⊢ ∃ a_1, a ≤ xs a_1
refine' ⟨i, hi.trans _⟩
case intro.intro
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
h_mono : Monotone xs
this : ∀ (a : α), ∃ n, a ≤ ys n
a : α
i : ℕ
hi : a ≤ ys i
⊢ i ∈ Finset.range (i + 1)
case intro.intro
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
h_mono : Monotone xs
this : ∀ (a : α), ∃ n, a ≤ ys n
a : α
i : ℕ
hi : a ≤ ys i
⊢ ys i ≤ xs i
refine' Finset.le_sup'_of_le _ _ le_rfl
no goals
case intro.intro
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
h_mono : Monotone xs
this : ∀ (a : α), ∃ n, a ≤ ys n
a : α
i : ℕ
hi : a ≤ ys i
⊢ i ∈ Finset.range (i + 1)
rw [Finset.mem_range_succ_iff]
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : ∀ (b : α), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ys a
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
h_mono : Monotone xs
⊢ ∀ (a : α), ∃ n, a ≤ ys n
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
h_mono : Monotone xs
⊢ ∀ (a : α), ∃ n, a ≤ ys n
rw [tendsto_atTop_atTop] at h
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : ∀ (b : α), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ys a
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
h_mono : Monotone xs
a : α
⊢ ∃ n, a ≤ ys n
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : ∀ (b : α), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ys a
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
h_mono : Monotone xs
⊢ ∀ (a : α), ∃ n, a ≤ ys n
intro a
case intro
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : ∀ (b : α), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ys a
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
h_mono : Monotone xs
a : α
i : ℕ
hi : ∀ (a_1 : ℕ), i ≤ a_1 → a ≤ ys a_1
⊢ ∃ n, a ≤ ys n
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : ∀ (b : α), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ys a
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
h_mono : Monotone xs
a : α
⊢ ∃ n, a ≤ ys n
obtain ⟨i, hi⟩ := h a
no goals
case intro
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : ∀ (b : α), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ys a
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
h_mono : Monotone xs
a : α
i : ℕ
hi : ∀ (a_1 : ℕ), i ≤ a_1 → a ≤ ys a_1
⊢ ∃ n, a ≤ ys n
exact ⟨i, hi i le_rfl⟩