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

State before:
a b : ℕ → ℝ
t u : ℝ
ha : TendsTo a t
hb : TendsTo b u
⊢ TendsTo (fun n => a n * b n) (t * u)
Tactic:
rw [tendsTo_sub_lim_iff] at *
State after:
a b : ℕ → ℝ
t u : ℝ
ha : TendsTo (fun n => a n - t) 0
hb : TendsTo (fun n => b n - u) 0
⊢ TendsTo (fun n => a n * b n - t * u) 0

State before:
a b : ℕ → ℝ
t u : ℝ
ha : TendsTo (fun n => a n - t) 0
hb : TendsTo (fun n => b n - u) 0
⊢ TendsTo (fun n => a n * b n - t * u) 0
Tactic:
have h : ∀ n, a n * b n - t * u = (a n - t) * (b n - u) + t * (b n - u) + (a n - t) * u := by
  intro n; ring
State after:
a b : ℕ → ℝ
t u : ℝ
ha : TendsTo (fun n => a n - t) 0
hb : TendsTo (fun n => b n - u) 0
h : ∀ (n : ℕ), a n * b n - t * u = (a n - t) * (b n - u) + t * (b n - u) + (a n - t) * u
⊢ TendsTo (fun n => a n * b n - t * u) 0

State before:
a b : ℕ → ℝ
t u : ℝ
ha : TendsTo (fun n => a n - t) 0
hb : TendsTo (fun n => b n - u) 0
h : ∀ (n : ℕ), a n * b n - t * u = (a n - t) * (b n - u) + t * (b n - u) + (a n - t) * u
⊢ TendsTo (fun n => a n * b n - t * u) 0
Tactic:
simp [h]
State after:
a b : ℕ → ℝ
t u : ℝ
ha : TendsTo (fun n => a n - t) 0
hb : TendsTo (fun n => b n - u) 0
h : ∀ (n : ℕ), a n * b n - t * u = (a n - t) * (b n - u) + t * (b n - u) + (a n - t) * u
⊢ TendsTo (fun n => (a n - t) * (b n - u) + t * (b n - u) + (a n - t) * u) 0

State before:
a b : ℕ → ℝ
t u : ℝ
ha : TendsTo (fun n => a n - t) 0
hb : TendsTo (fun n => b n - u) 0
h : ∀ (n : ℕ), a n * b n - t * u = (a n - t) * (b n - u) + t * (b n - u) + (a n - t) * u
⊢ TendsTo (fun n => (a n - t) * (b n - u) + t * (b n - u) + (a n - t) * u) 0
Tactic:
rw [show (0 : ℝ) = 0 + t * 0 + 0 * u by simp]
State after:
a b : ℕ → ℝ
t u : ℝ
ha : TendsTo (fun n => a n - t) 0
hb : TendsTo (fun n => b n - u) 0
h : ∀ (n : ℕ), a n * b n - t * u = (a n - t) * (b n - u) + t * (b n - u) + (a n - t) * u
⊢ TendsTo (fun n => (a n - t) * (b n - u) + t * (b n - u) + (a n - t) * u) (0 + t * 0 + 0 * u)

State before:
a b : ℕ → ℝ
t u : ℝ
ha : TendsTo (fun n => a n - t) 0
hb : TendsTo (fun n => b n - u) 0
h : ∀ (n : ℕ), a n * b n - t * u = (a n - t) * (b n - u) + t * (b n - u) + (a n - t) * u
⊢ TendsTo (fun n => (a n - t) * (b n - u) + t * (b n - u) + (a n - t) * u) (0 + t * 0 + 0 * u)
Tactic:
refine' tendsTo_add (tendsTo_add _ _) _
State after:
case refine'_1
a b : ℕ → ℝ
t u : ℝ
ha : TendsTo (fun n => a n - t) 0
hb : TendsTo (fun n => b n - u) 0
h : ∀ (n : ℕ), a n * b n - t * u = (a n - t) * (b n - u) + t * (b n - u) + (a n - t) * u
⊢ TendsTo (fun n => (a n - t) * (b n - u)) 0

case refine'_2
a b : ℕ → ℝ
t u : ℝ
ha : TendsTo (fun n => a n - t) 0
hb : TendsTo (fun n => b n - u) 0
h : ∀ (n : ℕ), a n * b n - t * u = (a n - t) * (b n - u) + t * (b n - u) + (a n - t) * u
⊢ TendsTo (fun n => t * (b n - u)) (t * 0)

case refine'_3
a b : ℕ → ℝ
t u : ℝ
ha : TendsTo (fun n => a n - t) 0
hb : TendsTo (fun n => b n - u) 0
h : ∀ (n : ℕ), a n * b n - t * u = (a n - t) * (b n - u) + t * (b n - u) + (a n - t) * u
⊢ TendsTo (fun n => (a n - t) * u) (0 * u)

State before:
a b : ℕ → ℝ
t u : ℝ
ha : TendsTo (fun n => a n - t) 0
hb : TendsTo (fun n => b n - u) 0
⊢ ∀ (n : ℕ), a n * b n - t * u = (a n - t) * (b n - u) + t * (b n - u) + (a n - t) * u
Tactic:
intro n
State after:
a b : ℕ → ℝ
t u : ℝ
ha : TendsTo (fun n => a n - t) 0
hb : TendsTo (fun n => b n - u) 0
n : ℕ
⊢ a n * b n - t * u = (a n - t) * (b n - u) + t * (b n - u) + (a n - t) * u

State before:
a b : ℕ → ℝ
t u : ℝ
ha : TendsTo (fun n => a n - t) 0
hb : TendsTo (fun n => b n - u) 0
n : ℕ
⊢ a n * b n - t * u = (a n - t) * (b n - u) + t * (b n - u) + (a n - t) * u
Tactic:
ring
State after:
no goals

State before:
a b : ℕ → ℝ
t u : ℝ
ha : TendsTo (fun n => a n - t) 0
hb : TendsTo (fun n => b n - u) 0
h : ∀ (n : ℕ), a n * b n - t * u = (a n - t) * (b n - u) + t * (b n - u) + (a n - t) * u
⊢ 0 = 0 + t * 0 + 0 * u
Tactic:
simp
State after:
no goals

State before:
case refine'_1
a b : ℕ → ℝ
t u : ℝ
ha : TendsTo (fun n => a n - t) 0
hb : TendsTo (fun n => b n - u) 0
h : ∀ (n : ℕ), a n * b n - t * u = (a n - t) * (b n - u) + t * (b n - u) + (a n - t) * u
⊢ TendsTo (fun n => (a n - t) * (b n - u)) 0
Tactic:
exact tendsTo_zero_mul_tendsTo_zero ha hb
State after:
no goals

State before:
case refine'_2
a b : ℕ → ℝ
t u : ℝ
ha : TendsTo (fun n => a n - t) 0
hb : TendsTo (fun n => b n - u) 0
h : ∀ (n : ℕ), a n * b n - t * u = (a n - t) * (b n - u) + t * (b n - u) + (a n - t) * u
⊢ TendsTo (fun n => t * (b n - u)) (t * 0)
Tactic:
exact tendsTo_const_mul t hb
State after:
no goals

State before:
case refine'_3
a b : ℕ → ℝ
t u : ℝ
ha : TendsTo (fun n => a n - t) 0
hb : TendsTo (fun n => b n - u) 0
h : ∀ (n : ℕ), a n * b n - t * u = (a n - t) * (b n - u) + t * (b n - u) + (a n - t) * u
⊢ TendsTo (fun n => (a n - t) * u) (0 * u)
Tactic:
exact tendsTo_mul_const u ha
State after:
no goals