awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p n k : ℕ
hk : k ∈ range (n + 1)
e_a : n + 1 - k = n - k + 1
⊢ HMul.hMul (α := MvPolynomial ℕ (ZMod (p ^ (n + 1))))
      ((C : (a : ZMod (p ^ (n + 1))) → MvPolynomial ℕ (ZMod (p ^ (n + 1))))
          (HPow.hPow (α := ZMod (p ^ (n + 1))) (↑p : ZMod (p ^ (n + 1))) k) :
        MvPolynomial ℕ (ZMod (p ^ (n + 1))))
      (HPow.hPow (α := MvPolynomial ℕ (ZMod (p ^ (n + 1)))) (X k) (p ^ (n + 1 - k))) =
    HMul.hMul (α := MvPolynomial ℕ (ZMod (p ^ (n + 1))))
      ((algebraMap (ZMod (p ^ (n + 1))) (MvPolynomial ℕ (ZMod (p ^ (n + 1)))) :
            (a : ZMod (p ^ (n + 1))) → MvPolynomial ℕ (ZMod (p ^ (n + 1))))
          (HPow.hPow (α := ZMod (p ^ (n + 1))) (↑p : ZMod (p ^ (n + 1))) k) :
        MvPolynomial ℕ (ZMod (p ^ (n + 1))))
      (HPow.hPow (α := MvPolynomial ℕ (ZMod (p ^ (n + 1)))) (X k) (p ^ (n - k + 1)))

Tactic:
congr
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p n k : ℕ
hk : k ∈ range (n + 1)
⊢ k < n + 1

Tactic:
rw [mem_range] at hk

Premises used: Finset.mem_range
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p n k : ℕ
hk : k < n + 1
e_a : 1 + n - k = n - k + 1
e_a₁ : 1 + (n - k) = n - k + 1
e_a₂ e_a₃ : n - k + 1 = n - k + 1
⊢ n + 1 - k = n - k + 1

Tactic:
rw [add_comm, add_tsub_assoc_of_le (Nat.lt_succ_iff.mp hk), ← add_comm]

Premises used: add_tsub_assoc_of_le, add_comm, Nat.lt_succ_iff, Iff.mp
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : NeZero p
inst_1 : CharZero R
n i : ℕ
⊢ Eq (α := Finset ℕ)
    (vars.{u_1, 0} (R := R)
      ((monomial (single i (p ^ (n - i))) : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i)))
    {i}

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

Premises used: pow_ne_zero, NeZero.out, MvPolynomial.vars_monomial_single
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : NeZero p
inst_1 : CharZero R
n i : ℕ
refine : HPow.hPow (α := R) (↑p : R) i ≠ 0
⊢ Eq (α := Finset ℕ)
    (vars.{u_1, 0} (R := R)
      ((monomial (single i (p ^ (n - i))) : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i)))
    {i}

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

Premises used: pow_ne_zero, NeZero.out, MvPolynomial.vars_monomial_single
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : NeZero p
inst_1 : CharZero R
n i : ℕ
⊢ HPow.hPow (α := R) (↑p : R) i ≠ 0

Tactic:
exact_mod_cast pow_ne_zero i hp.1

Premises used: pow_ne_zero, NeZero.out
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : NeZero p
inst_1 : CharZero R
n : ℕ
⊢ ∀ (i : ℕ),
    Eq (α := Finset ℕ)
      (vars.{u_1, 0} (R := R)
        ((monomial (single i (p ^ (n - i))) : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i)))
      {i}

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) ?_
    exact_mod_cast pow_ne_zero i hp.1
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : NeZero p
inst_1 : CharZero R
n : ℕ
this :
  ∀ (i : ℕ),
    Eq (α := Finset ℕ)
      (vars.{u_1, 0} (R := R)
        ((monomial (single i (p ^ (n - i))) : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i)))
      {i}
rw :
  ((range (n + 1)).biUnion fun (i : ℕ) ↦
      vars.{u_1, 0} (R := R)
        ((monomial (single i (p ^ (n - i))) : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i))) =
    range (n + 1)
