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
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
apply Nat.strongInductionOn n
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
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
clear n
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
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
intro n IH
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
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
rw [xInTermsOfW_eq, mul_comm, RingHom.map_mul, RingHom.map_sub, map_sum, constantCoeff_C,
  constantCoeff_X, zero_sub, mul_neg, neg_eq_zero]
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
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
refine' Eq.trans (_ : _ = ((⅟↑p : R) ^ n)* 0) (mul_zero _)
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
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
congr 1
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
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
rw [sum_eq_zero]
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
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
intro m H
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
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
rw [mem_range] at H
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
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
simp only [RingHom.map_mul, RingHom.map_pow, map_natCast, IH m H]
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)
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
rw [zero_pow, mul_zero]
no goals
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)
apply pow_pos hp.1.pos