no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.4042510
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
G : Type ?u.4042559
x : E
⊢ inner x (I • x) = 0
simp [real_inner_eq_re_inner 𝕜, inner_smul_right]