[GOAL]
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
n : ℕ
⊢ wittPolynomial p R n = ∑ i in range (n + 1), ↑C (↑p ^ i) * X i ^ p ^ (n - i)
[PROOFSTEP]
apply sum_congr rfl
[GOAL]
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
n : ℕ
⊢ ∀ (x : ℕ), x ∈ range (n + 1) → ↑(monomial (single x (p ^ (n - x)))) (↑p ^ x) = ↑C (↑p ^ x) * X x ^ p ^ (n - x)
[PROOFSTEP]
rintro i -
[GOAL]
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
n i : ℕ
⊢ ↑(monomial (single i (p ^ (n - i)))) (↑p ^ i) = ↑C (↑p ^ i) * X i ^ p ^ (n - i)
[PROOFSTEP]
rw [monomial_eq, Finsupp.prod_single_index]
[GOAL]
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
n i : ℕ
⊢ X i ^ 0 = 1
[PROOFSTEP]
rw [pow_zero]
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
n : ℕ
⊢ ↑(map f) (W_ R n) = W_ S n
[PROOFSTEP]
rw [wittPolynomial, map_sum, wittPolynomial]
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
n : ℕ
⊢ ∑ x in range (n + 1), ↑(map f) (↑(monomial (single x (p ^ (n - x)))) (↑p ^ x)) =
    ∑ i in range (n + 1), ↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)
[PROOFSTEP]
refine sum_congr rfl fun i _ => ?_
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
n i : ℕ
x✝ : i ∈ range (n + 1)
⊢ ↑(map f) (↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)) = ↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)
[PROOFSTEP]
rw [map_monomial, RingHom.map_pow, map_natCast]
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ↑constantCoeff (W_ R n) = 0
[PROOFSTEP]
simp only [wittPolynomial, map_sum, constantCoeff_monomial]
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (∑ x in range (n + 1), if single x (p ^ (n - x)) = 0 then ↑p ^ x else 0) = 0
[PROOFSTEP]
rw [sum_eq_zero]
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ (x : ℕ), x ∈ range (n + 1) → (if single x (p ^ (n - x)) = 0 then ↑p ^ x else 0) = 0
[PROOFSTEP]
rintro i _
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n i : ℕ
a✝ : i ∈ range (n + 1)
⊢ (if single i (p ^ (n - i)) = 0 then ↑p ^ i else 0) = 0
[PROOFSTEP]
rw [if_neg]
[GOAL]
case hnc
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n i : ℕ
a✝ : i ∈ range (n + 1)
⊢ ¬single i (p ^ (n - i)) = 0
[PROOFSTEP]
rw [Finsupp.single_eq_zero]
[GOAL]
case hnc
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n i : ℕ
a✝ : i ∈ range (n + 1)
⊢ ¬p ^ (n - i) = 0
[PROOFSTEP]
exact ne_of_gt (pow_pos hp.1.pos _)
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
inst✝ : CommRing S
⊢ W_ R 0 = X 0
[PROOFSTEP]
simp only [wittPolynomial, X, sum_singleton, range_one, pow_zero, zero_add, tsub_self]
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
inst✝ : CommRing S
⊢ W_ R 1 = ↑C ↑p * X 1 + X 0 ^ p
[PROOFSTEP]
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]
[GOAL]
p : ℕ
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : DecidableEq R
S : Type u_2
inst✝² : CommRing S
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ℕ → A
n : ℕ
⊢ ↑(aeval f) (W_ R n) = ∑ i in range (n + 1), ↑p ^ i * f i ^ p ^ (n - i)
[PROOFSTEP]
simp [wittPolynomial, AlgHom.map_sum, aeval_monomial, Finsupp.prod_single_index]
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
inst✝ : CommRing S
n : ℕ
⊢ W_ (ZMod (p ^ (n + 1))) (n + 1) = ↑(expand p) (W_ (ZMod (p ^ (n + 1))) n)
[PROOFSTEP]
simp only [wittPolynomial_eq_sum_C_mul_X_pow]
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
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))
[PROOFSTEP]
rw [sum_range_succ, ← Nat.cast_pow, CharP.cast_eq_zero (ZMod (p ^ (n + 1))) (p ^ (n + 1)), C_0, zero_mul, add_zero,
  AlgHom.map_sum, sum_congr rfl]
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
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))
[PROOFSTEP]
intro k hk
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
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))
[PROOFSTEP]
rw [AlgHom.map_mul, AlgHom.map_pow, expand_X, algHom_C, ← pow_mul, ← pow_succ]
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
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)
[PROOFSTEP]
congr
[GOAL]
case e_a.e_a.e_a
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
inst✝ : CommRing S
n k : ℕ
hk : k ∈ range (n + 1)
⊢ n + 1 - k = n - k + 1
[PROOFSTEP]
rw [mem_range] at hk 
[GOAL]
case e_a.e_a.e_a
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
inst✝ : CommRing S
n k : ℕ
hk : k < n + 1
⊢ n + 1 - k = n - k + 1
[PROOFSTEP]
rw [add_comm, add_tsub_assoc_of_le (Nat.lt_succ_iff.mp hk), ← add_comm]
[GOAL]
p : ℕ
R : Type u_1
inst✝³ : CommRing R
inst✝² : DecidableEq R
S : Type u_2
inst✝¹ : CommRing S
hp : NeZero p
inst✝ : CharZero R
n : ℕ
⊢ vars (W_ R n) = range (n + 1)
[PROOFSTEP]
have : ∀ i, (monomial (Finsupp.single i (p ^ (n - i))) ((p : R) ^ i)).vars = { i } :=
  by
  intro i
  refine' vars_monomial_single i (pow_ne_zero _ hp.1) _
  rw [← Nat.cast_pow, Nat.cast_ne_zero]
  exact pow_ne_zero i hp.1
