Theorem: Complex.one_div_cpow_eq (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
s : ℂ
x : ℝ
x_ne : x ≠ 0
⊢ 1 / ↑x ^ s = ↑x ^ (-s)
Tactic:
refine (eq_one_div_of_mul_eq_one_left ?_).symm
State after:
s : ℂ
x : ℝ
x_ne : x ≠ 0
⊢ ↑x ^ (-s) * ↑x ^ s = 1

State before:
s : ℂ
x : ℝ
x_ne : x ≠ 0
⊢ ↑x ^ (-s) * ↑x ^ s = 1
Tactic:
rw [← cpow_add _ _ <| mod_cast x_ne, add_left_neg, cpow_zero]
State after:
no goals