case h.e'_3
𝕜 : Type u_2
E : Type u_3
F : Type ?u.1474372
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
l : ι →₀ 𝕜
v : ι → E
x : E
⊢ (sum l fun i a => a • inner x (v i)) = ∑ i in l.support, inner x (↑l i • v i)
𝕜 : Type u_2
E : Type u_3
F : Type ?u.1474372
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
l : ι →₀ 𝕜
v : ι → E
x : E
⊢ inner x (sum l fun i a => a • v i) = sum l fun i a => a • inner x (v i)
convert _root_.inner_sum (𝕜 := 𝕜) l.support (fun a => l a • v a) x
no goals
case h.e'_3
𝕜 : Type u_2
E : Type u_3
F : Type ?u.1474372
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
l : ι →₀ 𝕜
v : ι → E
x : E
⊢ (sum l fun i a => a • inner x (v i)) = ∑ i in l.support, inner x (↑l i • v i)
simp only [inner_smul_right, Finsupp.sum, smul_eq_mul]