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

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

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

State before:
a b : ℕ → ℝ
t u : ℝ
ha : tends_to a t
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Tactic:
rw [tends_to] at ha
State after:
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 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 : tends_to b u
ε : ℝ
hεpos : 0 < ε
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Tactic:
have haε : 0 < ε / 2 :=
  by
  linarith
State after:
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
haε : 0 < ε / 2
⊢ ∃ 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 : tends_to b u
ε : ℝ
hεpos : 0 < ε
haε : 0 < ε / 2
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Tactic:
apply ha at haε
State after:
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 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 : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
haε : ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε / 2
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Tactic:
obtain ⟨Na, ha'⟩ := haε
State after:
case intro
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε

State before:
case intro
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Tactic:
have hbε : 0 < ε / 2 :=
  by
  linarith
State after:
case intro
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
hbε : 0 < ε / 2
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε

State before:
case intro
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
hbε : 0 < ε / 2
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Tactic:
apply hb at hbε
State after:
case intro
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
hbε : ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε / 2
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε

State before:
case intro
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
hbε : ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε / 2
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Tactic:
obtain ⟨Nb, hb'⟩ := hbε
State after:
case intro.intro
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε

State before:
case intro.intro
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Tactic:
let Nab := max Na Nb
State after:
case intro.intro
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε

State before:
case intro.intro
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Tactic:
use Nab
State after:
case h
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
⊢ ∀ (n : ℕ), Nab ≤ n → |a n + b n - (t + u)| < ε

State before:
case h
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
⊢ ∀ (n : ℕ), Nab ≤ n → |a n + b n - (t + u)| < ε
Tactic:
intro n
State after:
case h
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
⊢ Nab ≤ n → |a n + b n - (t + u)| < ε

State before:
case h
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
⊢ Nab ≤ n → |a n + b n - (t + u)| < ε
Tactic:
intro hn
State after:
case h
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
⊢ |a n + b n - (t + u)| < ε

State before:
case h
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
⊢ |a n + b n - (t + u)| < ε
Tactic:
have ha'' := ha' n
State after:
case h
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
ha'' : Na ≤ n → |a n - t| < ε / 2
⊢ |a n + b n - (t + u)| < ε

State before:
case h
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
ha'' : Na ≤ n → |a n - t| < ε / 2
⊢ |a n + b n - (t + u)| < ε
Tactic:
have hb'' := hb' n
State after:
case h
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
ha'' : Na ≤ n → |a n - t| < ε / 2
hb'' : Nb ≤ n → |b n - u| < ε / 2
⊢ |a n + b n - (t + u)| < ε

State before:
case h
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
ha'' : Na ≤ n → |a n - t| < ε / 2
hb'' : Nb ≤ n → |b n - u| < ε / 2
⊢ |a n + b n - (t + u)| < ε
Tactic:
have hNan : Na ≤ n :=
  by
  exact le_of_max_le_left hn
State after:
case h
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
ha'' : Na ≤ n → |a n - t| < ε / 2
hb'' : Nb ≤ n → |b n - u| < ε / 2
hNan : Na ≤ n
⊢ |a n + b n - (t + u)| < ε

State before:
case h
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
ha'' : Na ≤ n → |a n - t| < ε / 2
hb'' : Nb ≤ n → |b n - u| < ε / 2
hNan : Na ≤ n
⊢ |a n + b n - (t + u)| < ε
Tactic:
have hNbn : Nb ≤ n :=
  by
  exact le_of_max_le_right hn
State after:
case h
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
ha'' : Na ≤ n → |a n - t| < ε / 2
hb'' : Nb ≤ n → |b n - u| < ε / 2
hNan : Na ≤ n
hNbn : Nb ≤ n
⊢ |a n + b n - (t + u)| < ε

State before:
case h
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
ha'' : Na ≤ n → |a n - t| < ε / 2
hb'' : Nb ≤ n → |b n - u| < ε / 2
hNan : Na ≤ n
hNbn : Nb ≤ n
⊢ |a n + b n - (t + u)| < ε
Tactic:
apply ha'' at hNan
State after:
case h
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
ha'' : Na ≤ n → |a n - t| < ε / 2
hb'' : Nb ≤ n → |b n - u| < ε / 2
hNbn : Nb ≤ n
hNan : |a n - t| < ε / 2
⊢ |a n + b n - (t + u)| < ε

