case h.e'_3
𝕜 : Type u_2
E : Type u_3
F : Type ?u.1418390
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 => ↑(starRingEnd 𝕜) a • inner (v i) x) = ∑ i in l.support, inner (↑l i • v i) x
𝕜 : Type u_2
E : Type u_3
F : Type ?u.1418390
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 (sum l fun i a => a • v i) x = sum l fun i a => ↑(starRingEnd 𝕜) a • inner (v i) x
convert _root_.sum_inner (𝕜 := 𝕜) 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.1418390
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 => ↑(starRingEnd 𝕜) a • inner (v i) x) = ∑ i in l.support, inner (↑l i • v i) x
simp only [inner_smul_left, Finsupp.sum, smul_eq_mul]