z w : ℂ
⊢ (z.re + w.re) * (z.re + w.re) + (z.im + w.im) * (z.im + w.im) =
    z.re * z.re + z.im * z.im + (w.re * w.re + w.im * w.im) + 2 * (z.re * w.re - z.im * -w.im)
z w : ℂ
⊢ ↑normSq (z + w) = ↑normSq z + ↑normSq w + 2 * (z * ↑(starRingEnd ℂ) w).re
dsimp [normSq]
no goals
z w : ℂ
⊢ (z.re + w.re) * (z.re + w.re) + (z.im + w.im) * (z.im + w.im) =
    z.re * z.re + z.im * z.im + (w.re * w.re + w.im * w.im) + 2 * (z.re * w.re - z.im * -w.im)
ring