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

State before:
a : ℕ → ℝ
t : ℝ
⊢ TendsTo a t ↔ TendsTo (fun n => a n - t) 0
Tactic:
constructor
State after:
case mp
a : ℕ → ℝ
t : ℝ
⊢ TendsTo a t → TendsTo (fun n => a n - t) 0

case mpr
a : ℕ → ℝ
t : ℝ
⊢ TendsTo (fun n => a n - t) 0 → TendsTo a t

State before:
case mp
a : ℕ → ℝ
t : ℝ
⊢ TendsTo a t → TendsTo (fun n => a n - t) 0
Tactic:
intro h
State after:
case mp
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
⊢ TendsTo (fun n => a n - t) 0

State before:
case mp
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
⊢ TendsTo (fun n => a n - t) 0
Tactic:
simpa using tendsTo_sub h (tendsTo_const t)
State after:
no goals

State before:
case mpr
a : ℕ → ℝ
t : ℝ
⊢ TendsTo (fun n => a n - t) 0 → TendsTo a t
Tactic:
intro h
State after:
case mpr
a : ℕ → ℝ
t : ℝ
h : TendsTo (fun n => a n - t) 0
⊢ TendsTo a t

State before:
case mpr
a : ℕ → ℝ
t : ℝ
h : TendsTo (fun n => a n - t) 0
⊢ TendsTo a t
Tactic:
simpa using tendsTo_add h (tendsTo_const t)
State after:
no goals