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

State before:
a a' : ℝ
b : ℕ
c : ℝ
x✝¹ : a = a'
x✝ : a' ^ ↑b = c
⊢ Monoid.npow b a = c
Tactic:
subst_vars
State after:
a' : ℝ
b : ℕ
⊢ Monoid.npow b a' = a' ^ ↑b