no goals
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type ?u.103907
inst✝ : CommRing S
⊢ W_ R 0 = X 0
simp only [wittPolynomial, X, sum_singleton, range_one, pow_zero, zero_add, tsub_self]