p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
k : ℕ
⊢ ∑ x in range (k + 1), ↑(bind₁ (xInTermsOfW p R)) (↑C (↑p ^ x) * X x ^ p ^ (k - x)) = X k
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
k : ℕ
⊢ ↑(bind₁ (xInTermsOfW p R)) (W_ R k) = X k
rw [wittPolynomial_eq_sum_c_mul_x_pow, AlgHom.map_sum]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
k : ℕ
⊢ ∑ x in range (k + 1), ↑C ↑p ^ x * ↑(bind₁ (xInTermsOfW p R)) (X x) ^ p ^ (k - x) = X k
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
k : ℕ
⊢ ∑ x in range (k + 1), ↑(bind₁ (xInTermsOfW p R)) (↑C (↑p ^ x) * X x ^ p ^ (k - x)) = X k
simp only [Nat.cast_pow, AlgHom.map_pow, C_pow, AlgHom.map_mul, algHom_C]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
k : ℕ
⊢ X k - ∑ i in range k, ↑C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (k - i) +
      ∑ x in range k, ↑C ↑p ^ x * ↑(bind₁ (xInTermsOfW p R)) (X x) ^ p ^ (k - x) =
    X k
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
k : ℕ
⊢ ∑ x in range (k + 1), ↑C ↑p ^ x * ↑(bind₁ (xInTermsOfW p R)) (X x) ^ p ^ (k - x) = X k
rw [sum_range_succ_comm, tsub_self, pow_zero, pow_one, bind₁_X_right, mul_comm, ← C_pow,
  xInTermsOfW_aux]
no goals
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
k : ℕ
⊢ X k - ∑ i in range k, ↑C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (k - i) +
      ∑ x in range k, ↑C ↑p ^ x * ↑(bind₁ (xInTermsOfW p R)) (X x) ^ p ^ (k - x) =
    X k
simp only [Nat.cast_pow, C_pow, bind₁_X_right, sub_add_cancel]