h :
  Pairwise (α := ℕ)
    (Function.onFun (β := Finset ℕ) Disjoint fun (i : ℕ) ↦
      vars.{u_1, 0} (R := R)
        ((monomial (single i (p ^ (n - i))) : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i)))
⊢ vars (W_ R n) = range (n + 1)

Tactic:
rw [wittPolynomial, vars_sum_of_disjoint]

Premises used: MvPolynomial.vars_sum_of_disjoint, wittPolynomial
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : NeZero p
inst_1 : CharZero R
n : ℕ
this :
  ∀ (i : ℕ),
    Eq (α := Finset ℕ)
      (vars.{u_1, 0} (R := R)
        ((monomial (single i (p ^ (n - i))) : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i)))
      {i}
⊢ ((range (n + 1)).biUnion fun (i : ℕ) ↦
      vars.{u_1, 0} (R := R)
        ((monomial (single i (p ^ (n - i))) : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i))) =
    range (n + 1)

Tactic:
simp only [this, biUnion_singleton_eq_self]

Premises used: Finset.biUnion_singleton_eq_self
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : NeZero p
inst_1 : CharZero R
n : ℕ
this :
  ∀ (i : ℕ),
    Eq (α := Finset ℕ)
      (vars.{u_1, 0} (R := R)
        ((monomial (single i (p ^ (n - i))) : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i)))
      {i}
h : Pairwise (α := ℕ) (Function.onFun (β := Finset ℕ) Disjoint fun (i : ℕ) ↦ {i})
⊢ Pairwise (α := ℕ)
    (Function.onFun (β := Finset ℕ) Disjoint fun (i : ℕ) ↦
      vars.{u_1, 0} (R := R)
        ((monomial (single i (p ^ (n - i))) : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i)))

Tactic:
simp only [this]
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : NeZero p
inst_1 : CharZero R
n : ℕ
this :
  ∀ (i : ℕ),
    Eq (α := Finset ℕ)
      (vars.{u_1, 0} (R := R)
        ((monomial (single i (p ^ (n - i))) : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i)))
      {i}
a b : ℕ
h : a ≠ b
h₁ : a ∉ (fun (i : ℕ) ↦ ({i} : Finset ℕ)) b
⊢ Function.onFun (β := Finset ℕ) Disjoint (fun (i : ℕ) ↦ {i}) a b

Tactic:
apply disjoint_singleton_left.mpr

Premises used: Iff.mpr, Finset.disjoint_singleton_left
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : NeZero p
inst_1 : CharZero R
n : ℕ
this :
  ∀ (i : ℕ),
    Eq (α := Finset ℕ)
      (vars.{u_1, 0} (R := R)
        ((monomial (single i (p ^ (n - i))) : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i)))
      {i}
a b : ℕ
h : a ≠ b
h₁ h₂ h₃ h₄ : ¬a = b
⊢ a ∉ (fun (i : ℕ) ↦ ({i} : Finset ℕ)) b

Tactic:
rwa [mem_singleton]

Premises used: Finset.mem_singleton
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : NeZero p
n : ℕ
rw :
  vars.{u_1, 0} (R := R) ((map (Int.castRingHom R) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ R) (W_ ℤ n)) ⊆
    vars (W_ ℤ n)
⊢ vars (W_ R n) ⊆ range (n + 1)

Tactic:
rw [← map_wittPolynomial p (Int.castRingHom R), ← wittPolynomial_vars p ℤ]

Premises used: wittPolynomial_vars, Int, Int.castRingHom, map_wittPolynomial
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : NeZero p
n : ℕ
⊢ vars.{u_1, 0} (R := R) ((map (Int.castRingHom R) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ R) (W_ ℤ n)) ⊆
    vars (W_ ℤ n)

Tactic:
apply vars_map

