no goals
x✝ y✝ z✝ x : ℝ
hx : 0 ≤ x
y z : ℝ
⊢ x ^ (y * z) = (x ^ y) ^ z
rw [← Complex.ofReal_inj, Complex.ofReal_cpow (rpow_nonneg_of_nonneg hx _),
    Complex.ofReal_cpow hx, Complex.ofReal_mul, Complex.cpow_mul, Complex.ofReal_cpow hx] <;>
  simp only [(Complex.ofReal_mul _ _).symm, (Complex.ofReal_log hx).symm, Complex.ofReal_im,
    neg_lt_zero, pi_pos, le_of_lt pi_pos]