Theorem: tends_to_add_const (FM2023Exrcise/section02_reals/sheet3.lean)

State before:
a : ℕ → ℝ
t c : ℝ
h : tends_to a t
⊢ tends_to (fun n => a n + c) (t + c)
Tactic:
rw [tends_to_def] at *
State after:
a : ℕ → ℝ
t c : ℝ
h : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
⊢ ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n + c - (t + c)| < ε

State before:
a : ℕ → ℝ
t c : ℝ
h : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
⊢ ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n + c - (t + c)| < ε
Tactic:
intro ε hε
State after:
a : ℕ → ℝ
t c : ℝ
h : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hε : 0 < ε
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + c - (t + c)| < ε

State before:
a : ℕ → ℝ
t c : ℝ
h : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hε : 0 < ε
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + c - (t + c)| < ε
Tactic:
have hε' := h ε $ hε
State after:
a : ℕ → ℝ
t c : ℝ
h : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hε : 0 < ε
hε' : ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + c - (t + c)| < ε

State before:
a : ℕ → ℝ
t c : ℝ
h : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hε : 0 < ε
hε' : ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + c - (t + c)| < ε
Tactic:
obtain ⟨B', hε''⟩ := hε'
State after:
case intro
a : ℕ → ℝ
t c : ℝ
h : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hε : 0 < ε
B' : ℕ
hε'' : ∀ (n : ℕ), B' ≤ n → |a n - t| < ε
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + c - (t + c)| < ε

State before:
case intro
a : ℕ → ℝ
t c : ℝ
h : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hε : 0 < ε
B' : ℕ
hε'' : ∀ (n : ℕ), B' ≤ n → |a n - t| < ε
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + c - (t + c)| < ε
Tactic:
use B'
State after:
case h
a : ℕ → ℝ
t c : ℝ
h : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hε : 0 < ε
B' : ℕ
hε'' : ∀ (n : ℕ), B' ≤ n → |a n - t| < ε
⊢ ∀ (n : ℕ), B' ≤ n → |a n + c - (t + c)| < ε

State before:
case h
a : ℕ → ℝ
t c : ℝ
h : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hε : 0 < ε
B' : ℕ
hε'' : ∀ (n : ℕ), B' ≤ n → |a n - t| < ε
⊢ ∀ (n : ℕ), B' ≤ n → |a n + c - (t + c)| < ε
Tactic:
intro n hn
State after:
case h
a : ℕ → ℝ
t c : ℝ
h : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hε : 0 < ε
B' : ℕ
hε'' : ∀ (n : ℕ), B' ≤ n → |a n - t| < ε
n : ℕ
hn : B' ≤ n
⊢ |a n + c - (t + c)| < ε

State before:
case h
a : ℕ → ℝ
t c : ℝ
h : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hε : 0 < ε
B' : ℕ
hε'' : ∀ (n : ℕ), B' ≤ n → |a n - t| < ε
n : ℕ
hn : B' ≤ n
⊢ |a n + c - (t + c)| < ε
Tactic:
have h' := hε'' n hn
State after:
case h
a : ℕ → ℝ
t c : ℝ
h : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hε : 0 < ε
B' : ℕ
hε'' : ∀ (n : ℕ), B' ≤ n → |a n - t| < ε
n : ℕ
hn : B' ≤ n
h' : |a n - t| < ε
⊢ |a n + c - (t + c)| < ε

State before:
case h
a : ℕ → ℝ
t c : ℝ
h : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hε : 0 < ε
B' : ℕ
hε'' : ∀ (n : ℕ), B' ≤ n → |a n - t| < ε
n : ℕ
hn : B' ≤ n
h' : |a n - t| < ε
⊢ |a n + c - (t + c)| < ε
Tactic:
norm_num
State after:
case h
a : ℕ → ℝ
t c : ℝ
h : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hε : 0 < ε
B' : ℕ
hε'' : ∀ (n : ℕ), B' ≤ n → |a n - t| < ε
n : ℕ
hn : B' ≤ n
h' : |a n - t| < ε
⊢ |a n - t| < ε

State before:
case h
a : ℕ → ℝ
t c : ℝ
h : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hε : 0 < ε
B' : ℕ
hε'' : ∀ (n : ℕ), B' ≤ n → |a n - t| < ε
n : ℕ
hn : B' ≤ n
h' : |a n - t| < ε
⊢ |a n - t| < ε
Tactic:
apply h'
State after:
no goals