Theorem: C03S06.auxαα (MIL/C03_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:
use max N₀ N₁
State after:
case h
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 ≥ max N₀ N₁, |s n * t n - 0| < ε

State before:
case h
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 ≥ max N₀ N₁, |s n * t n - 0| < ε
Tactic:
intro n ngt
State after:
case h
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 : ℕ
ngt : n ≥ max N₀ N₁
⊢ |s n * t n - 0| < ε

State before:
case h
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 : ℕ
ngt : n ≥ max N₀ N₁
⊢ |s n * t n - 0| < ε
Tactic:
have ngeN₀ : n ≥ N₀ := le_of_max_le_left ngt
State after:
case h
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 : ℕ
ngt : n ≥ max N₀ N₁
ngeN₀ : n ≥ N₀
⊢ |s n * t n - 0| < ε

State before:
case h
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 : ℕ
ngt : n ≥ max N₀ N₁
ngeN₀ : n ≥ N₀
⊢ |s n * t n - 0| < ε
Tactic:
have ngeN₁ : n ≥ N₁ := le_of_max_le_right ngt
State after:
case h
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 : ℕ
ngt : n ≥ max N₀ N₁
ngeN₀ : n ≥ N₀
ngeN₁ : n ≥ N₁
⊢ |s n * t n - 0| < ε

State before:
case h
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 : ℕ
ngt : n ≥ max N₀ N₁
ngeN₀ : n ≥ N₀
ngeN₁ : n ≥ N₁
⊢ |s n * t n - 0| < ε
Tactic:
calc
  |s n * t n - 0| = |s n| * |t n - 0| := by rw [sub_zero, abs_mul, sub_zero]
  _ < B * (ε / B) := (mul_lt_mul'' (h₀ n ngeN₀) (h₁ n ngeN₁) (abs_nonneg _) (abs_nonneg _))
  _ = ε := mul_div_cancel₀ _ (ne_of_lt Bpos).symm
State after:
no goals

State before:
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 : ℕ
ngt : n ≥ max N₀ N₁
ngeN₀ : n ≥ N₀
ngeN₁ : n ≥ N₁
⊢ |s n * t n - 0| = |s n| * |t n - 0|
Tactic:
rw [sub_zero, abs_mul, sub_zero]
State after:
no goals