no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2058385
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
hv : Orthonormal 𝕜 v
l₁ l₂ : ι →₀ 𝕜
⊢ inner (↑(Finsupp.total ι E 𝕜 v) l₁) (↑(Finsupp.total ι E 𝕜 v) l₂) =
    Finsupp.sum l₂ fun i y => ↑(starRingEnd ((fun x => 𝕜) i)) (↑l₁ i) * y
simp only [l₂.total_apply _, Finsupp.inner_sum, hv.inner_left_finsupp, mul_comm, smul_eq_mul]