Theorem: C03S06.convergesTo_add (LeanCourse/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:
sorry
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