𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
x : E
y : NormedSpace.Dual 𝕜 E
⊢ ↑(↑(toDual 𝕜 E) (↑(LinearIsometryEquiv.symm (toDual 𝕜 E)) y)) x = ↑y x
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
x : E
y : NormedSpace.Dual 𝕜 E
⊢ inner (↑(LinearIsometryEquiv.symm (toDual 𝕜 E)) y) x = ↑y x
rw [← toDual_apply]
no goals
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
x : E
y : NormedSpace.Dual 𝕜 E
⊢ ↑(↑(toDual 𝕜 E) (↑(LinearIsometryEquiv.symm (toDual 𝕜 E)) y)) x = ↑y x
simp only [LinearIsometryEquiv.apply_symm_apply]