no goals
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.790578
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
x : E
⊢ HasSum (fun i => ↑(↑b.repr x) i • (fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) x
simpa using b.hasSum_repr_symm (b.repr x)