Theorem: subseq_tendsto_of_tendsto (LeanTeaching/TutoLib.lean)

State before:
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
h : seq_limit u l
hφ : extraction φ
⊢ seq_limit (u ∘ φ) l
Tactic:
intros ε ε_pos
State after:
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
h : seq_limit u l
hφ : extraction φ
ε : ℝ
ε_pos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |(u ∘ φ) n - l| ≤ ε

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

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

State before:
case h
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
h : seq_limit u l
hφ : extraction φ
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
⊢ ∀ n ≥ N, |(u ∘ φ) n - l| ≤ ε
Tactic:
intros n hn
State after:
case h
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
h : seq_limit u l
hφ : extraction φ
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
n : ℕ
hn : n ≥ N
⊢ |(u ∘ φ) n - l| ≤ ε

State before:
case h
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
h : seq_limit u l
hφ : extraction φ
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
n : ℕ
hn : n ≥ N
⊢ |(u ∘ φ) n - l| ≤ ε
Tactic:
apply hN
State after:
case h.a
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
h : seq_limit u l
hφ : extraction φ
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
n : ℕ
hn : n ≥ N
⊢ φ n ≥ N

State before:
case h.a
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
h : seq_limit u l
hφ : extraction φ
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
n : ℕ
hn : n ≥ N
⊢ φ n ≥ N
Tactic:
calc N ≤ n := hn
_ ≤ φ n := id_le_extraction hφ n
State after:
no goals