no goals
R : Type u_2
inst✝² : CommRing R
S : Submonoid R
P : Type u_1
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
n : ℕ
⊢ ↑(Nat.unaryCast n) = ↑n
induction n <;> simp [*, Nat.unaryCast]