no goals
K : Type u_1
E : Type ?u.6777307
inst✝ : IsROrC K
a : K
h : ‖a‖ ≤ ↑re a
⊢ ↑im a = 0
simpa only [mul_self_norm a, normSq_apply, self_eq_add_right, mul_self_eq_zero]
  using congr_arg (fun z => z * z) ((re_le_norm a).antisymm h)