case pos
α : Type u_1
f : α → ℝ
hf : Summable f
⊢ (∑' (a : α), ↑(f a)) = ↑(∑' (a : α), f a)

case neg
α : Type u_1
f : α → ℝ
hf : ¬Summable f
⊢ (∑' (a : α), ↑(f a)) = ↑(∑' (a : α), f a)
α : Type u_1
f : α → ℝ
⊢ (∑' (a : α), ↑(f a)) = ↑(∑' (a : α), f a)
by_cases hf : Summable f
no goals
case pos
α : Type u_1
f : α → ℝ
hf : Summable f
⊢ (∑' (a : α), ↑(f a)) = ↑(∑' (a : α), f a)
exact (hasSum_coe.mpr hf.hasSum).tsum_eq
no goals
case neg
α : Type u_1
f : α → ℝ
hf : ¬Summable f
⊢ (∑' (a : α), ↑(f a)) = ↑(∑' (a : α), f a)
simp [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable (summable_coe.not.mpr hf)]