[GOAL]
p : ℕ
R : Type u_1
inst✝³ : CommRing R
inst✝² : DecidableEq R
S : Type u_2
inst✝¹ : CommRing S
hp : NeZero p
inst✝ : CharZero R
n : ℕ
⊢ ∀ (i : ℕ), vars (↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)) = {i}
[PROOFSTEP]
intro i
[GOAL]
p : ℕ
R : Type u_1
inst✝³ : CommRing R
inst✝² : DecidableEq R
S : Type u_2
inst✝¹ : CommRing S
hp : NeZero p
inst✝ : CharZero R
n i : ℕ
⊢ vars (↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)) = {i}
[PROOFSTEP]
refine' vars_monomial_single i (pow_ne_zero _ hp.1) _
[GOAL]
p : ℕ
R : Type u_1
inst✝³ : CommRing R
inst✝² : DecidableEq R
S : Type u_2
inst✝¹ : CommRing S
hp : NeZero p
inst✝ : CharZero R
n i : ℕ
⊢ ↑p ^ i ≠ 0
[PROOFSTEP]
rw [← Nat.cast_pow, Nat.cast_ne_zero]
[GOAL]
p : ℕ
R : Type u_1
inst✝³ : CommRing R
inst✝² : DecidableEq R
S : Type u_2
inst✝¹ : CommRing S
hp : NeZero p
inst✝ : CharZero R
n i : ℕ
⊢ p ^ i ≠ 0
[PROOFSTEP]
exact pow_ne_zero i hp.1
[GOAL]
p : ℕ
R : Type u_1
inst✝³ : CommRing R
inst✝² : DecidableEq R
S : Type u_2
inst✝¹ : CommRing S
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), vars (↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)) = {i}
⊢ vars (W_ R n) = range (n + 1)
[PROOFSTEP]
rw [wittPolynomial, vars_sum_of_disjoint]
[GOAL]
p : ℕ
R : Type u_1
inst✝³ : CommRing R
inst✝² : DecidableEq R
S : Type u_2
inst✝¹ : CommRing S
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), vars (↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)) = {i}
⊢ (Finset.biUnion (range (n + 1)) fun i => vars (↑(monomial (single i (p ^ (n - i)))) (↑p ^ i))) = range (n + 1)
[PROOFSTEP]
simp only [this, biUnion_singleton_eq_self]
[GOAL]
case h
p : ℕ
R : Type u_1
inst✝³ : CommRing R
inst✝² : DecidableEq R
S : Type u_2
inst✝¹ : CommRing S
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), vars (↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)) = {i}
⊢ Pairwise (Disjoint on fun i => vars (↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)))
[PROOFSTEP]
simp only [this]
[GOAL]
case h
p : ℕ
R : Type u_1
inst✝³ : CommRing R
inst✝² : DecidableEq R
S : Type u_2
inst✝¹ : CommRing S
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), vars (↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)) = {i}
⊢ Pairwise (Disjoint on fun i => {i})
[PROOFSTEP]
intro a b h
[GOAL]
case h
p : ℕ
R : Type u_1
inst✝³ : CommRing R
inst✝² : DecidableEq R
S : Type u_2
inst✝¹ : CommRing S
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), vars (↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)) = {i}
a b : ℕ
h : a ≠ b
⊢ (Disjoint on fun i => {i}) a b
[PROOFSTEP]
apply disjoint_singleton_left.mpr
[GOAL]
case h
p : ℕ
R : Type u_1
inst✝³ : CommRing R
inst✝² : DecidableEq R
S : Type u_2
inst✝¹ : CommRing S
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), vars (↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)) = {i}
a b : ℕ
h : a ≠ b
⊢ ¬a ∈ (fun i => {i}) b
[PROOFSTEP]
rwa [mem_singleton]
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
inst✝ : CommRing S
hp : NeZero p
n : ℕ
⊢ vars (W_ R n) ⊆ range (n + 1)
[PROOFSTEP]
rw [← map_wittPolynomial p (Int.castRingHom R), ← wittPolynomial_vars p ℤ]
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
inst✝ : CommRing S
hp : NeZero p
n : ℕ
⊢ vars (↑(map (Int.castRingHom R)) (W_ ℤ n)) ⊆ vars (W_ ℤ n)
[PROOFSTEP]
apply vars_map
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
n : ℕ
⊢ xInTermsOfW p R n = (X n - ∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i)) * ↑C (⅟↑p ^ n)
[PROOFSTEP]
rw [xInTermsOfW, ← Fin.sum_univ_eq_sum_range]
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
⊢ ↑constantCoeff (xInTermsOfW p R n) = 0
[PROOFSTEP]
apply Nat.strongInductionOn n
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
⊢ ∀ (n : ℕ), (∀ (m : ℕ), m < n → ↑constantCoeff (xInTermsOfW p R m) = 0) → ↑constantCoeff (xInTermsOfW p R n) = 0
[PROOFSTEP]
clear n
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
⊢ ∀ (n : ℕ), (∀ (m : ℕ), m < n → ↑constantCoeff (xInTermsOfW p R m) = 0) → ↑constantCoeff (xInTermsOfW p R n) = 0
[PROOFSTEP]
intro n IH
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ (m : ℕ), m < n → ↑constantCoeff (xInTermsOfW p R m) = 0
⊢ ↑constantCoeff (xInTermsOfW p R n) = 0
[PROOFSTEP]
rw [xInTermsOfW_eq, mul_comm, RingHom.map_mul, RingHom.map_sub, map_sum, constantCoeff_C, constantCoeff_X, zero_sub,
  mul_neg, neg_eq_zero]
  -- porting note: here, we should be able to do `rw [sum_eq_zero]`, but the goal that
    -- is created is not what we expect, and the sum is not replaced by zero...
    -- is it a bug in `rw` tactic?
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ (m : ℕ), m < n → ↑constantCoeff (xInTermsOfW p R m) = 0
⊢ ⅟↑p ^ n * ∑ x in range n, ↑constantCoeff (↑C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x)) = 0
[PROOFSTEP]
refine' Eq.trans (_ : _ = ((⅟↑p : R) ^ n) * 0) (mul_zero _)
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ (m : ℕ), m < n → ↑constantCoeff (xInTermsOfW p R m) = 0
⊢ ⅟↑p ^ n * ∑ x in range n, ↑constantCoeff (↑C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x)) = ⅟↑p ^ n * 0
[PROOFSTEP]
congr 1
[GOAL]
case e_a
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ (m : ℕ), m < n → ↑constantCoeff (xInTermsOfW p R m) = 0
⊢ ∑ x in range n, ↑constantCoeff (↑C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x)) = 0
[PROOFSTEP]
rw [sum_eq_zero]
[GOAL]
case e_a
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ (m : ℕ), m < n → ↑constantCoeff (xInTermsOfW p R m) = 0
⊢ ∀ (x : ℕ), x ∈ range n → ↑constantCoeff (↑C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x)) = 0
[PROOFSTEP]
intro m H
[GOAL]
case e_a
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ (m : ℕ), m < n → ↑constantCoeff (xInTermsOfW p R m) = 0
m : ℕ
H : m ∈ range n
⊢ ↑constantCoeff (↑C (↑p ^ m) * xInTermsOfW p R m ^ p ^ (n - m)) = 0
[PROOFSTEP]
rw [mem_range] at H 
[GOAL]
case e_a
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ (m : ℕ), m < n → ↑constantCoeff (xInTermsOfW p R m) = 0
m : ℕ
H : m < n
⊢ ↑constantCoeff (↑C (↑p ^ m) * xInTermsOfW p R m ^ p ^ (n - m)) = 0
[PROOFSTEP]
simp only [RingHom.map_mul, RingHom.map_pow, map_natCast, IH m H]
[GOAL]
case e_a
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ (m : ℕ), m < n → ↑constantCoeff (xInTermsOfW p R m) = 0
m : ℕ
H : m < n
⊢ ↑p ^ m * 0 ^ p ^ (n - m) = 0
[PROOFSTEP]
rw [zero_pow, mul_zero]
[GOAL]
case e_a
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ (m : ℕ), m < n → ↑constantCoeff (xInTermsOfW p R m) = 0
m : ℕ
H : m < n
⊢ 0 < p ^ (n - m)
[PROOFSTEP]
apply pow_pos hp.1.pos
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
⊢ xInTermsOfW p R 0 = X 0
[PROOFSTEP]
rw [xInTermsOfW_eq, range_zero, sum_empty, pow_zero, C_1, mul_one, sub_zero]
[GOAL]
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
⊢ n ∈ vars (xInTermsOfW p ℚ n) ∧ vars (xInTermsOfW p ℚ n) ⊆ range (n + 1)
[PROOFSTEP]
apply Nat.strongInductionOn n
[GOAL]
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ (n : ℕ),
    (∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)) →
      n ∈ vars (xInTermsOfW p ℚ n) ∧ vars (xInTermsOfW p ℚ n) ⊆ range (n + 1)
