no goals
p : ℕ
R : Type u_2
S : Type u_1
T : Type ?u.510348
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type ?u.510363
β : Type ?u.510366
f : R →+* S
x y : 𝕎 R
n : ℕ
⊢ mapFun (↑f) (Nat.unaryCast n) = ↑n
induction n <;> simp [*, Nat.unaryCast, add, one, zero] <;> rfl