ι : Type u_1
ι' : Type ?u.788937
𝕜 : Type u_2
inst✝⁹ : IsROrC 𝕜
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
E' : Type ?u.788966
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : InnerProductSpace 𝕜 E'
F : Type ?u.788984
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type ?u.789004
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
⊢ ↑(Basis.ofEquivFun b.repr.toLinearEquiv) = ↑b
ι : Type u_1
ι' : Type ?u.788937
𝕜 : Type u_2
inst✝⁹ : IsROrC 𝕜
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
E' : Type ?u.788966
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : InnerProductSpace 𝕜 E'
F : Type ?u.788984
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type ?u.789004
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
⊢ ↑(OrthonormalBasis.toBasis b) = ↑b
rw [OrthonormalBasis.toBasis]
case h
ι : Type u_1
ι' : Type ?u.788937
𝕜 : Type u_2
inst✝⁹ : IsROrC 𝕜
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
E' : Type ?u.788966
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : InnerProductSpace 𝕜 E'
F : Type ?u.788984
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type ?u.789004
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
j : ι
⊢ ↑(Basis.ofEquivFun b.repr.toLinearEquiv) j = ↑b j
ι : Type u_1
ι' : Type ?u.788937
𝕜 : Type u_2
inst✝⁹ : IsROrC 𝕜
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
E' : Type ?u.788966
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : InnerProductSpace 𝕜 E'
F : Type ?u.788984
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type ?u.789004
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
⊢ ↑(Basis.ofEquivFun b.repr.toLinearEquiv) = ↑b
ext j
no goals
case h
ι : Type u_1
ι' : Type ?u.788937
𝕜 : Type u_2
inst✝⁹ : IsROrC 𝕜
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
E' : Type ?u.788966
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : InnerProductSpace 𝕜 E'
F : Type ?u.788984
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type ?u.789004
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
j : ι
⊢ ↑(Basis.ofEquivFun b.repr.toLinearEquiv) j = ↑b j
classical
  rw [Basis.coe_ofEquivFun]
  congr
case h
ι : Type u_1
ι' : Type ?u.788937
𝕜 : Type u_2
inst✝⁹ : IsROrC 𝕜
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
E' : Type ?u.788966
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : InnerProductSpace 𝕜 E'
F : Type ?u.788984
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type ?u.789004
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
j : ι
⊢ (fun i => ↑(LinearEquiv.symm b.repr.toLinearEquiv) (update 0 i 1)) j = ↑b j
case h
ι : Type u_1
ι' : Type ?u.788937
𝕜 : Type u_2
inst✝⁹ : IsROrC 𝕜
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
E' : Type ?u.788966
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : InnerProductSpace 𝕜 E'
F : Type ?u.788984
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type ?u.789004
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
j : ι
⊢ ↑(Basis.ofEquivFun b.repr.toLinearEquiv) j = ↑b j
rw [Basis.coe_ofEquivFun]
no goals
case h
ι : Type u_1
ι' : Type ?u.788937
𝕜 : Type u_2
inst✝⁹ : IsROrC 𝕜
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
E' : Type ?u.788966
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : InnerProductSpace 𝕜 E'
F : Type ?u.788984
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type ?u.789004
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
j : ι
⊢ (fun i => ↑(LinearEquiv.symm b.repr.toLinearEquiv) (update 0 i 1)) j = ↑b j
congr