no goals
x : ℂ
hx₁ : -π < x.im
hx₂ : x.im ≤ π
⊢ log (exp x) = x
rw [log, abs_exp, Real.log_exp, exp_eq_exp_re_mul_sin_add_cos, ← ofReal_exp,
  arg_mul_cos_add_sin_mul_I (Real.exp_pos _) ⟨hx₁, hx₂⟩, re_add_im]