no goals
ι : Type u_1
ι' : Type ?u.1157885
𝕜 : Type u_2
inst✝⁹ : IsROrC 𝕜
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
E' : Type ?u.1157914
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : InnerProductSpace 𝕜 E'
F : Type ?u.1157932
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type ?u.1157952
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
v : Basis ι 𝕜 E
hv : Orthonormal 𝕜 ↑v
⊢ ↑(Basis.toOrthonormalBasis v hv) = ↑(OrthonormalBasis.toBasis (Basis.toOrthonormalBasis v hv))
classical rw [OrthonormalBasis.coe_toBasis]
no goals
ι : Type u_1
ι' : Type ?u.1157885
𝕜 : Type u_2
inst✝⁹ : IsROrC 𝕜
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
E' : Type ?u.1157914
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : InnerProductSpace 𝕜 E'
F : Type ?u.1157932
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type ?u.1157952
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
v : Basis ι 𝕜 E
hv : Orthonormal 𝕜 ↑v
⊢ ↑(Basis.toOrthonormalBasis v hv) = ↑(OrthonormalBasis.toBasis (Basis.toOrthonormalBasis v hv))
rw [OrthonormalBasis.coe_toBasis]
no goals
ι : Type u_1
ι' : Type ?u.1157885
𝕜 : Type u_2
inst✝⁹ : IsROrC 𝕜
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
E' : Type ?u.1157914
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : InnerProductSpace 𝕜 E'
F : Type ?u.1157932
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type ?u.1157952
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
v : Basis ι 𝕜 E
hv : Orthonormal 𝕜 ↑v
⊢ ↑(OrthonormalBasis.toBasis (Basis.toOrthonormalBasis v hv)) = ↑v
simp