no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1385935
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
r : 𝕜
⊢ inner x (r • y) = r * inner x y
rw [← inner_conj_symm, inner_smul_left, RingHom.map_mul, conj_conj, inner_conj_symm]