no goals
ι : Type u_3
ι' : Type ?u.1163327
𝕜 : Type u_1
inst✝⁹ : IsROrC 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
E' : Type ?u.1163356
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : InnerProductSpace 𝕜 E'
F : Type ?u.1163374
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type ?u.1163394
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
v : ι → E
hon : Orthonormal 𝕜 v
hsp : ⊤ ≤ span 𝕜 (range v)
⊢ ↑(OrthonormalBasis.mk hon hsp) = v
classical rw [OrthonormalBasis.mk, _root_.Basis.coe_toOrthonormalBasis, Basis.coe_mk]
no goals
ι : Type u_3
ι' : Type ?u.1163327
𝕜 : Type u_1
inst✝⁹ : IsROrC 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
E' : Type ?u.1163356
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : InnerProductSpace 𝕜 E'
F : Type ?u.1163374
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type ?u.1163394
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
v : ι → E
hon : Orthonormal 𝕜 v
hsp : ⊤ ≤ span 𝕜 (range v)
⊢ ↑(OrthonormalBasis.mk hon hsp) = v
rw [OrthonormalBasis.mk, _root_.Basis.coe_toOrthonormalBasis, Basis.coe_mk]