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

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