p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
n : ℕ
⊢ ∀ (n : ℕ), (∀ (m : ℕ), m < n → ↑(bind₁ (W_ R)) (xInTermsOfW p R m) = X m) → ↑(bind₁ (W_ R)) (xInTermsOfW p R n) = X n
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
n : ℕ
⊢ ↑(bind₁ (W_ R)) (xInTermsOfW p R n) = X n
apply Nat.strongInductionOn n
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
⊢ ∀ (n : ℕ), (∀ (m : ℕ), m < n → ↑(bind₁ (W_ R)) (xInTermsOfW p R m) = X m) → ↑(bind₁ (W_ R)) (xInTermsOfW p R n) = X n
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
n : ℕ
⊢ ∀ (n : ℕ), (∀ (m : ℕ), m < n → ↑(bind₁ (W_ R)) (xInTermsOfW p R m) = X m) → ↑(bind₁ (W_ R)) (xInTermsOfW p R n) = X n
clear n
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ (m : ℕ), m < n → ↑(bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ ↑(bind₁ (W_ R)) (xInTermsOfW p R n) = X n
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
⊢ ∀ (n : ℕ), (∀ (m : ℕ), m < n → ↑(bind₁ (W_ R)) (xInTermsOfW p R m) = X m) → ↑(bind₁ (W_ R)) (xInTermsOfW p R n) = X n
intro n H
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ (m : ℕ), m < n → ↑(bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ (W_ R n - ∑ x in range n, ↑(bind₁ (W_ R)) (↑C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x))) * ↑C (⅟↑p ^ n) =
    X n * ↑C (↑p ^ n) * ↑C (⅟↑p ^ n)
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ (m : ℕ), m < n → ↑(bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ ↑(bind₁ (W_ R)) (xInTermsOfW p R n) = X n
rw [xInTermsOfW_eq, AlgHom.map_mul, AlgHom.map_sub, bind₁_X_right, algHom_C, AlgHom.map_sum,
  show X n = (X n * C ((p : R) ^ n)) * C ((⅟p : R) ^ n) by
    rw [mul_assoc, ← C_mul, ← mul_pow, mul_invOf_self, one_pow, map_one, mul_one]]
case e_a
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ (m : ℕ), m < n → ↑(bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ W_ R n - ∑ x in range n, ↑(bind₁ (W_ R)) (↑C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x)) = X n * ↑C (↑p ^ n)
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ (m : ℕ), m < n → ↑(bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ (W_ R n - ∑ x in range n, ↑(bind₁ (W_ R)) (↑C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x))) * ↑C (⅟↑p ^ n) =
    X n * ↑C (↑p ^ n) * ↑C (⅟↑p ^ n)
congr 1
case e_a
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ (m : ℕ), m < n → ↑(bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ ∑ x in range n, ↑C (↑p ^ x) * X x ^ p ^ (n - x) =
    ∑ x in range n, ↑(bind₁ (W_ R)) (↑C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x))
case e_a
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ (m : ℕ), m < n → ↑(bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ W_ R n - ∑ x in range n, ↑(bind₁ (W_ R)) (↑C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x)) = X n * ↑C (↑p ^ n)
rw [wittPolynomial_eq_sum_c_mul_x_pow, sum_range_succ_comm,
  tsub_self, pow_zero, pow_one, mul_comm (X n), add_sub_assoc, add_right_eq_self, sub_eq_zero]
case e_a
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ (m : ℕ), m < n → ↑(bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ ∀ (x : ℕ),
    x ∈ range n → ↑C (↑p ^ x) * X x ^ p ^ (n - x) = ↑(bind₁ (W_ R)) (↑C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x))
case e_a
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ (m : ℕ), m < n → ↑(bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ ∑ x in range n, ↑C (↑p ^ x) * X x ^ p ^ (n - x) =
    ∑ x in range n, ↑(bind₁ (W_ R)) (↑C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x))
apply sum_congr rfl
case e_a
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ (m : ℕ), m < n → ↑(bind₁ (W_ R)) (xInTermsOfW p R m) = X m
i : ℕ
h : i ∈ range n
⊢ ↑C (↑p ^ i) * X i ^ p ^ (n - i) = ↑(bind₁ (W_ R)) (↑C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i))
case e_a
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ (m : ℕ), m < n → ↑(bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ ∀ (x : ℕ),
    x ∈ range n → ↑C (↑p ^ x) * X x ^ p ^ (n - x) = ↑(bind₁ (W_ R)) (↑C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x))
intro i h
case e_a
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ (m : ℕ), m < n → ↑(bind₁ (W_ R)) (xInTermsOfW p R m) = X m
i : ℕ
h : i < n
⊢ ↑C (↑p ^ i) * X i ^ p ^ (n - i) = ↑(bind₁ (W_ R)) (↑C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i))
case e_a
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ (m : ℕ), m < n → ↑(bind₁ (W_ R)) (xInTermsOfW p R m) = X m
i : ℕ
h : i ∈ range n
⊢ ↑C (↑p ^ i) * X i ^ p ^ (n - i) = ↑(bind₁ (W_ R)) (↑C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i))
rw [mem_range] at h
no goals
case e_a
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ (m : ℕ), m < n → ↑(bind₁ (W_ R)) (xInTermsOfW p R m) = X m
i : ℕ
h : i < n
⊢ ↑C (↑p ^ i) * X i ^ p ^ (n - i) = ↑(bind₁ (W_ R)) (↑C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i))
rw [AlgHom.map_mul, AlgHom.map_pow, algHom_C, H i h]
no goals
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ (m : ℕ), m < n → ↑(bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ X n = X n * ↑C (↑p ^ n) * ↑C (⅟↑p ^ n)
rw [mul_assoc, ← C_mul, ← mul_pow, mul_invOf_self, one_pow, map_one, mul_one]