Theorem: tends_to_sub (FM2023Exrcise/section02_reals/sheet5.lean)

State before:
a b : ℕ → ℝ
t u : ℝ
ha : tends_to a t
hb : tends_to b u
⊢ tends_to (fun n => a n - b n) (t - u)
Tactic:
have hb' := tends_to_neg hb
State after:
a b : ℕ → ℝ
t u : ℝ
ha : tends_to a t
hb : tends_to b u
hb' : tends_to (fun n => -b n) (-u)
⊢ tends_to (fun n => a n - b n) (t - u)

State before:
a b : ℕ → ℝ
t u : ℝ
ha : tends_to a t
hb : tends_to b u
hb' : tends_to (fun n => -b n) (-u)
⊢ tends_to (fun n => a n - b n) (t - u)
Tactic:
have h'  := tends_to_add ha hb'
State after:
a b : ℕ → ℝ
t u : ℝ
ha : tends_to a t
hb : tends_to b u
hb' : tends_to (fun n => -b n) (-u)
h' : tends_to (fun n => a n + -b n) (t + -u)
⊢ tends_to (fun n => a n - b n) (t - u)

State before:
a b : ℕ → ℝ
t u : ℝ
ha : tends_to a t
hb : tends_to b u
hb' : tends_to (fun n => -b n) (-u)
h' : tends_to (fun n => a n + -b n) (t + -u)
⊢ tends_to (fun n => a n - b n) (t - u)
Tactic:
apply h'
State after:
no goals