Theorem: C03S06.convergesTo_addαα (MIL/C03_Logic/S06_Sequences_and_Convergence.lean)

State before:
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
⊢ ConvergesTo (fun n => s n + t n) (a + b)
Tactic:
intro ε εpos
State after:
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |(fun n => s n + t n) n - (a + b)| < ε

State before:
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |(fun n => s n + t n) n - (a + b)| < ε
Tactic:
dsimp
State after:
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |s n + t n - (a + b)| < ε

State before:
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |s n + t n - (a + b)| < ε
Tactic:
have ε2pos : 0 < ε / 2 := by linarith
State after:
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
ε2pos : 0 < ε / 2
⊢ ∃ N, ∀ n ≥ N, |s n + t n - (a + b)| < ε

State before:
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
ε2pos : 0 < ε / 2
⊢ ∃ N, ∀ n ≥ N, |s n + t n - (a + b)| < ε
Tactic:
rcases cs (ε / 2) ε2pos with ⟨Ns, hs⟩
State after:
case intro
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
ε2pos : 0 < ε / 2
Ns : ℕ
hs : ∀ n ≥ Ns, |s n - a| < ε / 2
⊢ ∃ N, ∀ n ≥ N, |s n + t n - (a + b)| < ε

State before:
case intro
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
ε2pos : 0 < ε / 2
Ns : ℕ
hs : ∀ n ≥ Ns, |s n - a| < ε / 2
⊢ ∃ N, ∀ n ≥ N, |s n + t n - (a + b)| < ε
Tactic:
rcases ct (ε / 2) ε2pos with ⟨Nt, ht⟩
State after:
case intro.intro
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
ε2pos : 0 < ε / 2
Ns : ℕ
hs : ∀ n ≥ Ns, |s n - a| < ε / 2
Nt : ℕ
ht : ∀ n ≥ Nt, |t n - b| < ε / 2
⊢ ∃ N, ∀ n ≥ N, |s n + t n - (a + b)| < ε

State before:
case intro.intro
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
ε2pos : 0 < ε / 2
Ns : ℕ
hs : ∀ n ≥ Ns, |s n - a| < ε / 2
Nt : ℕ
ht : ∀ n ≥ Nt, |t n - b| < ε / 2
⊢ ∃ N, ∀ n ≥ N, |s n + t n - (a + b)| < ε
Tactic:
use max Ns Nt
State after:
case h
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
ε2pos : 0 < ε / 2
Ns : ℕ
hs : ∀ n ≥ Ns, |s n - a| < ε / 2
Nt : ℕ
ht : ∀ n ≥ Nt, |t n - b| < ε / 2
⊢ ∀ n ≥ max Ns Nt, |s n + t n - (a + b)| < ε

State before:
case h
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
ε2pos : 0 < ε / 2
Ns : ℕ
hs : ∀ n ≥ Ns, |s n - a| < ε / 2
Nt : ℕ
ht : ∀ n ≥ Nt, |t n - b| < ε / 2
⊢ ∀ n ≥ max Ns Nt, |s n + t n - (a + b)| < ε
Tactic:
intro n hn
State after:
case h
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
ε2pos : 0 < ε / 2
Ns : ℕ
hs : ∀ n ≥ Ns, |s n - a| < ε / 2
Nt : ℕ
ht : ∀ n ≥ Nt, |t n - b| < ε / 2
n : ℕ
hn : n ≥ max Ns Nt
⊢ |s n + t n - (a + b)| < ε

State before:
case h
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
ε2pos : 0 < ε / 2
Ns : ℕ
hs : ∀ n ≥ Ns, |s n - a| < ε / 2
Nt : ℕ
ht : ∀ n ≥ Nt, |t n - b| < ε / 2
n : ℕ
hn : n ≥ max Ns Nt
⊢ |s n + t n - (a + b)| < ε
Tactic:
have ngeNs : n ≥ Ns := le_of_max_le_left hn
State after:
case h
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
ε2pos : 0 < ε / 2
Ns : ℕ
hs : ∀ n ≥ Ns, |s n - a| < ε / 2
Nt : ℕ
ht : ∀ n ≥ Nt, |t n - b| < ε / 2
n : ℕ
hn : n ≥ max Ns Nt
ngeNs : n ≥ Ns
⊢ |s n + t n - (a + b)| < ε

