Theorem: tends_to_neg (FM2023Exrcise/section02_reals/sheet5.lean)

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

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

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

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

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

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

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

State before:
case h
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hεpos : 0 < ε
N : ℕ
h : ∀ (n : ℕ), N ≤ n → |a n - t| < ε
n : ℕ
hn : N ≤ n
h' : |a n - t| < ε
⊢ |-a n + t| < ε
Tactic:
rw [← abs_neg] at h'
State after:
case h
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hεpos : 0 < ε
N : ℕ
h : ∀ (n : ℕ), N ≤ n → |a n - t| < ε
n : ℕ
hn : N ≤ n
h' : |(-(a n - t))| < ε
⊢ |-a n + t| < ε

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

State before:
case h
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hεpos : 0 < ε
N : ℕ
h : ∀ (n : ℕ), N ≤ n → |a n - t| < ε
n : ℕ
hn : N ≤ n
h' : |t - a n| < ε
⊢ |-a n + t| < ε
Tactic:
rw [add_comm]
State after:
case h
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
ε : ℝ
hεpos : 0 < ε
N : ℕ
h : ∀ (n : ℕ), N ≤ n → |a n - t| < ε
n : ℕ
hn : N ≤ n
h' : |t - a n| < ε
⊢ |t + -a n| < ε

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