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

State before:
n : ℕ
inst✝ : n.AtLeastTwo
⊢ ↑n = OfNat.ofNat n
Tactic:
rfl
State after:
no goals