no goals
F : Type ?u.976970
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : AddCommMonoid β
inst✝ : LipschitzAdd β
ι : Type u_1
s : Finset ι
f : ι → α →ᵇ β
a : α
⊢ ↑(∑ i in s, f i) a = ∑ i in s, ↑(f i) a
simp