no goals
ι : Type u_3
𝕜 : Type u_1
inst✝⁵ : IsROrC 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.879353
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
U : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ U }
b : HilbertBasis ι 𝕜 { x // x ∈ U }
x : E
⊢ HasSum
    (fun i =>
      inner (↑((fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i)) x •
        (fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i)
    (↑(orthogonalProjection U) x)
simpa only [b.repr_apply_apply, inner_orthogonalProjection_eq_of_mem_left] using
  b.hasSum_repr (orthogonalProjection U x)