no goals
p : ℕ
R : Type u_1
S : Type ?u.681371
T : Type ?u.681374
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type ?u.681389
β : Type ?u.681392
x y : 𝕎 R
i : ℕ
⊢ WittVector.ghostFun (Nat.unaryCast i) = ↑i
induction i <;>
  simp [*, Nat.unaryCast, ghostFun_zero, ghostFun_one, ghostFun_add, -Pi.coe_nat]