Premises used: MvPolynomial.vars_map
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) (↑p : R)
n : ℕ
rw :
  HMul.hMul (β := MvPolynomial ℕ R)
      (HSub.hSub (α := MvPolynomial ℕ R) (X n)
        (∑ i : Fin n,
          HMul.hMul (α := MvPolynomial ℕ R)
            ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) (↑i : ℕ)) : MvPolynomial ℕ R)
            (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R (↑i : ℕ)) (p ^ (n - (↑i : ℕ))))))
      ((C : (a : R) → MvPolynomial ℕ R)
          (HPow.hPow (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) n) :
        MvPolynomial ℕ R) =
    HMul.hMul (β := MvPolynomial ℕ R)
      (HSub.hSub (α := MvPolynomial ℕ R) (X n)
        (∑ i ∈ range n,
          HMul.hMul (α := MvPolynomial ℕ R)
            ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
            (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R i) (p ^ (n - i)))))
      ((C : (a : R) → MvPolynomial ℕ R)
          (HPow.hPow (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) n) :
        MvPolynomial ℕ R)
rw₁ rw₂ :
  HMul.hMul (β := MvPolynomial ℕ R)
      (HSub.hSub (α := MvPolynomial ℕ R) (X n)
        (∑ i : Fin n,
          HMul.hMul (α := MvPolynomial ℕ R)
            ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) (↑i : ℕ)) : MvPolynomial ℕ R)
            (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R (↑i : ℕ)) (p ^ (n - (↑i : ℕ))))))
      ((C : (a : R) → MvPolynomial ℕ R)
          (HPow.hPow (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) n) :
        MvPolynomial ℕ R) =
    HMul.hMul (β := MvPolynomial ℕ R)
      (HSub.hSub (α := MvPolynomial ℕ R) (X n)
        (∑ i : Fin n,
          HMul.hMul (α := MvPolynomial ℕ R)
            ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) (↑i : ℕ)) : MvPolynomial ℕ R)
            (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R (↑i : ℕ)) (p ^ (n - (↑i : ℕ))))))
      ((C : (a : R) → MvPolynomial ℕ R)
          (HPow.hPow (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) n) :
        MvPolynomial ℕ R)
⊢ xInTermsOfW p R n =
    HMul.hMul (β := MvPolynomial ℕ R)
      (HSub.hSub (α := MvPolynomial ℕ R) (X n)
        (∑ i ∈ range n,
          HMul.hMul (α := MvPolynomial ℕ R)
            ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
            (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R i) (p ^ (n - i)))))
      ((C : (a : R) → MvPolynomial ℕ R)
          (HPow.hPow (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) n) :
        MvPolynomial ℕ R)

Tactic:
rw [xInTermsOfW, ← Fin.sum_univ_eq_sum_range]

Premises used: Fin.sum_univ_eq_sum_range, xInTermsOfW
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
inst_1 : Invertible (α := R) (↑p : R)
n : ℕ
IH : ∀ m < n, Eq (α := R) ((constantCoeff : (a : MvPolynomial ℕ R) → R) (xInTermsOfW p R m) : R) (0 : R)
⊢ Eq (α := R) ((constantCoeff : (a : MvPolynomial ℕ R) → R) (xInTermsOfW p R n) : R) (0 : R)

Tactic:
?_
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
inst_1 : Invertible (α := R) (↑p : R)
n : ℕ
ind :
  ∀ (n : ℕ) (IH : ∀ m < n, Eq (α := R) ((constantCoeff : (a : MvPolynomial ℕ R) → R) (xInTermsOfW p R m) : R) (0 : R)),
    Eq (α := R) ((constantCoeff : (a : MvPolynomial ℕ R) → R) (xInTermsOfW p R n) : R) (0 : R)
⊢ Eq (α := R) ((constantCoeff : (a : MvPolynomial ℕ R) → R) (xInTermsOfW p R n) : R) (0 : R)

