Theorem: Section2sheet6.tendsTo_sub_lim_iff (FormalisingMathematics2024/Section02reals/Sheet6.lean)

State before:
a : ℕ → ℝ
t : ℝ
⊢ TendsTo a t ↔ TendsTo (fun n => a n - t) 0
Tactic:
sorry
State after:
no goals