no goals
K : Type u_1
E : Type ?u.7033014
inst✝ : IsROrC K
x : K
⊢ ‖x + ↑(starRingEnd K) x‖ ^ 2 = ↑re (x + ↑(starRingEnd K) x) ^ 2
rw [add_conj, ← ofReal_ofNat, ← ofReal_mul, norm_ofReal, sq_abs, ofReal_re]