no goals
E : Type ?u.13792
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z w : ℂ
h : z.im = w.im
⊢ dist z w = dist z.re w.re
rw [dist_eq_re_im, h, sub_self, zero_pow two_pos, add_zero, Real.sqrt_sq_eq_abs, Real.dist_eq]