no goals
E : Type ?u.15628
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
⊢ dist (↑(starRingEnd ℂ) z) z = 2 * Abs.abs z.im
rw [dist_of_re_eq (conj_re z), conj_im, dist_comm, Real.dist_eq, sub_neg_eq_add, ← two_mul,
  _root_.abs_mul, abs_of_pos (zero_lt_two' ℝ)]