no goals
ι : Type u_1
ι' : Type ?u.817499
𝕜 : Type u_2
inst✝⁹ : IsROrC 𝕜
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
E' : Type ?u.817528
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : InnerProductSpace 𝕜 E'
F : Type ?u.817546
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type ?u.817566
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
v : EuclideanSpace 𝕜 ι
⊢ ∑ i : ι, v i • ↑b i = ↑(LinearIsometryEquiv.symm b.repr) v
simpa using (b.toBasis.equivFun_symm_apply v).symm