no goals
ι : Type u_1
ι' : Type ?u.796257
𝕜 : Type u_2
inst✝⁹ : IsROrC 𝕜
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
E' : Type ?u.796286
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : InnerProductSpace 𝕜 E'
F : Type ?u.796304
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type ?u.796324
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
i : ι
⊢ ↑(↑(OrthonormalBasis.toBasis b).repr x) i = ↑b.repr x i
rw [← Basis.equivFun_apply, OrthonormalBasis.coe_toBasis_repr,
  LinearIsometryEquiv.coe_toLinearEquiv]