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

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