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

State before:
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : c < 0
⊢ TendsTo (fun n => c * a n) (c * t)
Tactic:
have hc' : 0 < -c := neg_pos.mpr hc
State after:
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : c < 0
hc' : 0 < -c
⊢ TendsTo (fun n => c * a n) (c * t)

State before:
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : c < 0
hc' : 0 < -c
⊢ TendsTo (fun n => c * a n) (c * t)
Tactic:
intro ε hε
State after:
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : c < 0
hc' : 0 < -c
ε : ℝ
hε : ε > 0
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |(fun n => c * a n) n - c * t| < ε

State before:
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : c < 0
hc' : 0 < -c
ε : ℝ
hε : ε > 0
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |(fun n => c * a n) n - c * t| < ε
Tactic:
obtain ⟨X, hX⟩ := h (ε / -c) (div_pos hε hc')
State after:
case intro
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : c < 0
hc' : 0 < -c
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / -c
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |(fun n => c * a n) n - c * t| < ε

State before:
case intro
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : c < 0
hc' : 0 < -c
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / -c
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |(fun n => c * a n) n - c * t| < ε
Tactic:
use X
State after:
case h
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : c < 0
hc' : 0 < -c
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / -c
⊢ ∀ (n : ℕ), X ≤ n → |(fun n => c * a n) n - c * t| < ε

State before:
case h
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : c < 0
hc' : 0 < -c
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / -c
⊢ ∀ (n : ℕ), X ≤ n → |(fun n => c * a n) n - c * t| < ε
Tactic:
intro n hn
State after:
case h
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : c < 0
hc' : 0 < -c
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / -c
n : ℕ
hn : X ≤ n
⊢ |(fun n => c * a n) n - c * t| < ε

State before:
case h
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : c < 0
hc' : 0 < -c
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / -c
n : ℕ
hn : X ≤ n
⊢ |(fun n => c * a n) n - c * t| < ε
Tactic:
specialize hX n hn
State after:
case h
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : c < 0
hc' : 0 < -c
ε : ℝ
hε : ε > 0
X n : ℕ
hn : X ≤ n
hX : |a n - t| < ε / -c
⊢ |(fun n => c * a n) n - c * t| < ε

State before:
case h
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : c < 0
hc' : 0 < -c
ε : ℝ
hε : ε > 0
X n : ℕ
hn : X ≤ n
hX : |a n - t| < ε / -c
⊢ |(fun n => c * a n) n - c * t| < ε
Tactic:
simp
State after:
case h
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : c < 0
hc' : 0 < -c
ε : ℝ
hε : ε > 0
X n : ℕ
hn : X ≤ n
hX : |a n - t| < ε / -c
⊢ |c * a n - c * t| < ε

State before:
case h
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : c < 0
hc' : 0 < -c
ε : ℝ
hε : ε > 0
X n : ℕ
hn : X ≤ n
hX : |a n - t| < ε / -c
⊢ |c * a n - c * t| < ε
Tactic:
rw [← mul_sub, abs_mul, abs_of_neg hc]
State after:
case h
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : c < 0
hc' : 0 < -c
ε : ℝ
hε : ε > 0
X n : ℕ
hn : X ≤ n
hX : |a n - t| < ε / -c
⊢ -c * |a n - t| < ε

State before:
case h
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : c < 0
hc' : 0 < -c
ε : ℝ
hε : ε > 0
X n : ℕ
hn : X ≤ n
hX : |a n - t| < ε / -c
⊢ -c * |a n - t| < ε
Tactic:
exact (lt_div_iff' hc').mp hX
State after:
no goals