no goals
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type ?u.105241
inst✝ : CommRing S
⊢ W_ R 1 = ↑C ↑p * X 1 + X 0 ^ p
simp only [wittPolynomial_eq_sum_c_mul_x_pow, sum_range_succ_comm, range_one, sum_singleton,
  one_mul, pow_one, C_1, pow_zero, tsub_self, tsub_zero]