Theorem: C03S06.aux (LeanInRome/S3_Logic/S06_Sequences_and_Convergence.lean)

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

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

State before:
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |s n * t n - 0| < ε
Tactic:
rcases exists_abs_le_of_convergesTo cs with ⟨N₀, B, h₀⟩
State after:
case intro.intro
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
N₀ : ℕ
B : ℝ
h₀ : ∀ (n : ℕ), N₀ ≤ n → |s n| < B
⊢ ∃ N, ∀ n ≥ N, |s n * t n - 0| < ε

State before:
case intro.intro
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
N₀ : ℕ
B : ℝ
h₀ : ∀ (n : ℕ), N₀ ≤ n → |s n| < B
⊢ ∃ N, ∀ n ≥ N, |s n * t n - 0| < ε
Tactic:
have Bpos : 0 < B := lt_of_le_of_lt (abs_nonneg _) (h₀ N₀ (le_refl _))
State after:
case intro.intro
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
N₀ : ℕ
B : ℝ
h₀ : ∀ (n : ℕ), N₀ ≤ n → |s n| < B
Bpos : 0 < B
⊢ ∃ N, ∀ n ≥ N, |s n * t n - 0| < ε

State before:
case intro.intro
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
N₀ : ℕ
B : ℝ
h₀ : ∀ (n : ℕ), N₀ ≤ n → |s n| < B
Bpos : 0 < B
⊢ ∃ N, ∀ n ≥ N, |s n * t n - 0| < ε
Tactic:
have pos₀ : ε / B > 0 := div_pos εpos Bpos
State after:
case intro.intro
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
N₀ : ℕ
B : ℝ
h₀ : ∀ (n : ℕ), N₀ ≤ n → |s n| < B
Bpos : 0 < B
pos₀ : ε / B > 0
⊢ ∃ N, ∀ n ≥ N, |s n * t n - 0| < ε

State before:
case intro.intro
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
N₀ : ℕ
B : ℝ
h₀ : ∀ (n : ℕ), N₀ ≤ n → |s n| < B
Bpos : 0 < B
pos₀ : ε / B > 0
⊢ ∃ N, ∀ n ≥ N, |s n * t n - 0| < ε
Tactic:
rcases ct _ pos₀ with ⟨N₁, h₁⟩
State after:
case intro.intro.intro
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
N₀ : ℕ
B : ℝ
h₀ : ∀ (n : ℕ), N₀ ≤ n → |s n| < B
Bpos : 0 < B
pos₀ : ε / B > 0
N₁ : ℕ
h₁ : ∀ n ≥ N₁, |t n - 0| < ε / B
⊢ ∃ N, ∀ n ≥ N, |s n * t n - 0| < ε

State before:
case intro.intro.intro
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
N₀ : ℕ
B : ℝ
h₀ : ∀ (n : ℕ), N₀ ≤ n → |s n| < B
Bpos : 0 < B
pos₀ : ε / B > 0
N₁ : ℕ
h₁ : ∀ n ≥ N₁, |t n - 0| < ε / B
⊢ ∃ N, ∀ n ≥ N, |s n * t n - 0| < ε
Tactic:
sorry
State after:
no goals