-- Mathlib/RingTheory/WittVector/WittPolynomial.lean
theorem constantCoeff_xInTermsOfW [hp : Fact p.Prime] [Invertible (p : R)] (n : ℕ) :
    constantCoeff (xInTermsOfW p R n) = 0

Proof state:
case ind
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ m < n, constantCoeff (xInTermsOfW p R m) = 0
⊢ ⅟↑p ^ n * ∑ x ∈ range n, constantCoeff (C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x)) = ⅟↑p ^ n * 0

Tactic:
congr 1

Result:
case ind.e_a
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ m < n, constantCoeff (xInTermsOfW p R m) = 0
⊢ ∑ x ∈ range n, constantCoeff (C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x)) = 0

Proof state:
case ind.e_a
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ m < n, constantCoeff (xInTermsOfW p R m) = 0
m : ℕ
H : m < n
⊢ p ^ (n - m) ≠ 0

Tactic:
exact pow_ne_zero _ hp.1.ne_zero

Result:
no goals

Proof state:
case ind.e_a
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ m < n, constantCoeff (xInTermsOfW p R m) = 0
m : ℕ
H : m < n
⊢ constantCoeff (C (↑p ^ m) * xInTermsOfW p R m ^ p ^ (n - m)) = 0

Tactic:
simp only [RingHom.map_mul, RingHom.map_pow, map_natCast, IH m H]

Result:
case ind.e_a
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ m < n, constantCoeff (xInTermsOfW p R m) = 0
m : ℕ
H : m < n
⊢ ↑p ^ m * 0 ^ p ^ (n - m) = 0

Proof state:
case ind.e_a
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ 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

Tactic:
rw [mem_range] at H

Result:
case ind.e_a
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ m < n, constantCoeff (xInTermsOfW p R m) = 0
m : ℕ
H : m < n
⊢ constantCoeff (C (↑p ^ m) * xInTermsOfW p R m ^ p ^ (n - m)) = 0

Proof state:
case ind
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ m < n, constantCoeff (xInTermsOfW p R m) = 0
⊢ constantCoeff (xInTermsOfW p R n) = 0

Tactic:
rw [xInTermsOfW_eq, mul_comm, RingHom.map_mul, RingHom.map_sub, map_sum, constantCoeff_C,
  constantCoeff_X, zero_sub, mul_neg, neg_eq_zero]

Result:
case ind
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ m < n, constantCoeff (xInTermsOfW p R m) = 0
⊢ ⅟↑p ^ n * ∑ x ∈ range n, constantCoeff (C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x)) = 0

Proof state:
case ind.e_a
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ m < n, constantCoeff (xInTermsOfW p R m) = 0
m : ℕ
H : m < n
⊢ ↑p ^ m * 0 ^ p ^ (n - m) = 0

Tactic:
rw [zero_pow, mul_zero]

Result:
case ind.e_a
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ m < n, constantCoeff (xInTermsOfW p R m) = 0
m : ℕ
H : m < n
⊢ p ^ (n - m) ≠ 0

Proof state:
case ind.e_a
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ m < n, constantCoeff (xInTermsOfW p R m) = 0
⊢ ∀ x ∈ range n, constantCoeff (C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x)) = 0

Tactic:
intro m H

Result:
case ind.e_a
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ 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

Proof state:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
⊢ constantCoeff (xInTermsOfW p R n) = 0

Tactic:
induction n using Nat.strongRecOn with | ind n IH => ?_

Result:
case ind
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ m < n, constantCoeff (xInTermsOfW p R m) = 0
⊢ constantCoeff (xInTermsOfW p R n) = 0

Proof state:
case ind.e_a
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ m < n, constantCoeff (xInTermsOfW p R m) = 0
⊢ ∑ x ∈ range n, constantCoeff (C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x)) = 0

Tactic:
rw [sum_eq_zero]

Result:
case ind.e_a
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ m < n, constantCoeff (xInTermsOfW p R m) = 0
⊢ ∀ x ∈ range n, constantCoeff (C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x)) = 0

Proof state:
case ind
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ m < n, constantCoeff (xInTermsOfW p R m) = 0
⊢ ⅟↑p ^ n * ∑ x ∈ range n, constantCoeff (C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x)) = 0

Tactic:
refine Eq.trans (?_ : _ = ((⅟↑p : R) ^ n)* 0) (mul_zero _)

Result:
case ind
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ m < n, constantCoeff (xInTermsOfW p R m) = 0
⊢ ⅟↑p ^ n * ∑ x ∈ range n, constantCoeff (C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x)) = ⅟↑p ^ n * 0