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

State before:
a a' : ℝ
p : a = a'
⊢ a = a ^ 1 * 1
Tactic:
simp [*]
State after:
no goals