Theorem: Section2sheet5.tendsTo_add (FormalisingMathematics2024/Section02reals/Sheet5.lean)

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

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

State before:
a b : ℕ → ℝ
t u : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Tactic:
specialize ha (ε / 2) (by linarith)
State after:
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
ha : ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε / 2
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε

State before:
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
ha : ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε / 2
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Tactic:
cases' ha with X hX
State after:
case intro
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / 2
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε

State before:
case intro
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / 2
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Tactic:
obtain ⟨Y, hY⟩ := hb (ε / 2) (by linarith)
State after:
case intro.intro
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / 2
Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |b n - u| < ε / 2
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε

State before:
case intro.intro
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / 2
Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |b n - u| < ε / 2
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Tactic:
use max X Y
State after:
case h
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / 2
Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |b n - u| < ε / 2
⊢ ∀ (n : ℕ), max X Y ≤ n → |a n + b n - (t + u)| < ε

State before:
case h
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / 2
Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |b n - u| < ε / 2
⊢ ∀ (n : ℕ), max X Y ≤ n → |a n + b n - (t + u)| < ε
Tactic:
intro n hn
State after:
case h
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / 2
Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |b n - u| < ε / 2
n : ℕ
hn : max X Y ≤ n
⊢ |a n + b n - (t + u)| < ε

State before:
case h
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / 2
Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |b n - u| < ε / 2
n : ℕ
hn : max X Y ≤ n
⊢ |a n + b n - (t + u)| < ε
Tactic:
rw [max_le_iff] at hn
State after:
case h
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / 2
Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |b n - u| < ε / 2
n : ℕ
hn : X ≤ n ∧ Y ≤ n
⊢ |a n + b n - (t + u)| < ε

State before:
case h
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / 2
Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |b n - u| < ε / 2
n : ℕ
hn : X ≤ n ∧ Y ≤ n
⊢ |a n + b n - (t + u)| < ε
Tactic:
specialize hX n hn.1
State after:
case h
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
X Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |b n - u| < ε / 2
n : ℕ
hn : X ≤ n ∧ Y ≤ n
hX : |a n - t| < ε / 2
⊢ |a n + b n - (t + u)| < ε

State before:
case h
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
X Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |b n - u| < ε / 2
n : ℕ
hn : X ≤ n ∧ Y ≤ n
hX : |a n - t| < ε / 2
⊢ |a n + b n - (t + u)| < ε
Tactic:
specialize hY n hn.2
State after:
case h
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
X Y n : ℕ
hn : X ≤ n ∧ Y ≤ n
hX : |a n - t| < ε / 2
hY : |b n - u| < ε / 2
⊢ |a n + b n - (t + u)| < ε

State before:
case h
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
X Y n : ℕ
hn : X ≤ n ∧ Y ≤ n
hX : |a n - t| < ε / 2
hY : |b n - u| < ε / 2
⊢ |a n + b n - (t + u)| < ε
Tactic:
rw [abs_lt] at *
State after:
case h
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
X Y n : ℕ
hn : X ≤ n ∧ Y ≤ n
hX : -(ε / 2) < a n - t ∧ a n - t < ε / 2
hY : -(ε / 2) < b n - u ∧ b n - u < ε / 2
⊢ -ε < a n + b n - (t + u) ∧ a n + b n - (t + u) < ε

State before:
case h
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
X Y n : ℕ
hn : X ≤ n ∧ Y ≤ n
hX : -(ε / 2) < a n - t ∧ a n - t < ε / 2
hY : -(ε / 2) < b n - u ∧ b n - u < ε / 2
⊢ -ε < a n + b n - (t + u) ∧ a n + b n - (t + u) < ε
Tactic:
constructor <;>linarith
State after:
no goals

State before:
a b : ℕ → ℝ
t u : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
⊢ 0 < ε / 2
Tactic:
linarith
State after:
no goals

State before:
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / 2
⊢ 0 < ε / 2
Tactic:
linarith
State after:
no goals