no goals
𝕜 : Type u_1
E : Type u_2
E' : Type ?u.63572
F : Type ?u.63575
G : Type ?u.63578
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
x y : E
⊢ inner (↑(↑ℝ T) x) y = inner x (↑(↑ℝ T) y)
simp [hT x y, real_inner_eq_re_inner, LinearMap.coe_restrictScalars ℝ]