no goals
p : ℕ
R : Type u_1
S : Type ?u.755378
T : Type ?u.755381
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type ?u.755396
β : Type ?u.755399
x y : 𝕎 R
i : ℤ
⊢ WittVector.ghostFun (Int.castDef i) = ↑i
cases i <;> simp [*, Int.castDef, ghostFun_nat_cast, ghostFun_neg, -Pi.coe_nat, -Pi.coe_int]