Theorem: Section2sheet5solutions.tendsTo_sub (FormalisingMathematics2024/Solutions/Section02reals/Sheet5.lean)

State before:
a b : ℕ → ℝ
t u : ℝ
ha : TendsTo a t
hb : TendsTo b u
⊢ TendsTo (fun n => a n - b n) (t - u)
Tactic:
simpa [sub_eq_add_neg] using tendsTo_add ha (tendsTo_neg hb)
State after:
no goals