Theorem: Mathlib.Tactic.RPowRing.inv_congr (PrimeNumberTheoremAnd/Tactic/RPowSimp.lean)

State before:
a a' b : ℝ
x✝¹ : a = a'
x✝ : a' ^ (-1) = b
⊢ a⁻¹ = b
Tactic:
subst_vars
State after:
a' : ℝ
⊢ a'⁻¹ = a' ^ (-1)

State before:
a' : ℝ
⊢ a'⁻¹ = a' ^ (-1)
Tactic:
simp [rpow_neg_one]
State after:
no goals