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

State before:
a : ℝ
⊢ a = a ^ 1 * 1
Tactic:
simp
State after:
no goals