α : Type u_1
β : Type u_2
γ : Type ?u.13763
δ : Type ?u.13766
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f g : β → α
a b : α
s : Finset β
ha : Summable f
⊢ HasSum f (Classical.choose (_ : Summable fun b => f b))
α : Type u_1
β : Type u_2
γ : Type ?u.13763
δ : Type ?u.13766
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f g : β → α
a b : α
s : Finset β
ha : Summable f
⊢ HasSum f (∑' (b : β), f b)
simp only [tsum_def, ha, dite_true]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.13763
δ : Type ?u.13766
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f g : β → α
a b : α
s : Finset β
ha : Summable f
⊢ HasSum f (Classical.choose (_ : Summable fun b => f b))
exact Classical.choose_spec ha