Tactic:
induction n using Nat.strongRecOn with | ind n IH => ?_
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
inst_1 : Invertible (α := R) (↑p : R)
n : ℕ
IH : ∀ m < n, Eq (α := R) ((constantCoeff : (a : MvPolynomial ℕ R) → R) (xInTermsOfW p R m) : R) (0 : R)
ind :
  ∀ x ∈ range n,
    Eq (α := R)
      ((constantCoeff : (a : MvPolynomial ℕ R) → R)
          (HMul.hMul (α := MvPolynomial ℕ R)
            ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) x) : MvPolynomial ℕ R)
            (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R x) (p ^ (n - x)))) :
        R)
      (0 : R)
⊢ Eq (α := R) ((constantCoeff : (a : MvPolynomial ℕ R) → R) (xInTermsOfW p R n) : R) (0 : R)

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

Premises used: map_sub, MvPolynomial.constantCoeff_C, Finset.sum_eq_zero, xInTermsOfW_eq, neg_eq_zero, map_sum, MulZeroClass.mul_zero, MvPolynomial.constantCoeff_X, map_mul, mul_comm, zero_sub, mul_neg
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
inst_1 : Invertible (α := R) (↑p : R)
n : ℕ
IH : ∀ m < n, Eq (α := R) ((constantCoeff : (a : MvPolynomial ℕ R) → R) (xInTermsOfW p R m) : R) (0 : R)
m : ℕ
H : m ∈ range n
⊢ m < n

Tactic:
rw [mem_range] at H

Premises used: Finset.mem_range
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
inst_1 : Invertible (α := R) (↑p : R)
n : ℕ
IH : ∀ m < n, Eq (α := R) ((constantCoeff : (a : MvPolynomial ℕ R) → R) (xInTermsOfW p R m) : R) (0 : R)
m : ℕ
H : m < n
ind : HPow.hPow (α := R) (↑p : R) m * HPow.hPow (α := R) 0 (p ^ (n - m)) = 0
⊢ Eq (α := R)
    ((constantCoeff : (a : MvPolynomial ℕ R) → R)
        (HMul.hMul (α := MvPolynomial ℕ R)
          ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) m) : MvPolynomial ℕ R)
          (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R m) (p ^ (n - m)))) :
      R)
    (0 : R)

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

Premises used: map_pow, map_mul, map_natCast
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
inst_1 : Invertible (α := R) (↑p : R)
n : ℕ
IH : ∀ m < n, Eq (α := R) ((constantCoeff : (a : MvPolynomial ℕ R) → R) (xInTermsOfW p R m) : R) (0 : R)
m : ℕ
H : m < n
ind : p ^ (n - m) ≠ 0
⊢ HPow.hPow (α := R) (↑p : R) m * HPow.hPow (α := R) 0 (p ^ (n - m)) = 0

Tactic:
rw [zero_pow, mul_zero]

Premises used: MulZeroClass.mul_zero, zero_pow
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
inst_1 : Invertible (α := R) (↑p : R)
n : ℕ
IH : ∀ m < n, Eq (α := R) ((constantCoeff : (a : MvPolynomial ℕ R) → R) (xInTermsOfW p R m) : R) (0 : R)
m : ℕ
H : m < n
⊢ p ^ (n - m) ≠ 0

Tactic:
pow_ne_zero _ hp.1.ne_zero

Premises used: pow_ne_zero, Nat.Prime.ne_zero, Fact.out
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
inst_1 : Invertible (α := R) (↑p : R)
n : ℕ
IH : ∀ m < n, Eq (α := R) ((constantCoeff : (a : MvPolynomial ℕ R) → R) (xInTermsOfW p R m) : R) (0 : R)
m : ℕ
H : m < n
⊢ p ^ (n - m) ≠ 0

Tactic:
exact pow_ne_zero _ hp.1.ne_zero

Premises used: pow_ne_zero, Nat.Prime.ne_zero, Fact.out
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) (↑p : R)
rw :
  HMul.hMul (β := MvPolynomial ℕ R)
      (HSub.hSub (α := MvPolynomial ℕ R) (X 0)
        (∑ i ∈ range 0,
          HMul.hMul (α := MvPolynomial ℕ R)
            ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
            (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R i) (p ^ (0 - i)))))
      ((C : (a : R) → MvPolynomial ℕ R)
          (HPow.hPow (α := R) (β := ℕ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) 0) :
        MvPolynomial ℕ R) =
    X 0
