no goals
α : Type u_1
β : Type u_2
γ : Type ?u.814079
δ : Type ?u.814082
inst✝³ : AddCommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : StarAddMonoid α
inst✝ : ContinuousStar α
f : β → α
a : α
hf : Summable fun b => Star.star (f b)
⊢ Summable f
simpa only [star_star] using hf.star