[PROOFSTEP]
clear n
[GOAL]
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
⊢ ∀ (n : ℕ),
    (∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)) →
      n ∈ vars (xInTermsOfW p ℚ n) ∧ vars (xInTermsOfW p ℚ n) ⊆ range (n + 1)
[PROOFSTEP]
intro n ih
[GOAL]
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ n ∈ vars (xInTermsOfW p ℚ n) ∧ vars (xInTermsOfW p ℚ n) ⊆ range (n + 1)
[PROOFSTEP]
rw [xInTermsOfW_eq, mul_comm, vars_C_mul _ (nonzero_of_invertible _), vars_sub_of_disjoint, vars_X, range_succ,
  insert_eq]
[GOAL]
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ n ∈ {n} ∪ vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) ∧
    {n} ∪ vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) ⊆ {n} ∪ range n
case hpq
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ Disjoint (vars (X n)) (vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)))
[PROOFSTEP]
on_goal 1 =>
  simp only [true_and_iff, true_or_iff, eq_self_iff_true, mem_union, mem_singleton]
  intro i
  rw [mem_union, mem_union]
  apply Or.imp id
[GOAL]
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ n ∈ {n} ∪ vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) ∧
    {n} ∪ vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) ⊆ {n} ∪ range n
case hpq
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ Disjoint (vars (X n)) (vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)))
[PROOFSTEP]
on_goal 1 =>
  simp only [true_and_iff, true_or_iff, eq_self_iff_true, mem_union, mem_singleton]
  intro i
  rw [mem_union, mem_union]
  apply Or.imp id
