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