no goals
𝕜 : Type ?u.3140024
E : Type ?u.3140027
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x : F
r : ℝ
⊢ inner (r • x) x = r * (‖x‖ * ‖x‖)
rw [real_inner_smul_left, ← real_inner_self_eq_norm_mul_norm]