Theorem: C03S06.convergesTo_mul_constαα (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:
intro ε εpos
State after:
case neg
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : ¬c = 0
acpos : 0 < |c|
ε : ℝ
εpos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |(fun n => c * s n) n - c * a| < ε

State before:
case neg
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : ¬c = 0
acpos : 0 < |c|
ε : ℝ
εpos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |(fun n => c * s n) n - c * a| < ε
Tactic:
dsimp
State after:
case neg
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : ¬c = 0
acpos : 0 < |c|
ε : ℝ
εpos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |c * s n - c * a| < ε

State before:
case neg
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : ¬c = 0
acpos : 0 < |c|
ε : ℝ
εpos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |c * s n - c * a| < ε
Tactic:
have εcpos : 0 < ε / |c| := by apply div_pos εpos acpos
State after:
case neg
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : ¬c = 0
acpos : 0 < |c|
ε : ℝ
εpos : ε > 0
εcpos : 0 < ε / |c|
⊢ ∃ N, ∀ n ≥ N, |c * s n - c * a| < ε

State before:
case neg
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : ¬c = 0
acpos : 0 < |c|
ε : ℝ
εpos : ε > 0
εcpos : 0 < ε / |c|
⊢ ∃ N, ∀ n ≥ N, |c * s n - c * a| < ε
Tactic:
rcases cs (ε / |c|) εcpos with ⟨Ns, hs⟩
State after:
case neg.intro
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : ¬c = 0
acpos : 0 < |c|
ε : ℝ
εpos : ε > 0
εcpos : 0 < ε / |c|
Ns : ℕ
hs : ∀ n ≥ Ns, |s n - a| < ε / |c|
⊢ ∃ N, ∀ n ≥ N, |c * s n - c * a| < ε

State before:
case neg.intro
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : ¬c = 0
acpos : 0 < |c|
ε : ℝ
εpos : ε > 0
εcpos : 0 < ε / |c|
Ns : ℕ
hs : ∀ n ≥ Ns, |s n - a| < ε / |c|
⊢ ∃ N, ∀ n ≥ N, |c * s n - c * a| < ε
Tactic:
use Ns
State after:
case h
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : ¬c = 0
acpos : 0 < |c|
ε : ℝ
εpos : ε > 0
εcpos : 0 < ε / |c|
Ns : ℕ
hs : ∀ n ≥ Ns, |s n - a| < ε / |c|
⊢ ∀ n ≥ Ns, |c * s n - c * a| < ε

State before:
case h
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : ¬c = 0
acpos : 0 < |c|
ε : ℝ
εpos : ε > 0
εcpos : 0 < ε / |c|
Ns : ℕ
hs : ∀ n ≥ Ns, |s n - a| < ε / |c|
⊢ ∀ n ≥ Ns, |c * s n - c * a| < ε
Tactic:
intro n ngt
State after:
case h
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : ¬c = 0
acpos : 0 < |c|
ε : ℝ
εpos : ε > 0
εcpos : 0 < ε / |c|
Ns : ℕ
hs : ∀ n ≥ Ns, |s n - a| < ε / |c|
n : ℕ
ngt : n ≥ Ns
⊢ |c * s n - c * a| < ε

State before:
case h
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : ¬c = 0
acpos : 0 < |c|
ε : ℝ
εpos : ε > 0
εcpos : 0 < ε / |c|
Ns : ℕ
hs : ∀ n ≥ Ns, |s n - a| < ε / |c|
n : ℕ
ngt : n ≥ Ns
⊢ |c * s n - c * a| < ε
Tactic:
calc
  |c * s n - c * a| = |c| * |s n - a| := by rw [← abs_mul, mul_sub]
  _ < |c| * (ε / |c|) := (mul_lt_mul_of_pos_left (hs n ngt) acpos)
  _ = ε := mul_div_cancel₀ _ (ne_of_lt acpos).symm
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

State before:
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : ¬c = 0
acpos : 0 < |c|
ε : ℝ
εpos : ε > 0
⊢ 0 < ε / |c|
Tactic:
apply div_pos εpos acpos
State after:
no goals

State before:
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : ¬c = 0
acpos : 0 < |c|
ε : ℝ
εpos : ε > 0
εcpos : 0 < ε / |c|
Ns : ℕ
hs : ∀ n ≥ Ns, |s n - a| < ε / |c|
n : ℕ
ngt : n ≥ Ns
⊢ |c * s n - c * a| = |c| * |s n - a|
Tactic:
rw [← abs_mul, mul_sub]
State after:
no goals