[GOAL]
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ n ∈ {n} ∪ vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) ∧
    {n} ∪ vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) ⊆ {n} ∪ range n
[PROOFSTEP]
simp only [true_and_iff, true_or_iff, eq_self_iff_true, mem_union, mem_singleton]
[GOAL]
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ {n} ∪ vars (∑ x in range n, ↑C (↑p ^ x) * xInTermsOfW p ℚ x ^ p ^ (n - x)) ⊆ {n} ∪ range n
[PROOFSTEP]
intro i
[GOAL]
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i : ℕ
⊢ i ∈ {n} ∪ vars (∑ x in range n, ↑C (↑p ^ x) * xInTermsOfW p ℚ x ^ p ^ (n - x)) → i ∈ {n} ∪ range n
[PROOFSTEP]
rw [mem_union, mem_union]
[GOAL]
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i : ℕ
⊢ i ∈ {n} ∨ i ∈ vars (∑ x in range n, ↑C (↑p ^ x) * xInTermsOfW p ℚ x ^ p ^ (n - x)) → i ∈ {n} ∨ i ∈ range n
[PROOFSTEP]
apply Or.imp id
[GOAL]
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i : ℕ
⊢ i ∈ vars (∑ x in range n, ↑C (↑p ^ x) * xInTermsOfW p ℚ x ^ p ^ (n - x)) → i ∈ range n
case hpq
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ Disjoint (vars (X n)) (vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)))
[PROOFSTEP]
on_goal 2 => rw [vars_X, disjoint_singleton_left]
[GOAL]
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i : ℕ
⊢ i ∈ vars (∑ x in range n, ↑C (↑p ^ x) * xInTermsOfW p ℚ x ^ p ^ (n - x)) → i ∈ range n
case hpq
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ Disjoint (vars (X n)) (vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)))
[PROOFSTEP]
on_goal 2 => rw [vars_X, disjoint_singleton_left]
[GOAL]
case hpq
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ Disjoint (vars (X n)) (vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)))
[PROOFSTEP]
rw [vars_X, disjoint_singleton_left]
[GOAL]
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i : ℕ
⊢ i ∈ vars (∑ x in range n, ↑C (↑p ^ x) * xInTermsOfW p ℚ x ^ p ^ (n - x)) → i ∈ range n
case hpq
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ ¬n ∈ vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))
[PROOFSTEP]
all_goals
  intro H
  replace H := vars_sum_subset _ _ H
  rw [mem_biUnion] at H 
  rcases H with ⟨j, hj, H⟩
  rw [vars_C_mul] at H 
  swap
  · apply pow_ne_zero
    exact_mod_cast hp.1.ne_zero
  rw [mem_range] at hj 
  replace H := (ih j hj).2 (vars_pow _ _ H)
  rw [mem_range] at H 
