ι : Type u_1
ι' : Type ?u.767988
𝕜 : Type u_2
inst✝¹⁰ : IsROrC 𝕜
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.768017
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.768035
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.768055
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι
⊢ (fun i => EquivLike.coe (LinearIsometryEquiv.symm e) (EuclideanSpace.single i 1)) = fun i =>
    EquivLike.coe (LinearIsometryEquiv.symm e) (EuclideanSpace.single i 1)
ι : Type u_1
ι' : Type ?u.767988
𝕜 : Type u_2
inst✝¹⁰ : IsROrC 𝕜
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.768017
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.768035
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.768055
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι
⊢ ↑{ repr := e } = fun i => ↑(LinearIsometryEquiv.symm e) (EuclideanSpace.single i 1)
dsimp only [FunLike.coe]
case h
ι : Type u_1
ι' : Type ?u.767988
𝕜 : Type u_2
inst✝¹⁰ : IsROrC 𝕜
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.768017
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.768035
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.768055
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι
x✝ : ι
⊢ EquivLike.coe (LinearIsometryEquiv.symm e) (EuclideanSpace.single x✝ 1) =
    EquivLike.coe (LinearIsometryEquiv.symm e) (EuclideanSpace.single x✝ 1)
ι : Type u_1
ι' : Type ?u.767988
𝕜 : Type u_2
inst✝¹⁰ : IsROrC 𝕜
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.768017
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.768035
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.768055
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι
⊢ (fun i => EquivLike.coe (LinearIsometryEquiv.symm e) (EuclideanSpace.single i 1)) = fun i =>
    EquivLike.coe (LinearIsometryEquiv.symm e) (EuclideanSpace.single i 1)
funext
no goals
case h
ι : Type u_1
ι' : Type ?u.767988
𝕜 : Type u_2
inst✝¹⁰ : IsROrC 𝕜
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.768017
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.768035
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.768055
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι
x✝ : ι
⊢ EquivLike.coe (LinearIsometryEquiv.symm e) (EuclideanSpace.single x✝ 1) =
    EquivLike.coe (LinearIsometryEquiv.symm e) (EuclideanSpace.single x✝ 1)
congr!