Theorem: C03S06.convergesTo_mul (LeanCourse/MIL/C03_Logic/S06_Sequences_and_Convergence.lean)

State before:
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
⊢ ConvergesTo (fun n => s n * t n) (a * b)
Tactic:
have h₁ : ConvergesTo (fun n ↦ s n * (t n + -b)) 0 := by
  apply aux cs
  convert convergesTo_add ct (convergesTo_const (-b))
  ring
State after:
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
h₁ : ConvergesTo (fun n => s n * (t n + -b)) 0
⊢ ConvergesTo (fun n => s n * t n) (a * b)

State before:
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
h₁ : ConvergesTo (fun n => s n * (t n + -b)) 0
⊢ ConvergesTo (fun n => s n * t n) (a * b)
Tactic:
have := convergesTo_add h₁ (convergesTo_mul_const b cs)
State after:
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
h₁ : ConvergesTo (fun n => s n * (t n + -b)) 0
this : ConvergesTo (fun n => s n * (t n + -b) + b * s n) (0 + b * a)
⊢ ConvergesTo (fun n => s n * t n) (a * b)

State before:
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
h₁ : ConvergesTo (fun n => s n * (t n + -b)) 0
this : ConvergesTo (fun n => s n * (t n + -b) + b * s n) (0 + b * a)
⊢ ConvergesTo (fun n => s n * t n) (a * b)
Tactic:
convert convergesTo_add h₁ (convergesTo_mul_const b cs) using 1
State after:
case h.e'_1
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
h₁ : ConvergesTo (fun n => s n * (t n + -b)) 0
this : ConvergesTo (fun n => s n * (t n + -b) + b * s n) (0 + b * a)
⊢ (fun n => s n * t n) = fun n => s n * (t n + -b) + b * s n

case h.e'_2
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
h₁ : ConvergesTo (fun n => s n * (t n + -b)) 0
this : ConvergesTo (fun n => s n * (t n + -b) + b * s n) (0 + b * a)
⊢ a * b = 0 + b * a

State before:
case h.e'_2
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
h₁ : ConvergesTo (fun n => s n * (t n + -b)) 0
this : ConvergesTo (fun n => s n * (t n + -b) + b * s n) (0 + b * a)
⊢ a * b = 0 + b * a
Tactic:
ring
State after:
no goals

State before:
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
⊢ ConvergesTo (fun n => s n * (t n + -b)) 0
Tactic:
apply aux cs
State after:
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
⊢ ConvergesTo (fun n => t n + -b) 0

State before:
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
⊢ ConvergesTo (fun n => t n + -b) 0
Tactic:
convert convergesTo_add ct (convergesTo_const (-b))
State after:
case h.e'_2
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
⊢ 0 = b + -b

State before:
case h.e'_2
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
⊢ 0 = b + -b
Tactic:
ring
State after:
no goals

State before:
case h.e'_1
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
h₁ : ConvergesTo (fun n => s n * (t n + -b)) 0
this : ConvergesTo (fun n => s n * (t n + -b) + b * s n) (0 + b * a)
⊢ (fun n => s n * t n) = fun n => s n * (t n + -b) + b * s n
Tactic:
ext
State after:
case h.e'_1.h
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
h₁ : ConvergesTo (fun n => s n * (t n + -b)) 0
this : ConvergesTo (fun n => s n * (t n + -b) + b * s n) (0 + b * a)
x✝ : ℕ
⊢ s x✝ * t x✝ = s x✝ * (t x✝ + -b) + b * s x✝

State before:
case h.e'_1.h
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
h₁ : ConvergesTo (fun n => s n * (t n + -b)) 0
this : ConvergesTo (fun n => s n * (t n + -b) + b * s n) (0 + b * a)
x✝ : ℕ
⊢ s x✝ * t x✝ = s x✝ * (t x✝ + -b) + b * s x✝
Tactic:
ring
State after:
no goals