ι : Type u_1
ι' : Type ?u.771553
𝕜 : Type u_2
inst✝¹⁰ : IsROrC 𝕜
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.771582
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.771600
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.771620
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : OrthonormalBasis ι 𝕜 E
i : ι
⊢ EquivLike.coe (LinearIsometryEquiv.symm b.repr) (EuclideanSpace.single i 1) =
    EquivLike.coe (LinearIsometryEquiv.symm b.repr) (EuclideanSpace.single i 1)
ι : Type u_1
ι' : Type ?u.771553
𝕜 : Type u_2
inst✝¹⁰ : IsROrC 𝕜
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.771582
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.771600
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.771620
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : OrthonormalBasis ι 𝕜 E
i : ι
⊢ ↑(LinearIsometryEquiv.symm b.repr) (EuclideanSpace.single i 1) = ↑b i
dsimp only [FunLike.coe]
no goals
ι : Type u_1
ι' : Type ?u.771553
𝕜 : Type u_2
inst✝¹⁰ : IsROrC 𝕜
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.771582
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.771600
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.771620
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : OrthonormalBasis ι 𝕜 E
i : ι
⊢ EquivLike.coe (LinearIsometryEquiv.symm b.repr) (EuclideanSpace.single i 1) =
    EquivLike.coe (LinearIsometryEquiv.symm b.repr) (EuclideanSpace.single i 1)
congr!