K : Type u_1
E : Type ?u.4701150
inst✝ : IsROrC K
z w : K
⊢ (↑re z + ↑re w) * (↑re z + ↑re w) + (↑im z + ↑im w) * (↑im z + ↑im w) =
    ↑re z * ↑re z + ↑im z * ↑im z + (↑re w * ↑re w + ↑im w * ↑im w) + 2 * (↑re z * ↑re w - ↑im z * -↑im w)
K : Type u_1
E : Type ?u.4701150
inst✝ : IsROrC K
z w : K
⊢ ↑normSq (z + w) = ↑normSq z + ↑normSq w + 2 * ↑re (z * ↑(starRingEnd K) w)
simp only [normSq_apply, map_add, isROrC_simps]
no goals
K : Type u_1
E : Type ?u.4701150
inst✝ : IsROrC K
z w : K
⊢ (↑re z + ↑re w) * (↑re z + ↑re w) + (↑im z + ↑im w) * (↑im z + ↑im w) =
    ↑re z * ↑re z + ↑im z * ↑im z + (↑re w * ↑re w + ↑im w * ↑im w) + 2 * (↑re z * ↑re w - ↑im z * -↑im w)
ring