no goals
ι : Type u_3
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.899044
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
v : ι → E
hv : Orthonormal 𝕜 v
h : ⊤ ≤ topologicalClosure (span 𝕜 (Set.range v))
i : ι
⊢ ↑(LinearIsometryEquiv.symm
          (IsHilbertSum.linearIsometryEquiv
            (_ : IsHilbertSum 𝕜 (fun x => 𝕜) fun i => LinearIsometry.toSpanSingleton 𝕜 E (_ : ‖v i‖ = 1))))
      (lp.single 2 i 1) =
    v i
rw [IsHilbertSum.linearIsometryEquiv_symm_apply_single, LinearIsometry.toSpanSingleton_apply,
  one_smul]