rw₁ :
  HMul.hMul (β := MvPolynomial ℕ R)
      (HSub.hSub (α := MvPolynomial ℕ R) (X 0)
        (∑ i ∈ ∅,
          HMul.hMul (α := MvPolynomial ℕ R)
            ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
            (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R i) (p ^ (0 - i)))))
      ((C : (a : R) → MvPolynomial ℕ R)
          (HPow.hPow (α := R) (β := ℕ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) 0) :
        MvPolynomial ℕ R) =
    X 0
rw₂ :
  HMul.hMul (β := MvPolynomial ℕ R) (HSub.hSub (α := MvPolynomial ℕ R) (X 0) 0)
      ((C : (a : R) → MvPolynomial ℕ R)
          (HPow.hPow (α := R) (β := ℕ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) 0) :
        MvPolynomial ℕ R) =
    X 0
rw₃ : HSub.hSub (α := MvPolynomial ℕ R) (X 0) 0 * (C : (a : R) → MvPolynomial ℕ R) 1 = X 0
rw₄ : HSub.hSub (α := MvPolynomial ℕ R) (X 0) 0 * 1 = X 0
rw₅ : HSub.hSub (α := MvPolynomial ℕ R) (X 0) 0 = X 0
rw₆ rw₇ : Eq.{u_1 + 1} (α := MvPolynomial ℕ R) (X 0) (X 0)
⊢ Eq (α := MvPolynomial ℕ R) (xInTermsOfW p R 0) (X 0)

Tactic:
rw [xInTermsOfW_eq, range_zero, sum_empty, pow_zero, C_1, mul_one, sub_zero]

Premises used: sub_zero, xInTermsOfW_eq, MvPolynomial.C_1, pow_zero, Finset.sum_empty, mul_one, Finset.range_zero
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ 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)

Tactic:
?_
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ind :
  ∀ (n : ℕ) (ih : ∀ 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)
⊢ n ∈ vars (xInTermsOfW p ℚ n) ∧ vars (xInTermsOfW p ℚ n) ⊆ range (n + 1)

Tactic:
induction n using Nat.strongRecOn with | ind n ih => ?_
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
ind :
  Membership.mem (γ := Finset ℕ)
      ({n} ∪
        vars (R := ℚ)
          (∑ i ∈ range n,
            HMul.hMul (α := MvPolynomial ℕ ℚ)
              ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
              (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ i) (p ^ (n - i)))))
      n ∧
    {n} ∪
        vars (R := ℚ)
          (∑ i ∈ range n,
            HMul.hMul (α := MvPolynomial ℕ ℚ)
              ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
              (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ i) (p ^ (n - i)))) ⊆
      {n} ∪ range n
ind₁ :
  Disjoint (vars (R := ℚ) (X n))
    (vars (R := ℚ)
      (∑ i ∈ range n,
        HMul.hMul (α := MvPolynomial ℕ ℚ)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
          (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ i) (p ^ (n - i)))))
⊢ n ∈ vars (xInTermsOfW p ℚ n) ∧ vars (xInTermsOfW p ℚ n) ⊆ range (n + 1)

Tactic:
rw [xInTermsOfW_eq, mul_comm, vars_C_mul _ (Invertible.ne_zero _),
    vars_sub_of_disjoint, vars_X, range_add_one, insert_eq]

Premises used: MvPolynomial.vars_X, Finset.insert_eq, MvPolynomial.vars_sub_of_disjoint, xInTermsOfW_eq, Finset.range_add_one, MvPolynomial.vars_C_mul, mul_comm
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
ind :
  {n} ∪
      vars (R := ℚ)
        (∑ i ∈ range n,
          HMul.hMul (α := MvPolynomial ℕ ℚ)
            ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
            (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ i) (p ^ (n - i)))) ⊆
    {n} ∪ range n
