no goals
ι : Type u_1
ι' : Type ?u.774819
𝕜 : Type u_2
inst✝¹⁰ : IsROrC 𝕜
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.774848
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.774866
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.774886
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : OrthonormalBasis ι 𝕜 E
i : ι
⊢ ↑b.repr (↑b i) = EuclideanSpace.single i 1
rw [← b.repr_symm_single i, LinearIsometryEquiv.apply_symm_apply]