rw [rpow_def_of_pos h, ofReal_exp, ofReal_mul, Complex.ofReal_log h.le,
  Complex.cpow_def_of_ne_zero]
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x : ℝ
h : x > 0
y : ℝ
⊢ ↑(x ^ y) = ↑x ^ ↑y
case hx
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x : ℝ
h : x > 0
y : ℝ
⊢ ↑x ≠ 0