State before:
case h
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
ε2pos : 0 < ε / 2
Ns : ℕ
hs : ∀ n ≥ Ns, |s n - a| < ε / 2
Nt : ℕ
ht : ∀ n ≥ Nt, |t n - b| < ε / 2
n : ℕ
hn : n ≥ max Ns Nt
ngeNs : n ≥ Ns
⊢ |s n + t n - (a + b)| < ε
Tactic:
have ngeNt : n ≥ Nt := le_of_max_le_right hn
State after:
case h
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
ε2pos : 0 < ε / 2
Ns : ℕ
hs : ∀ n ≥ Ns, |s n - a| < ε / 2
Nt : ℕ
ht : ∀ n ≥ Nt, |t n - b| < ε / 2
n : ℕ
hn : n ≥ max Ns Nt
ngeNs : n ≥ Ns
ngeNt : n ≥ Nt
⊢ |s n + t n - (a + b)| < ε

State before:
case h
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
ε2pos : 0 < ε / 2
Ns : ℕ
hs : ∀ n ≥ Ns, |s n - a| < ε / 2
Nt : ℕ
ht : ∀ n ≥ Nt, |t n - b| < ε / 2
n : ℕ
hn : n ≥ max Ns Nt
ngeNs : n ≥ Ns
ngeNt : n ≥ Nt
⊢ |s n + t n - (a + b)| < ε
Tactic:
calc
  |s n + t n - (a + b)| = |s n - a + (t n - b)| := by
    congr
    ring
  _ ≤ |s n - a| + |t n - b| := (abs_add _ _)
  _ < ε / 2 + ε / 2 := (add_lt_add (hs n ngeNs) (ht n ngeNt))
  _ = ε := by norm_num
State after:
no goals

State before:
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
⊢ 0 < ε / 2
Tactic:
linarith
State after:
no goals

State before:
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
ε2pos : 0 < ε / 2
Ns : ℕ
hs : ∀ n ≥ Ns, |s n - a| < ε / 2
Nt : ℕ
ht : ∀ n ≥ Nt, |t n - b| < ε / 2
n : ℕ
hn : n ≥ max Ns Nt
ngeNs : n ≥ Ns
ngeNt : n ≥ Nt
⊢ |s n + t n - (a + b)| = |s n - a + (t n - b)|
Tactic:
congr
State after:
case e_a
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
ε2pos : 0 < ε / 2
Ns : ℕ
hs : ∀ n ≥ Ns, |s n - a| < ε / 2
Nt : ℕ
ht : ∀ n ≥ Nt, |t n - b| < ε / 2
n : ℕ
hn : n ≥ max Ns Nt
ngeNs : n ≥ Ns
ngeNt : n ≥ Nt
⊢ s n + t n - (a + b) = s n - a + (t n - b)

State before:
case e_a
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
ε2pos : 0 < ε / 2
Ns : ℕ
hs : ∀ n ≥ Ns, |s n - a| < ε / 2
Nt : ℕ
ht : ∀ n ≥ Nt, |t n - b| < ε / 2
n : ℕ
hn : n ≥ max Ns Nt
ngeNs : n ≥ Ns
ngeNt : n ≥ Nt
⊢ s n + t n - (a + b) = s n - a + (t n - b)
Tactic:
ring
State after:
no goals

State before:
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
ε2pos : 0 < ε / 2
Ns : ℕ
hs : ∀ n ≥ Ns, |s n - a| < ε / 2
Nt : ℕ
ht : ∀ n ≥ Nt, |t n - b| < ε / 2
n : ℕ
hn : n ≥ max Ns Nt
ngeNs : n ≥ Ns
ngeNt : n ≥ Nt
⊢ ε / 2 + ε / 2 = ε
Tactic:
norm_num
State after:
no goals