no goals
p : ℕ
R : Type u_2
S : Type u_1
T : Type ?u.559389
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type ?u.559404
β : Type ?u.559407
f : R →+* S
x y : 𝕎 R
n : ℤ
⊢ mapFun (↑f) (Int.castDef n) = ↑n
cases n <;> simp [*, Int.castDef, add, one, neg, zero, nat_cast] <;> rfl