-- Mathlib/Order/Filter/AtTopBot/CountablyGenerated.lean
theorem exists_seq_monotone_tendsto_atTop_atTop (α : Type*) [Preorder α] [Nonempty α]
    [IsDirected α (· ≤ ·)] [(atTop : Filter α).IsCountablyGenerated] :
    ∃ xs : ℕ → α, Monotone xs ∧ Tendsto xs atTop atTop

Proof state:
case intro
α : Type u_3
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝ : atTop.IsCountablyGenerated
ys : ℕ → α
h : Tendsto ys atTop atTop
c : α → α → α
hleft : ∀ (a b : α), a ≤ c a b
hright : ∀ (a b : α), b ≤ c a b
xs : ℕ → α := fun n => List.foldl (fun x n => c x (ys n)) (ys 0) (List.range n)
⊢ ∃ xs, Monotone xs ∧ Tendsto xs atTop atTop

Tactic:
have hsucc (n : ℕ) : xs (n + 1) = c (xs n) (ys n) := by simp [xs, List.range_succ]

Result:
case intro
α : Type u_3
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝ : atTop.IsCountablyGenerated
ys : ℕ → α
h : Tendsto ys atTop atTop
c : α → α → α
hleft : ∀ (a b : α), a ≤ c a b
hright : ∀ (a b : α), b ≤ c a b
xs : ℕ → α := fun n => List.foldl (fun x n => c x (ys n)) (ys 0) (List.range n)
hsucc : ∀ (n : ℕ), xs (n + 1) = c (xs n) (ys n)
⊢ ∃ xs, Monotone xs ∧ Tendsto xs atTop atTop

Proof state:
case intro.refine_2
α : Type u_3
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝ : atTop.IsCountablyGenerated
ys : ℕ → α
h : Tendsto ys atTop atTop
c : α → α → α
hleft : ∀ (a b : α), a ≤ c a b
hright : ∀ (a b : α), b ≤ c a b
xs : ℕ → α := fun n => List.foldl (fun x n => c x (ys n)) (ys 0) (List.range n)
hsucc : ∀ (n : ℕ), xs (n + 1) = c (xs n) (ys n)
n : ℕ
⊢ ys n ≤ xs (n + 1)

Tactic:
rw [hsucc]

Result:
case intro.refine_2
α : Type u_3
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝ : atTop.IsCountablyGenerated
ys : ℕ → α
h : Tendsto ys atTop atTop
c : α → α → α
hleft : ∀ (a b : α), a ≤ c a b
hright : ∀ (a b : α), b ≤ c a b
xs : ℕ → α := fun n => List.foldl (fun x n => c x (ys n)) (ys 0) (List.range n)
hsucc : ∀ (n : ℕ), xs (n + 1) = c (xs n) (ys n)
n : ℕ
⊢ ys n ≤ c (xs n) (ys n)

Proof state:
case intro.refine_1
α : Type u_3
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝ : atTop.IsCountablyGenerated
ys : ℕ → α
h : Tendsto ys atTop atTop
c : α → α → α
hleft : ∀ (a b : α), a ≤ c a b
hright : ∀ (a b : α), b ≤ c a b
xs : ℕ → α := fun n => List.foldl (fun x n => c x (ys n)) (ys 0) (List.range n)
hsucc : ∀ (n : ℕ), xs (n + 1) = c (xs n) (ys n)
⊢ Monotone xs

Tactic:
refine monotone_nat_of_le_succ fun n ↦ ?_

Result:
case intro.refine_1
α : Type u_3
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝ : atTop.IsCountablyGenerated
ys : ℕ → α
h : Tendsto ys atTop atTop
c : α → α → α
hleft : ∀ (a b : α), a ≤ c a b
hright : ∀ (a b : α), b ≤ c a b
xs : ℕ → α := fun n => List.foldl (fun x n => c x (ys n)) (ys 0) (List.range n)
hsucc : ∀ (n : ℕ), xs (n + 1) = c (xs n) (ys n)
n : ℕ
⊢ xs n ≤ xs (n + 1)

Proof state:
case intro
α : Type u_3
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝ : atTop.IsCountablyGenerated
ys : ℕ → α
h : Tendsto ys atTop atTop
c : α → α → α
hleft : ∀ (a b : α), a ≤ c a b
hright : ∀ (a b : α), b ≤ c a b
⊢ ∃ xs, Monotone xs ∧ Tendsto xs atTop atTop

Tactic:
set xs : ℕ → α := fun n => (List.range n).foldl (fun x n ↦ c x (ys n)) (ys 0)

Result:
case intro
α : Type u_3
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝ : atTop.IsCountablyGenerated
ys : ℕ → α
h : Tendsto ys atTop atTop
c : α → α → α
hleft : ∀ (a b : α), a ≤ c a b
hright : ∀ (a b : α), b ≤ c a b
xs : ℕ → α := fun n => List.foldl (fun x n => c x (ys n)) (ys 0) (List.range n)
⊢ ∃ xs, Monotone xs ∧ Tendsto xs atTop atTop

