Theorem: limit_of_sub_le_inv_succ (LeanTeaching/TutoLib.lean)

State before:
u : ℕ → ℝ
x : ℝ
h : ∀ (n : ℕ), |u n - x| ≤ 1 / (↑n + 1)
⊢ seq_limit u x
Tactic:
intros ε ε_pos
State after:
u : ℕ → ℝ
x : ℝ
h : ∀ (n : ℕ), |u n - x| ≤ 1 / (↑n + 1)
ε : ℝ
ε_pos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |u n - x| ≤ ε

State before:
u : ℕ → ℝ
x : ℝ
h : ∀ (n : ℕ), |u n - x| ≤ 1 / (↑n + 1)
ε : ℝ
ε_pos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |u n - x| ≤ ε
Tactic:
rcases inv_succ_le_all ε ε_pos with ⟨N, hN⟩
State after:
case intro
u : ℕ → ℝ
x : ℝ
h : ∀ (n : ℕ), |u n - x| ≤ 1 / (↑n + 1)
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, 1 / (↑n + 1) ≤ ε
⊢ ∃ N, ∀ n ≥ N, |u n - x| ≤ ε

State before:
case intro
u : ℕ → ℝ
x : ℝ
h : ∀ (n : ℕ), |u n - x| ≤ 1 / (↑n + 1)
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, 1 / (↑n + 1) ≤ ε
⊢ ∃ N, ∀ n ≥ N, |u n - x| ≤ ε
Tactic:
use N
State after:
case h
u : ℕ → ℝ
x : ℝ
h : ∀ (n : ℕ), |u n - x| ≤ 1 / (↑n + 1)
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, 1 / (↑n + 1) ≤ ε
⊢ ∀ n ≥ N, |u n - x| ≤ ε

State before:
case h
u : ℕ → ℝ
x : ℝ
h : ∀ (n : ℕ), |u n - x| ≤ 1 / (↑n + 1)
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, 1 / (↑n + 1) ≤ ε
⊢ ∀ n ≥ N, |u n - x| ≤ ε
Tactic:
intros n hn
State after:
case h
u : ℕ → ℝ
x : ℝ
h : ∀ (n : ℕ), |u n - x| ≤ 1 / (↑n + 1)
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, 1 / (↑n + 1) ≤ ε
n : ℕ
hn : n ≥ N
⊢ |u n - x| ≤ ε

State before:
case h
u : ℕ → ℝ
x : ℝ
h : ∀ (n : ℕ), |u n - x| ≤ 1 / (↑n + 1)
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, 1 / (↑n + 1) ≤ ε
n : ℕ
hn : n ≥ N
⊢ |u n - x| ≤ ε
Tactic:
specialize h n
State after:
case h
u : ℕ → ℝ
x ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, 1 / (↑n + 1) ≤ ε
n : ℕ
hn : n ≥ N
h : |u n - x| ≤ 1 / (↑n + 1)
⊢ |u n - x| ≤ ε

State before:
case h
u : ℕ → ℝ
x ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, 1 / (↑n + 1) ≤ ε
n : ℕ
hn : n ≥ N
h : |u n - x| ≤ 1 / (↑n + 1)
⊢ |u n - x| ≤ ε
Tactic:
specialize hN n hn
State after:
case h
u : ℕ → ℝ
x ε : ℝ
ε_pos : ε > 0
N n : ℕ
hn : n ≥ N
h : |u n - x| ≤ 1 / (↑n + 1)
hN : 1 / (↑n + 1) ≤ ε
⊢ |u n - x| ≤ ε

State before:
case h
u : ℕ → ℝ
x ε : ℝ
ε_pos : ε > 0
N n : ℕ
hn : n ≥ N
h : |u n - x| ≤ 1 / (↑n + 1)
hN : 1 / (↑n + 1) ≤ ε
⊢ |u n - x| ≤ ε
Tactic:
linarith
State after:
no goals