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

State before:
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
⊢ ConvergesTo (fun n => c * s n) (c * a)
Tactic:
by_cases h : c = 0
State after:
case pos
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : c = 0
⊢ ConvergesTo (fun n => c * s n) (c * a)

case neg
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : ¬c = 0
⊢ ConvergesTo (fun n => c * s n) (c * a)

State before:
case neg
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : ¬c = 0
⊢ ConvergesTo (fun n => c * s n) (c * a)
Tactic:
have acpos : 0 < |c| := abs_pos.mpr h
State after:
case neg
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : ¬c = 0
acpos : 0 < |c|
⊢ ConvergesTo (fun n => c * s n) (c * a)

State before:
case neg
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : ¬c = 0
acpos : 0 < |c|
⊢ ConvergesTo (fun n => c * s n) (c * a)
Tactic:
sorry
State after:
no goals

State before:
case pos
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : c = 0
⊢ ConvergesTo (fun n => c * s n) (c * a)
Tactic:
convert convergesTo_const 0
State after:
case h.e'_1.h
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : c = 0
x✝ : ℕ
⊢ c * s x✝ = 0

case h.e'_2
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : c = 0
⊢ c * a = 0

State before:
case h.e'_2
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : c = 0
⊢ c * a = 0
Tactic:
rw [h]
State after:
case h.e'_2
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : c = 0
⊢ 0 * a = 0

State before:
case h.e'_2
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : c = 0
⊢ 0 * a = 0
Tactic:
ring
State after:
no goals

State before:
case h.e'_1.h
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : c = 0
x✝ : ℕ
⊢ c * s x✝ = 0
Tactic:
rw [h]
State after:
case h.e'_1.h
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : c = 0
x✝ : ℕ
⊢ 0 * s x✝ = 0

State before:
case h.e'_1.h
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : c = 0
x✝ : ℕ
⊢ 0 * s x✝ = 0
Tactic:
ring
State after:
no goals