Theorem: sum_cons' (Ray/Analytic/Series.lean)

State before:
a : ℂ
f : ℕ → ℂ
h : Summable f
⊢ tsum (Stream'.cons a f) = a + tsum f
Tactic:
rcases h with ⟨g, h⟩
State after:
case intro
a : ℂ
f : ℕ → ℂ
g : ℂ
h : HasSum f g
⊢ tsum (Stream'.cons a f) = a + tsum f

State before:
case intro
a : ℂ
f : ℕ → ℂ
g : ℂ
h : HasSum f g
⊢ tsum (Stream'.cons a f) = a + tsum f
Tactic:
rw [HasSum.tsum_eq h]
State after:
case intro
a : ℂ
f : ℕ → ℂ
g : ℂ
h : HasSum f g
⊢ tsum (Stream'.cons a f) = a + g

State before:
case intro
a : ℂ
f : ℕ → ℂ
g : ℂ
h : HasSum f g
⊢ tsum (Stream'.cons a f) = a + g
Tactic:
rw [HasSum.tsum_eq _]
State after:
a : ℂ
f : ℕ → ℂ
g : ℂ
h : HasSum f g
⊢ HasSum (fun b => Stream'.cons a f b) (a + g)

State before:
a : ℂ
f : ℕ → ℂ
g : ℂ
h : HasSum f g
⊢ HasSum (fun b => Stream'.cons a f b) (a + g)
Tactic:
exact sum_cons h
State after:
no goals