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

State before:
a a' c b : ℝ
x✝¹ : a = a'
x✝ : a' ^ b = c
⊢ a ^ b = c
Tactic:
subst_vars
State after:
a' b : ℝ
⊢ a' ^ b = a' ^ b

State before:
a' b : ℝ
⊢ a' ^ b = a' ^ b
Tactic:
rfl
State after:
no goals