no goals
𝕜 : Type u_1
E : Type ?u.787535
F : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : Core 𝕜 F
x : F
⊢ ↑re (inner x x) = ‖x‖ * ‖x‖
rw [norm_eq_sqrt_inner, ← sqrt_mul inner_self_nonneg (re ⟪x, x⟫), sqrt_mul_self inner_self_nonneg]