rcases ct _ pos₀ with ⟨N₁, h₁⟩
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| < ε
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| < ε