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

State before:
a : ℕ → ℝ
t c : ℝ
h : TendsTo a t
⊢ TendsTo (fun n => c * a n) (c * t)
Tactic:
obtain hc | rfl | hc := lt_trichotomy 0 c
State after:
case inl
a : ℕ → ℝ
t c : ℝ
h : TendsTo a t
hc : 0 < c
⊢ TendsTo (fun n => c * a n) (c * t)

case inr.inl
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
⊢ TendsTo (fun n => 0 * a n) (0 * t)

case inr.inr
a : ℕ → ℝ
t c : ℝ
h : TendsTo a t
hc : c < 0
⊢ TendsTo (fun n => c * a n) (c * t)

State before:
case inl
a : ℕ → ℝ
t c : ℝ
h : TendsTo a t
hc : 0 < c
⊢ TendsTo (fun n => c * a n) (c * t)
Tactic:
exact tendsTo_pos_const_mul h hc
State after:
no goals

State before:
case inr.inl
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
⊢ TendsTo (fun n => 0 * a n) (0 * t)
Tactic:
simpa using tendsTo_const 0
State after:
no goals

State before:
case inr.inr
a : ℕ → ℝ
t c : ℝ
h : TendsTo a t
hc : c < 0
⊢ TendsTo (fun n => c * a n) (c * t)
Tactic:
exact tendsTo_neg_const_mul h hc
State after:
no goals