-- Mathlib/RingTheory/WittVector/WittPolynomial.lean
theorem wittPolynomial_vars [CharZero R] (n : ℕ) : (wittPolynomial p R n).vars = range (n + 1)

Proof state:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : NeZero p
inst✝ : CharZero R
n i : ℕ
⊢ ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars = {i}

Tactic:
refine vars_monomial_single i (pow_ne_zero _ hp.1) ?_

Result:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : NeZero p
inst✝ : CharZero R
n i : ℕ
⊢ ↑p ^ i ≠ 0

Proof state:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : NeZero p
inst✝ : CharZero R
n : ℕ
⊢ ∀ (i : ℕ), ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars = {i}

Tactic:
intro i

Result:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : NeZero p
inst✝ : CharZero R
n i : ℕ
⊢ ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars = {i}

Proof state:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : NeZero p
inst✝ : CharZero R
n : ℕ
⊢ (W_ R n).vars = range (n + 1)

Tactic:
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

Result:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars = {i}
⊢ (W_ R n).vars = range (n + 1)

Proof state:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars = {i}
⊢ (W_ R n).vars = range (n + 1)

Tactic:
rw [wittPolynomial, vars_sum_of_disjoint]

Result:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars = {i}
⊢ ((range (n + 1)).biUnion fun i => ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars) = range (n + 1)

case h
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars = {i}
⊢ Pairwise (Function.onFun Disjoint fun i => ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars)

Proof state:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars = {i}
⊢ ((range (n + 1)).biUnion fun i => ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars) = range (n + 1)

Tactic:
simp only [this, biUnion_singleton_eq_self]

Result:
no goals

Proof state:
case h
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars = {i}
⊢ Pairwise (Function.onFun Disjoint fun i => ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars)

Tactic:
simp only [this]

Result:
case h
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars = {i}
⊢ Pairwise (Function.onFun Disjoint fun i => {i})

Proof state:
case h
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars = {i}
⊢ Pairwise (Function.onFun Disjoint fun i => {i})

Tactic:
intro a b h

Result:
case h
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars = {i}
a b : ℕ
h : a ≠ b
⊢ Function.onFun Disjoint (fun i => {i}) a b

Proof state:
case h
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars = {i}
a b : ℕ
h : a ≠ b
⊢ Function.onFun Disjoint (fun i => {i}) a b

Tactic:
apply disjoint_singleton_left.mpr

Result:
case h
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars = {i}
a b : ℕ
h : a ≠ b
⊢ a ∉ (fun i => {i}) b

Proof state:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : NeZero p
inst✝ : CharZero R
n i : ℕ
⊢ p ^ i ≠ 0

Tactic:
exact pow_ne_zero i hp.1

Result:
no goals

Proof state:
case h
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars = {i}
a b : ℕ
h : a ≠ b
⊢ a ∉ (fun i => {i}) b

Tactic:
rwa [mem_singleton]

Result:
no goals

Proof state:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : NeZero p
inst✝ : CharZero R
n i : ℕ
⊢ ↑p ^ i ≠ 0

Tactic:
rw [← Nat.cast_pow, Nat.cast_ne_zero]

Result:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : NeZero p
inst✝ : CharZero R
n i : ℕ
⊢ p ^ i ≠ 0