Theorem: Section2sheet6Solutions.tendsTo_zero_mul_tendsTo_zero (FormalisingMathematics2024/Solutions/Section02reals/Sheet6.lean)

State before:
a b : ℕ → ℝ
ha : TendsTo a 0
hb : TendsTo b 0
⊢ TendsTo (fun n => a n * b n) 0
Tactic:
intro ε hε
State after:
a b : ℕ → ℝ
ha : TendsTo a 0
hb : TendsTo b 0
ε : ℝ
hε : ε > 0
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |(fun n => a n * b n) n - 0| < ε

State before:
a b : ℕ → ℝ
ha : TendsTo a 0
hb : TendsTo b 0
ε : ℝ
hε : ε > 0
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |(fun n => a n * b n) n - 0| < ε
Tactic:
obtain ⟨X, hX⟩ := ha ε hε
State after:
case intro
a b : ℕ → ℝ
ha : TendsTo a 0
hb : TendsTo b 0
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - 0| < ε
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |(fun n => a n * b n) n - 0| < ε

State before:
case intro
a b : ℕ → ℝ
ha : TendsTo a 0
hb : TendsTo b 0
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - 0| < ε
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |(fun n => a n * b n) n - 0| < ε
Tactic:
obtain ⟨Y, hY⟩ := hb 1 zero_lt_one
State after:
case intro.intro
a b : ℕ → ℝ
ha : TendsTo a 0
hb : TendsTo b 0
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - 0| < ε
Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |b n - 0| < 1
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |(fun n => a n * b n) n - 0| < ε

State before:
case intro.intro
a b : ℕ → ℝ
ha : TendsTo a 0
hb : TendsTo b 0
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - 0| < ε
Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |b n - 0| < 1
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |(fun n => a n * b n) n - 0| < ε
Tactic:
use max X Y
State after:
case h
a b : ℕ → ℝ
ha : TendsTo a 0
hb : TendsTo b 0
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - 0| < ε
Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |b n - 0| < 1
⊢ ∀ (n : ℕ), max X Y ≤ n → |(fun n => a n * b n) n - 0| < ε

State before:
case h
a b : ℕ → ℝ
ha : TendsTo a 0
hb : TendsTo b 0
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - 0| < ε
Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |b n - 0| < 1
⊢ ∀ (n : ℕ), max X Y ≤ n → |(fun n => a n * b n) n - 0| < ε
Tactic:
intro n hn
State after:
case h
a b : ℕ → ℝ
ha : TendsTo a 0
hb : TendsTo b 0
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - 0| < ε
Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |b n - 0| < 1
n : ℕ
hn : max X Y ≤ n
⊢ |(fun n => a n * b n) n - 0| < ε

State before:
case h
a b : ℕ → ℝ
ha : TendsTo a 0
hb : TendsTo b 0
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - 0| < ε
Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |b n - 0| < 1
n : ℕ
hn : max X Y ≤ n
⊢ |(fun n => a n * b n) n - 0| < ε
Tactic:
specialize hX n (le_of_max_le_left hn)
State after:
case h
a b : ℕ → ℝ
ha : TendsTo a 0
hb : TendsTo b 0
ε : ℝ
hε : ε > 0
X Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |b n - 0| < 1
n : ℕ
hn : max X Y ≤ n
hX : |a n - 0| < ε
⊢ |(fun n => a n * b n) n - 0| < ε

State before:
case h
a b : ℕ → ℝ
ha : TendsTo a 0
hb : TendsTo b 0
ε : ℝ
hε : ε > 0
X Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |b n - 0| < 1
n : ℕ
hn : max X Y ≤ n
hX : |a n - 0| < ε
⊢ |(fun n => a n * b n) n - 0| < ε
Tactic:
specialize hY n (le_of_max_le_right hn)
State after:
case h
a b : ℕ → ℝ
ha : TendsTo a 0
hb : TendsTo b 0
ε : ℝ
hε : ε > 0
X Y n : ℕ
hn : max X Y ≤ n
hX : |a n - 0| < ε
hY : |b n - 0| < 1
⊢ |(fun n => a n * b n) n - 0| < ε

State before:
case h
a b : ℕ → ℝ
ha : TendsTo a 0
hb : TendsTo b 0
ε : ℝ
hε : ε > 0
X Y n : ℕ
hn : max X Y ≤ n
hX : |a n - 0| < ε
hY : |b n - 0| < 1
⊢ |(fun n => a n * b n) n - 0| < ε
Tactic:
simpa [abs_mul] using mul_lt_mul'' hX hY
State after:
no goals