Proof state:
case intro.refine_1
α : Type u_3
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝ : atTop.IsCountablyGenerated
ys : ℕ → α
h : Tendsto ys atTop atTop
c : α → α → α
hleft : ∀ (a b : α), a ≤ c a b
hright : ∀ (a b : α), b ≤ c a b
xs : ℕ → α := fun n => List.foldl (fun x n => c x (ys n)) (ys 0) (List.range n)
hsucc : ∀ (n : ℕ), xs (n + 1) = c (xs n) (ys n)
n : ℕ
⊢ xs n ≤ xs (n + 1)

Tactic:
rw [hsucc]

Result:
case intro.refine_1
α : Type u_3
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝ : atTop.IsCountablyGenerated
ys : ℕ → α
h : Tendsto ys atTop atTop
c : α → α → α
hleft : ∀ (a b : α), a ≤ c a b
hright : ∀ (a b : α), b ≤ c a b
xs : ℕ → α := fun n => List.foldl (fun x n => c x (ys n)) (ys 0) (List.range n)
hsucc : ∀ (n : ℕ), xs (n + 1) = c (xs n) (ys n)
n : ℕ
⊢ xs n ≤ c (xs n) (ys n)

Proof state:
case intro.refine_2
α : Type u_3
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝ : atTop.IsCountablyGenerated
ys : ℕ → α
h : Tendsto ys atTop atTop
c : α → α → α
hleft : ∀ (a b : α), a ≤ c a b
hright : ∀ (a b : α), b ≤ c a b
xs : ℕ → α := fun n => List.foldl (fun x n => c x (ys n)) (ys 0) (List.range n)
hsucc : ∀ (n : ℕ), xs (n + 1) = c (xs n) (ys n)
⊢ Tendsto xs atTop atTop

Tactic:
refine (tendsto_add_atTop_iff_nat 1).1 <| tendsto_atTop_mono (fun n ↦ ?_) h

Result:
case intro.refine_2
α : Type u_3
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝ : atTop.IsCountablyGenerated
ys : ℕ → α
h : Tendsto ys atTop atTop
c : α → α → α
hleft : ∀ (a b : α), a ≤ c a b
hright : ∀ (a b : α), b ≤ c a b
xs : ℕ → α := fun n => List.foldl (fun x n => c x (ys n)) (ys 0) (List.range n)
hsucc : ∀ (n : ℕ), xs (n + 1) = c (xs n) (ys n)
n : ℕ
⊢ ys n ≤ xs (n + 1)

Proof state:
case intro.refine_1
α : Type u_3
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝ : atTop.IsCountablyGenerated
ys : ℕ → α
h : Tendsto ys atTop atTop
c : α → α → α
hleft : ∀ (a b : α), a ≤ c a b
hright : ∀ (a b : α), b ≤ c a b
xs : ℕ → α := fun n => List.foldl (fun x n => c x (ys n)) (ys 0) (List.range n)
hsucc : ∀ (n : ℕ), xs (n + 1) = c (xs n) (ys n)
n : ℕ
⊢ xs n ≤ c (xs n) (ys n)

Tactic:
apply hleft

Result:
no goals

Proof state:
α : Type u_3
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝ : atTop.IsCountablyGenerated
ys : ℕ → α
h : Tendsto ys atTop atTop
c : α → α → α
hleft : ∀ (a b : α), a ≤ c a b
hright : ∀ (a b : α), b ≤ c a b
xs : ℕ → α := fun n => List.foldl (fun x n => c x (ys n)) (ys 0) (List.range n)
n : ℕ
⊢ xs (n + 1) = c (xs n) (ys n)

Tactic:
simp [xs, List.range_succ]

Result:
no goals

Proof state:
case intro.refine_2
α : Type u_3
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝ : atTop.IsCountablyGenerated
ys : ℕ → α
h : Tendsto ys atTop atTop
c : α → α → α
hleft : ∀ (a b : α), a ≤ c a b
hright : ∀ (a b : α), b ≤ c a b
xs : ℕ → α := fun n => List.foldl (fun x n => c x (ys n)) (ys 0) (List.range n)
hsucc : ∀ (n : ℕ), xs (n + 1) = c (xs n) (ys n)
n : ℕ
⊢ ys n ≤ c (xs n) (ys n)

Tactic:
apply hright

Result:
no goals

Proof state:
α : Type u_3
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝ : atTop.IsCountablyGenerated
⊢ ∃ xs, Monotone xs ∧ Tendsto xs atTop atTop

Tactic:
obtain ⟨ys, h⟩ := exists_seq_tendsto (atTop : Filter α)

Result:
case intro
α : Type u_3
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝ : atTop.IsCountablyGenerated
ys : ℕ → α
h : Tendsto ys atTop atTop
⊢ ∃ xs, Monotone xs ∧ Tendsto xs atTop atTop