Theorem: convergesTo_mul_const (LeanCourse/Assignments/Assignment3.lean)

State before:
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
⊢ SequentialLimit (fun n => c * s n) (c * a)
Tactic:
intro ε hε
State after:
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
⊢ ∃ N, ∀ n ≥ N, |(fun n => c * s n) n - c * a| < ε

State before:
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
⊢ ∃ N, ∀ n ≥ N, |(fun n => c * s n) n - c * a| < ε
Tactic:
obtain ⟨N, hN⟩ := hs (ε / max |c| 1) (by positivity)
State after:
case intro
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s n - a| < ε / max |c| 1
⊢ ∃ N, ∀ n ≥ N, |(fun n => c * s n) n - c * a| < ε

State before:
case intro
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s n - a| < ε / max |c| 1
⊢ ∃ N, ∀ n ≥ N, |(fun n => c * s n) n - c * a| < ε
Tactic:
use N
State after:
case h
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s n - a| < ε / max |c| 1
⊢ ∀ n ≥ N, |(fun n => c * s n) n - c * a| < ε

State before:
case h
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s n - a| < ε / max |c| 1
⊢ ∀ n ≥ N, |(fun n => c * s n) n - c * a| < ε
Tactic:
intro n hn
State after:
case h
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s n - a| < ε / max |c| 1
n : ℕ
hn : n ≥ N
⊢ |(fun n => c * s n) n - c * a| < ε

State before:
case h
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s n - a| < ε / max |c| 1
n : ℕ
hn : n ≥ N
⊢ |(fun n => c * s n) n - c * a| < ε
Tactic:
specialize hN n hn
State after:
case h
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
N n : ℕ
hn : n ≥ N
hN : |s n - a| < ε / max |c| 1
⊢ |(fun n => c * s n) n - c * a| < ε

State before:
case h
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
N n : ℕ
hn : n ≥ N
hN : |s n - a| < ε / max |c| 1
⊢ |(fun n => c * s n) n - c * a| < ε
Tactic:
simp
State after:
case h
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
N n : ℕ
hn : n ≥ N
hN : |s n - a| < ε / max |c| 1
⊢ |c * s n - c * a| < ε

State before:
case h
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
N n : ℕ
hn : n ≥ N
hN : |s n - a| < ε / max |c| 1
⊢ |c * s n - c * a| < ε
Tactic:
calc |c * s n - c * a|
    = |c * (s n - a)| := by ring
  _ = |c| * |s n - a| := by exact abs_mul c (s n - a)
  _ ≤ max |c| 1 * |s n - a| := by gcongr; exact le_max_left |c| 1
  _ < max |c| 1 * (ε / max |c| 1) := by gcongr
  _ = ε := by refine mul_div_cancel' ε ?hb; positivity
State after:
no goals

State before:
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
⊢ ε / max |c| 1 > 0
Tactic:
positivity
State after:
no goals

State before:
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
N n : ℕ
hn : n ≥ N
hN : |s n - a| < ε / max |c| 1
⊢ |c * s n - c * a| = |c * (s n - a)|
Tactic:
ring
State after:
no goals

State before:
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
N n : ℕ
hn : n ≥ N
hN : |s n - a| < ε / max |c| 1
⊢ |c * (s n - a)| = |c| * |s n - a|
Tactic:
exact abs_mul c (s n - a)
State after:
no goals

State before:
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
N n : ℕ
hn : n ≥ N
hN : |s n - a| < ε / max |c| 1
⊢ |c| * |s n - a| ≤ max |c| 1 * |s n - a|
Tactic:
gcongr
State after:
case h
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
N n : ℕ
hn : n ≥ N
hN : |s n - a| < ε / max |c| 1
⊢ |c| ≤ max |c| 1

State before:
case h
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
N n : ℕ
hn : n ≥ N
hN : |s n - a| < ε / max |c| 1
⊢ |c| ≤ max |c| 1
Tactic:
exact le_max_left |c| 1
State after:
no goals

State before:
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
N n : ℕ
hn : n ≥ N
hN : |s n - a| < ε / max |c| 1
⊢ max |c| 1 * |s n - a| < max |c| 1 * (ε / max |c| 1)
Tactic:
gcongr
State after:
no goals

State before:
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
N n : ℕ
hn : n ≥ N
hN : |s n - a| < ε / max |c| 1
⊢ max |c| 1 * (ε / max |c| 1) = ε
Tactic:
refine mul_div_cancel' ε ?hb
State after:
case hb
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
N n : ℕ
hn : n ≥ N
hN : |s n - a| < ε / max |c| 1
⊢ max |c| 1 ≠ 0

State before:
case hb
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
N n : ℕ
hn : n ≥ N
hN : |s n - a| < ε / max |c| 1
⊢ max |c| 1 ≠ 0
Tactic:
positivity
State after:
no goals