Theorem: near_cluster (GlimpseOfLean/Solutions/Topics/SequenceLimits.lean)

State before:
u : ℕ → ℝ
a : ℝ
⊢ cluster_point u a → ∀ ε > 0, ∀ (N : ℕ), ∃ n ≥ N, |u n - a| ≤ ε
Tactic:
intro hyp ε ε_pos N
State after:
u : ℕ → ℝ
a : ℝ
hyp : cluster_point u a
ε : ℝ
ε_pos : ε > 0
N : ℕ
⊢ ∃ n ≥ N, |u n - a| ≤ ε

State before:
u : ℕ → ℝ
a : ℝ
hyp : cluster_point u a
ε : ℝ
ε_pos : ε > 0
N : ℕ
⊢ ∃ n ≥ N, |u n - a| ≤ ε
Tactic:
rcases hyp with ⟨φ, φ_extr, hφ⟩
State after:
case intro.intro
u : ℕ → ℝ
a ε : ℝ
ε_pos : ε > 0
N : ℕ
φ : ℕ → ℕ
φ_extr : extraction φ
hφ : seq_limit (u ∘ φ) a
⊢ ∃ n ≥ N, |u n - a| ≤ ε

State before:
case intro.intro
u : ℕ → ℝ
a ε : ℝ
ε_pos : ε > 0
N : ℕ
φ : ℕ → ℕ
φ_extr : extraction φ
hφ : seq_limit (u ∘ φ) a
⊢ ∃ n ≥ N, |u n - a| ≤ ε
Tactic:
cases' hφ ε ε_pos with N' hN'
State after:
case intro.intro.intro
u : ℕ → ℝ
a ε : ℝ
ε_pos : ε > 0
N : ℕ
φ : ℕ → ℕ
φ_extr : extraction φ
hφ : seq_limit (u ∘ φ) a
N' : ℕ
hN' : ∀ n ≥ N', |(u ∘ φ) n - a| ≤ ε
⊢ ∃ n ≥ N, |u n - a| ≤ ε

State before:
case intro.intro.intro
u : ℕ → ℝ
a ε : ℝ
ε_pos : ε > 0
N : ℕ
φ : ℕ → ℕ
φ_extr : extraction φ
hφ : seq_limit (u ∘ φ) a
N' : ℕ
hN' : ∀ n ≥ N', |(u ∘ φ) n - a| ≤ ε
⊢ ∃ n ≥ N, |u n - a| ≤ ε
Tactic:
rcases extraction_ge φ_extr N N' with ⟨q, hq, hq'⟩
State after:
case intro.intro.intro.intro.intro
u : ℕ → ℝ
a ε : ℝ
ε_pos : ε > 0
N : ℕ
φ : ℕ → ℕ
φ_extr : extraction φ
hφ : seq_limit (u ∘ φ) a
N' : ℕ
hN' : ∀ n ≥ N', |(u ∘ φ) n - a| ≤ ε
q : ℕ
hq : q ≥ N'
hq' : φ q ≥ N
⊢ ∃ n ≥ N, |u n - a| ≤ ε

State before:
case intro.intro.intro.intro.intro
u : ℕ → ℝ
a ε : ℝ
ε_pos : ε > 0
N : ℕ
φ : ℕ → ℕ
φ_extr : extraction φ
hφ : seq_limit (u ∘ φ) a
N' : ℕ
hN' : ∀ n ≥ N', |(u ∘ φ) n - a| ≤ ε
q : ℕ
hq : q ≥ N'
hq' : φ q ≥ N
⊢ ∃ n ≥ N, |u n - a| ≤ ε
Tactic:
exact ⟨φ q, hq', hN' _ hq⟩
State after:
no goals