no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2760926
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.2760975
ι' : Type ?u.2760978
ι'' : Type ?u.2760981
E' : Type u_3
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
E'' : Type ?u.2761002
inst✝¹ : NormedAddCommGroup E''
inst✝ : InnerProductSpace 𝕜 E''
f : E →ₗᵢ[𝕜] E'
x y : E
⊢ inner (↑f x) (↑f y) = inner x y
simp [inner_eq_sum_norm_sq_div_four, ← f.norm_map]