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.905970
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
v : ι → E
hv : Orthonormal 𝕜 v
hsp : ⊤ ≤ topologicalClosure (span 𝕜 (Set.range v))
⊢ (fun i => ↑(LinearIsometryEquiv.symm (HilbertBasis.mk hv hsp).repr) (lp.single 2 i 1)) = v
apply funext <| Orthonormal.linearIsometryEquiv_symm_apply_single_one hv hsp