no goals
K : Type u_1
E : Type ?u.5548479
inst✝ : IsROrC K
z w : K
⊢ ↑re (z / w) = ↑re z * ↑re w / ↑normSq w + ↑im z * ↑im w / ↑normSq w
simp only [div_eq_mul_inv, mul_assoc, sub_eq_add_neg, neg_mul, mul_neg, neg_neg, map_neg,
  isROrC_simps]