no goals
x : ℂ
hx : x ≠ 0
⊢ exp (log x) = x
rw [log, exp_add_mul_I, ← ofReal_sin, sin_arg, ← ofReal_cos, cos_arg hx, ← ofReal_exp,
  Real.exp_log (abs.pos hx), mul_add, ofReal_div, ofReal_div,
  mul_div_cancel' _ (ofReal_ne_zero.2 <| abs.ne_zero hx), ← mul_assoc,
  mul_div_cancel' _ (ofReal_ne_zero.2 <| abs.ne_zero hx), re_add_im]