[GOAL]
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i : ℕ
⊢ i ∈ vars (∑ x in range n, ↑C (↑p ^ x) * xInTermsOfW p ℚ x ^ p ^ (n - x)) → i ∈ range n
[PROOFSTEP]
intro H
[GOAL]
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i : ℕ
H : i ∈ vars (∑ x in range n, ↑C (↑p ^ x) * xInTermsOfW p ℚ x ^ p ^ (n - x))
⊢ i ∈ range n
[PROOFSTEP]
replace H := vars_sum_subset _ _ H
[GOAL]
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i : ℕ
H : i ∈ Finset.biUnion (range n) fun i => vars (↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))
⊢ i ∈ range n
[PROOFSTEP]
rw [mem_biUnion] at H 
[GOAL]
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i : ℕ
H : ∃ a, a ∈ range n ∧ i ∈ vars (↑C (↑p ^ a) * xInTermsOfW p ℚ a ^ p ^ (n - a))
⊢ i ∈ range n
[PROOFSTEP]
rcases H with ⟨j, hj, H⟩
[GOAL]
case intro.intro
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i j : ℕ
hj : j ∈ range n
H : i ∈ vars (↑C (↑p ^ j) * xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ i ∈ range n
[PROOFSTEP]
rw [vars_C_mul] at H 
[GOAL]
case intro.intro
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i j : ℕ
hj : j ∈ range n
H : i ∈ vars (xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ i ∈ range n
case intro.intro.ha
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i j : ℕ
hj : j ∈ range n
H : i ∈ vars (↑C (↑p ^ j) * xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ ↑p ^ j ≠ 0
[PROOFSTEP]
swap
[GOAL]
case intro.intro.ha
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i j : ℕ
hj : j ∈ range n
H : i ∈ vars (↑C (↑p ^ j) * xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ ↑p ^ j ≠ 0
[PROOFSTEP]
apply pow_ne_zero
[GOAL]
case intro.intro.ha.h
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i j : ℕ
hj : j ∈ range n
H : i ∈ vars (↑C (↑p ^ j) * xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ ↑p ≠ 0
[PROOFSTEP]
exact_mod_cast hp.1.ne_zero
[GOAL]
case intro.intro
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i j : ℕ
hj : j ∈ range n
H : i ∈ vars (xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ i ∈ range n
[PROOFSTEP]
rw [mem_range] at hj 
[GOAL]
case intro.intro
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i j : ℕ
hj : j < n
H : i ∈ vars (xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ i ∈ range n
[PROOFSTEP]
replace H := (ih j hj).2 (vars_pow _ _ H)
[GOAL]
case intro.intro
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i j : ℕ
hj : j < n
H : i ∈ range (j + 1)
⊢ i ∈ range n
[PROOFSTEP]
rw [mem_range] at H 
[GOAL]
case hpq
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ ¬n ∈ vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))
[PROOFSTEP]
intro H
[GOAL]
case hpq
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
H : n ∈ vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))
⊢ False
[PROOFSTEP]
replace H := vars_sum_subset _ _ H
[GOAL]
case hpq
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
H : n ∈ Finset.biUnion (range n) fun i => vars (↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))
⊢ False
[PROOFSTEP]
rw [mem_biUnion] at H 
[GOAL]
case hpq
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
H : ∃ a, a ∈ range n ∧ n ∈ vars (↑C (↑p ^ a) * xInTermsOfW p ℚ a ^ p ^ (n - a))
⊢ False
[PROOFSTEP]
rcases H with ⟨j, hj, H⟩
[GOAL]
case hpq.intro.intro
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H : n ∈ vars (↑C (↑p ^ j) * xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ False
[PROOFSTEP]
rw [vars_C_mul] at H 
[GOAL]
case hpq.intro.intro
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H : n ∈ vars (xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ False
case hpq.intro.intro.ha
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H : n ∈ vars (↑C (↑p ^ j) * xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ ↑p ^ j ≠ 0
[PROOFSTEP]
swap
[GOAL]
case hpq.intro.intro.ha
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H : n ∈ vars (↑C (↑p ^ j) * xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ ↑p ^ j ≠ 0
[PROOFSTEP]
apply pow_ne_zero
[GOAL]
case hpq.intro.intro.ha.h
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H : n ∈ vars (↑C (↑p ^ j) * xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ ↑p ≠ 0
[PROOFSTEP]
exact_mod_cast hp.1.ne_zero
[GOAL]
case hpq.intro.intro
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H : n ∈ vars (xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ False
[PROOFSTEP]
rw [mem_range] at hj 
[GOAL]
case hpq.intro.intro
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j < n
H : n ∈ vars (xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ False
[PROOFSTEP]
replace H := (ih j hj).2 (vars_pow _ _ H)
[GOAL]
case hpq.intro.intro
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j < n
H : n ∈ range (j + 1)
⊢ False
[PROOFSTEP]
rw [mem_range] at H 
[GOAL]
case intro.intro
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i j : ℕ
hj : j < n
H : i < j + 1
⊢ i ∈ range n
[PROOFSTEP]
rw [mem_range]
[GOAL]
case intro.intro
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i j : ℕ
hj : j < n
H : i < j + 1
⊢ i < n
[PROOFSTEP]
linarith
[GOAL]
case hpq.intro.intro
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j < n
H : n < j + 1
⊢ False
[PROOFSTEP]
linarith
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
n : ℕ
⊢ xInTermsOfW p R n * ↑C (↑p ^ n) = X n - ∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i)
[PROOFSTEP]
rw [xInTermsOfW_eq, mul_assoc, ← C_mul, ← mul_pow, invOf_mul_self, one_pow, C_1, mul_one]
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
k : ℕ
⊢ ↑(bind₁ (xInTermsOfW p R)) (W_ R k) = X k
[PROOFSTEP]
rw [wittPolynomial_eq_sum_C_mul_X_pow, AlgHom.map_sum]
[GOAL]
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
[PROOFSTEP]
simp only [Nat.cast_pow, AlgHom.map_pow, C_pow, AlgHom.map_mul, algHom_C]
[GOAL]
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
[PROOFSTEP]
rw [sum_range_succ_comm, tsub_self, pow_zero, pow_one, bind₁_X_right, mul_comm, ← C_pow, xInTermsOfW_aux]
[GOAL]
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
[PROOFSTEP]
simp only [Nat.cast_pow, C_pow, bind₁_X_right, sub_add_cancel]
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
n : ℕ
⊢ ↑(bind₁ (W_ R)) (xInTermsOfW p R n) = X n
[PROOFSTEP]
apply Nat.strongInductionOn n
[GOAL]
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
[PROOFSTEP]
clear n
[GOAL]
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
[PROOFSTEP]
intro n H
[GOAL]
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
[PROOFSTEP]
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]]
[GOAL]
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)
[PROOFSTEP]
rw [mul_assoc, ← C_mul, ← mul_pow, mul_invOf_self, one_pow, map_one, mul_one]
[GOAL]
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)
[PROOFSTEP]
congr 1
[GOAL]
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)
[PROOFSTEP]
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]
[GOAL]
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))
[PROOFSTEP]
apply sum_congr rfl
[GOAL]
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))
[PROOFSTEP]
intro i h
[GOAL]
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))
[PROOFSTEP]
rw [mem_range] at h 
[GOAL]
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))
[PROOFSTEP]
rw [AlgHom.map_mul, AlgHom.map_pow, algHom_C, H i h]
