Theorem: Complex.ofReal_rpow (PrimeNumberTheoremAnd/MellinCalculus.lean)

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

State before:
case hx
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x : ℝ
h : x > 0
y : ℝ
⊢ ↑x ≠ 0
Tactic:
simp only [ne_eq, ofReal_eq_zero, ne_of_gt h, not_false_eq_true]
State after:
no goals