no goals
𝕜 : Type u_3
E : Type u_4
F : Type ?u.1509183
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
dec : DecidableEq ι
α : ι → Type u_2
inst✝¹ : (i : ι) → AddZeroClass (α i)
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
f : (i : ι) → α i → E
l : Π₀ (i : ι), α i
x : E
⊢ inner x (sum l f) = sum l fun i a => inner x (f i a)
simp (config := { contextual := true }) only [Dfinsupp.sum, _root_.inner_sum, smul_eq_mul]