no goals
V : Type ?u.446095
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type ?u.446104
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g : NormedAddGroupHom V₁ V₂
ι : Type u_1
s : Finset ι
f : ι → NormedAddGroupHom V₁ V₂
v : V₁
⊢ ↑(∑ i in s, f i) v = ∑ i in s, ↑(f i) v
simp only [coe_sum, Finset.sum_apply]