Theorem: Real.rpow_inv (PrimeNumberTheoremAnd/Tactic/RPowSimp.lean)

State before:
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ (x ^ y)⁻¹ = x ^ (-y)
Tactic:
simp [← inv_rpow' hx, inv_rpow hx]
State after:
no goals