⊢ Membership.mem (γ := Finset ℕ)
      ({n} ∪
        vars (R := ℚ)
          (∑ i ∈ range n,
            HMul.hMul (α := MvPolynomial ℕ ℚ)
              ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
              (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ i) (p ^ (n - i)))))
      n ∧
    {n} ∪
        vars (R := ℚ)
          (∑ i ∈ range n,
            HMul.hMul (α := MvPolynomial ℕ ℚ)
              ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
              (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ i) (p ^ (n - i)))) ⊆
      {n} ∪ range n

Tactic:
simp only [true_and, true_or, mem_union, mem_singleton]

Premises used: Finset.mem_singleton, true_or, Finset.mem_union, true_and
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i : ℕ
ind :
  Membership.mem (γ := Finset ℕ) {n} i ∨
      Membership.mem (γ := Finset ℕ)
        (vars (R := ℚ)
          (∑ i ∈ range n,
            HMul.hMul (α := MvPolynomial ℕ ℚ)
              ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
              (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ i) (p ^ (n - i)))))
        i →
    Membership.mem (γ := Finset ℕ) {n} i ∨ i ∈ range n
⊢ Membership.mem (γ := Finset ℕ)
      ({n} ∪
        vars (R := ℚ)
          (∑ i ∈ range n,
            HMul.hMul (α := MvPolynomial ℕ ℚ)
              ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
              (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ i) (p ^ (n - i)))))
      i →
    i ∈ {n} ∪ range n

Tactic:
rw [mem_union, mem_union]

Premises used: Finset.mem_union
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i : ℕ
ind :
  Membership.mem (γ := Finset ℕ)
      (vars (R := ℚ)
        (∑ i ∈ range n,
          HMul.hMul (α := MvPolynomial ℕ ℚ)
            ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
            (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ i) (p ^ (n - i)))))
      i →
    i ∈ range n
⊢ Membership.mem (γ := Finset ℕ) {n} i ∨
      Membership.mem (γ := Finset ℕ)
        (vars (R := ℚ)
          (∑ i ∈ range n,
            HMul.hMul (α := MvPolynomial ℕ ℚ)
              ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
              (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ i) (p ^ (n - i)))))
        i →
    Membership.mem (γ := Finset ℕ) {n} i ∨ i ∈ range n

Tactic:
apply Or.imp id

Premises used: id, Or.imp
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
ind :
  ∀ ⦃i : ℕ⦄,
    Membership.mem (γ := Finset ℕ)
        (vars (R := ℚ)
          (∑ i ∈ range n,
            HMul.hMul (α := MvPolynomial ℕ ℚ)
              ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
              (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ i) (p ^ (n - i)))))
        i →
      i ∈ range n
⊢ Membership.mem (γ := Finset ℕ)
      ({n} ∪
        vars (R := ℚ)
          (∑ i ∈ range n,
            HMul.hMul (α := MvPolynomial ℕ ℚ)
              ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
              (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ i) (p ^ (n - i)))))
      n ∧
    {n} ∪
        vars (R := ℚ)
          (∑ i ∈ range n,
            HMul.hMul (α := MvPolynomial ℕ ℚ)
              ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
              (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ i) (p ^ (n - i)))) ⊆
      {n} ∪ range n

Tactic:
on_goal 1 =>
    simp only [true_and, true_or, mem_union, mem_singleton]
    intro i
    rw [mem_union, mem_union]
    apply Or.imp id

Premises used: Finset.mem_singleton, true_or, id, Finset.mem_union, Or.imp, true_and
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
ind :
  n ∉
    vars (R := ℚ)
      (∑ i ∈ range n,
        HMul.hMul (α := MvPolynomial ℕ ℚ)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
          (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ i) (p ^ (n - i))))
⊢ Disjoint (vars (R := ℚ) (X n))
    (vars (R := ℚ)
      (∑ i ∈ range n,
        HMul.hMul (α := MvPolynomial ℕ ℚ)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
          (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ i) (p ^ (n - i)))))

Tactic:
rw [vars_X, disjoint_singleton_left]

Premises used: MvPolynomial.vars_X, Finset.disjoint_singleton_left