z w : ℂ
⊢ ↑normSq z + ↑normSq (-w) + 2 * (z * ↑(starRingEnd ℂ) (-w)).re =
    ↑normSq z + ↑normSq w - 2 * (z * ↑(starRingEnd ℂ) w).re
z w : ℂ
⊢ ↑normSq (z - w) = ↑normSq z + ↑normSq w - 2 * (z * ↑(starRingEnd ℂ) w).re
rw [sub_eq_add_neg, normSq_add]
z w : ℂ
⊢ ↑normSq z + ↑normSq w + -(2 * (z * ↑(starRingEnd ℂ) w).re) = ↑normSq z + ↑normSq w - 2 * (z * ↑(starRingEnd ℂ) w).re
z w : ℂ
⊢ ↑normSq z + ↑normSq (-w) + 2 * (z * ↑(starRingEnd ℂ) (-w)).re =
    ↑normSq z + ↑normSq w - 2 * (z * ↑(starRingEnd ℂ) w).re
simp only [RingHom.map_neg, mul_neg, neg_re, normSq_neg]
no goals
z w : ℂ
⊢ ↑normSq z + ↑normSq w + -(2 * (z * ↑(starRingEnd ℂ) w).re) = ↑normSq z + ↑normSq w - 2 * (z * ↑(starRingEnd ℂ) w).re
ring