State before:
case h
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
ha'' : Na ≤ n → |a n - t| < ε / 2
hb'' : Nb ≤ n → |b n - u| < ε / 2
hNbn : Nb ≤ n
hNan : |a n - t| < ε / 2
⊢ |a n + b n - (t + u)| < ε
Tactic:
apply hb'' at hNbn
State after:
case h
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
ha'' : Na ≤ n → |a n - t| < ε / 2
hb'' : Nb ≤ n → |b n - u| < ε / 2
hNan : |a n - t| < ε / 2
hNbn : |b n - u| < ε / 2
⊢ |a n + b n - (t + u)| < ε

State before:
case h
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
ha'' : Na ≤ n → |a n - t| < ε / 2
hb'' : Nb ≤ n → |b n - u| < ε / 2
hNan : |a n - t| < ε / 2
hNbn : |b n - u| < ε / 2
⊢ |a n + b n - (t + u)| < ε
Tactic:
calc
  |a n + b n - (t + u)|
    = |(a n - t) + (b n - u)| :=
    by
    apply congrArg
    ring
  _ ≤ |a n - t| + |b n - u|   :=
    by
    exact abs_add (a n - t) (b n - u)
  _ < ε / 2 + ε / 2           :=
    by
    exact add_lt_add hNan hNbn
  _ = ε                       :=
    by
    ring
State after:
no goals

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

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

State before:
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
ha'' : Na ≤ n → |a n - t| < ε / 2
hb'' : Nb ≤ n → |b n - u| < ε / 2
⊢ Na ≤ n
Tactic:
exact le_of_max_le_left hn
State after:
no goals

State before:
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
ha'' : Na ≤ n → |a n - t| < ε / 2
hb'' : Nb ≤ n → |b n - u| < ε / 2
hNan : Na ≤ n
⊢ Nb ≤ n
Tactic:
exact le_of_max_le_right hn
State after:
no goals

State before:
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
ha'' : Na ≤ n → |a n - t| < ε / 2
hb'' : Nb ≤ n → |b n - u| < ε / 2
hNan : |a n - t| < ε / 2
hNbn : |b n - u| < ε / 2
⊢ |a n + b n - (t + u)| = |a n - t + (b n - u)|
Tactic:
apply congrArg
State after:
case h
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
ha'' : Na ≤ n → |a n - t| < ε / 2
hb'' : Nb ≤ n → |b n - u| < ε / 2
hNan : |a n - t| < ε / 2
hNbn : |b n - u| < ε / 2
⊢ a n + b n - (t + u) = a n - t + (b n - u)

State before:
case h
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
ha'' : Na ≤ n → |a n - t| < ε / 2
hb'' : Nb ≤ n → |b n - u| < ε / 2
hNan : |a n - t| < ε / 2
hNbn : |b n - u| < ε / 2
⊢ a n + b n - (t + u) = a n - t + (b n - u)
Tactic:
ring
State after:
no goals

State before:
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
ha'' : Na ≤ n → |a n - t| < ε / 2
hb'' : Nb ≤ n → |b n - u| < ε / 2
hNan : |a n - t| < ε / 2
hNbn : |b n - u| < ε / 2
⊢ |a n - t + (b n - u)| ≤ |a n - t| + |b n - u|
Tactic:
exact abs_add (a n - t) (b n - u)
State after:
no goals

State before:
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
ha'' : Na ≤ n → |a n - t| < ε / 2
hb'' : Nb ≤ n → |b n - u| < ε / 2
hNan : |a n - t| < ε / 2
hNbn : |b n - u| < ε / 2
⊢ |a n - t| + |b n - u| < ε / 2 + ε / 2
Tactic:
exact add_lt_add hNan hNbn
State after:
no goals

State before:
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
ha'' : Na ≤ n → |a n - t| < ε / 2
hb'' : Nb ≤ n → |b n - u| < ε / 2
hNan : |a n - t| < ε / 2
hNbn : |b n - u| < ε / 2
⊢ ε / 2 + ε / 2 = ε
Tactic:
ring
State after:
no goals