p : ℕ
R : Type ?u.148919
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type ?u.148934
inst✝ : CommRing S
n : ℕ
⊢ ∑ x in range (n + 1 + 1), ↑C (↑p ^ x) * X x ^ p ^ (n + 1 - x) =
    ↑(expand p) (∑ x in range (n + 1), ↑C (↑p ^ x) * X x ^ p ^ (n - x))
p : ℕ
R : Type ?u.148919
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type ?u.148934
inst✝ : CommRing S
n : ℕ
⊢ W_ (ZMod (p ^ (n + 1))) (n + 1) = ↑(expand p) (W_ (ZMod (p ^ (n + 1))) n)
simp only [wittPolynomial_eq_sum_c_mul_x_pow]
p : ℕ
R : Type ?u.148919
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type ?u.148934
inst✝ : CommRing S
n : ℕ
⊢ ∀ (x : ℕ), x ∈ range (n + 1) → ↑C (↑p ^ x) * X x ^ p ^ (n + 1 - x) = ↑(expand p) (↑C (↑p ^ x) * X x ^ p ^ (n - x))
p : ℕ
R : Type ?u.148919
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type ?u.148934
inst✝ : CommRing S
n : ℕ
⊢ ∑ x in range (n + 1 + 1), ↑C (↑p ^ x) * X x ^ p ^ (n + 1 - x) =
    ↑(expand p) (∑ x in range (n + 1), ↑C (↑p ^ x) * X x ^ p ^ (n - x))
rw [sum_range_succ, ← Nat.cast_pow, CharP.cast_eq_zero (ZMod (p ^ (n + 1))) (p ^ (n + 1)), C_0,
  MulZeroClass.zero_mul, add_zero, AlgHom.map_sum, sum_congr rfl]
p : ℕ
R : Type ?u.148919
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type ?u.148934
inst✝ : CommRing S
n k : ℕ
hk : k ∈ range (n + 1)
⊢ ↑C (↑p ^ k) * X k ^ p ^ (n + 1 - k) = ↑(expand p) (↑C (↑p ^ k) * X k ^ p ^ (n - k))
p : ℕ
R : Type ?u.148919
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type ?u.148934
inst✝ : CommRing S
n : ℕ
⊢ ∀ (x : ℕ), x ∈ range (n + 1) → ↑C (↑p ^ x) * X x ^ p ^ (n + 1 - x) = ↑(expand p) (↑C (↑p ^ x) * X x ^ p ^ (n - x))
intro k hk
p : ℕ
R : Type ?u.148919
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type ?u.148934
inst✝ : CommRing S
n k : ℕ
hk : k ∈ range (n + 1)
⊢ ↑C (↑p ^ k) * X k ^ p ^ (n + 1 - k) = ↑C (↑p ^ k) * X k ^ p ^ (n - k + 1)
p : ℕ
R : Type ?u.148919
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type ?u.148934
inst✝ : CommRing S
n k : ℕ
hk : k ∈ range (n + 1)
⊢ ↑C (↑p ^ k) * X k ^ p ^ (n + 1 - k) = ↑(expand p) (↑C (↑p ^ k) * X k ^ p ^ (n - k))
rw [AlgHom.map_mul, AlgHom.map_pow, expand_X, algHom_C, ← pow_mul, ← pow_succ]
case e_a.e_a.e_a
p : ℕ
R : Type ?u.148919
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type ?u.148934
inst✝ : CommRing S
n k : ℕ
hk : k ∈ range (n + 1)
⊢ n + 1 - k = n - k + 1
p : ℕ
R : Type ?u.148919
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type ?u.148934
inst✝ : CommRing S
n k : ℕ
hk : k ∈ range (n + 1)
⊢ ↑C (↑p ^ k) * X k ^ p ^ (n + 1 - k) = ↑C (↑p ^ k) * X k ^ p ^ (n - k + 1)
congr
case e_a.e_a.e_a
p : ℕ
R : Type ?u.148919
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type ?u.148934
inst✝ : CommRing S
n k : ℕ
hk : k < n + 1
⊢ n + 1 - k = n - k + 1
case e_a.e_a.e_a
p : ℕ
R : Type ?u.148919
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type ?u.148934
inst✝ : CommRing S
n k : ℕ
hk : k ∈ range (n + 1)
⊢ n + 1 - k = n - k + 1
rw [mem_range] at hk
no goals
case e_a.e_a.e_a
p : ℕ
R : Type ?u.148919
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type ?u.148934
inst✝ : CommRing S
n k : ℕ
hk : k < n + 1
⊢ n + 1 - k = n - k + 1
rw [add_comm, add_tsub_assoc_of_le (Nat.lt_succ_iff.mp hk), ← add_comm]