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

State before:
a b : ℕ → ℝ
t u : ℝ
h1 : TendsTo (fun n => a n - b n) t
h2 : TendsTo b u
⊢ TendsTo a (t + u)
Tactic:
simpa using tendsTo_add h1 h2
State after:
no goals