no goals
z : ℂ
⊢ Abs.abs z.re < ↑abs z ↔ z.im ≠ 0
rw [Complex.abs, AbsoluteValue.coe_mk, MulHom.coe_mk, Real.lt_sqrt (abs_nonneg _), normSq_apply,
  _root_.sq_abs, ← sq, lt_add_iff_pos_right, mul_self_pos]