x : ℝ
hx : x < 0
y : ℝ
⊢ (Complex.exp (Complex.log ↑x * ↑y)).re = exp (log x * y) * cos (y * π)

case hnc
x : ℝ
hx : x < 0
y : ℝ
⊢ ¬↑x = 0
x : ℝ
hx : x < 0
y : ℝ
⊢ x ^ y = exp (log x * y) * cos (y * π)
rw [rpow_def, Complex.cpow_def, if_neg]
x : ℝ
hx : x < 0
y : ℝ
this : Complex.log ↑x * ↑y = ↑(log (-x) * y) + ↑(y * π) * Complex.I
⊢ (Complex.exp (Complex.log ↑x * ↑y)).re = exp (log x * y) * cos (y * π)

case hnc
x : ℝ
hx : x < 0
y : ℝ
⊢ ¬↑x = 0
x : ℝ
hx : x < 0
y : ℝ
⊢ (Complex.exp (Complex.log ↑x * ↑y)).re = exp (log x * y) * cos (y * π)

case hnc
x : ℝ
hx : x < 0
y : ℝ
⊢ ¬↑x = 0
have : Complex.log x * y = ↑(log (-x) * y) + ↑(y * π) * Complex.I := by
  simp only [Complex.log, abs_of_neg hx, Complex.arg_ofReal_of_neg hx, Complex.abs_ofReal,
    Complex.ofReal_mul]
  ring
x : ℝ
hx : x < 0
y : ℝ
⊢ (↑(log (-x)) + ↑π * Complex.I) * ↑y = ↑(log (-x)) * ↑y + ↑y * ↑π * Complex.I
x : ℝ
hx : x < 0
y : ℝ
⊢ Complex.log ↑x * ↑y = ↑(log (-x) * y) + ↑(y * π) * Complex.I
simp only [Complex.log, abs_of_neg hx, Complex.arg_ofReal_of_neg hx, Complex.abs_ofReal,
  Complex.ofReal_mul]
no goals
x : ℝ
hx : x < 0
y : ℝ
⊢ (↑(log (-x)) + ↑π * Complex.I) * ↑y = ↑(log (-x)) * ↑y + ↑y * ↑π * Complex.I
ring
x : ℝ
hx : x < 0
y : ℝ
this : Complex.log ↑x * ↑y = ↑(log (-x) * y) + ↑(y * π) * Complex.I
⊢ exp (log x * y) * cos (y * π) + ((↑(exp (log x * y) * sin (y * π))).re * 0 - 0 * Complex.I.im) =
    exp (log x * y) * cos (y * π)
x : ℝ
hx : x < 0
y : ℝ
this : Complex.log ↑x * ↑y = ↑(log (-x) * y) + ↑(y * π) * Complex.I
⊢ (Complex.exp (Complex.log ↑x * ↑y)).re = exp (log x * y) * cos (y * π)
rw [this, Complex.exp_add_mul_I, ← Complex.ofReal_exp, ← Complex.ofReal_cos, ←
  Complex.ofReal_sin, mul_add, ← Complex.ofReal_mul, ← mul_assoc, ← Complex.ofReal_mul,
  Complex.add_re, Complex.ofReal_re, Complex.mul_re, Complex.I_re, Complex.ofReal_im,
  Real.log_neg_eq_log]
no goals
x : ℝ
hx : x < 0
y : ℝ
this : Complex.log ↑x * ↑y = ↑(log (-x) * y) + ↑(y * π) * Complex.I
⊢ exp (log x * y) * cos (y * π) + ((↑(exp (log x * y) * sin (y * π))).re * 0 - 0 * Complex.I.im) =
    exp (log x * y) * cos (y * π)
ring
case hnc
x : ℝ
hx : x < 0
y : ℝ
⊢ ¬x = 0
case hnc
x : ℝ
hx : x < 0
y : ℝ
⊢ ¬↑x = 0
rw [Complex.ofReal_eq_zero]
no goals
case hnc
x : ℝ
hx : x < 0
y : ℝ
⊢ ¬x = 0
exact ne_of_lt hx