awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p n : ℕ
⊢ Eq (α := MvPolynomial ℕ (ZMod (p ^ (n + 1))))
    (∑ i ∈ range (n + 1 + 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))) i) :
          MvPolynomial ℕ (ZMod (p ^ (n + 1))))
        (HPow.hPow (α := MvPolynomial ℕ (ZMod (p ^ (n + 1)))) (X i) (p ^ (n + 1 - i))))
    ((expand p : (a : MvPolynomial ℕ (ZMod (p ^ (n + 1)))) → MvPolynomial ℕ (ZMod (p ^ (n + 1))))
      (∑ i ∈ range (n + 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))) i) :
            MvPolynomial ℕ (ZMod (p ^ (n + 1))))
          (HPow.hPow (α := MvPolynomial ℕ (ZMod (p ^ (n + 1)))) (X i) (p ^ (n - i)))))
have rw : ∀ x ∈ range (n + 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))) x) :
        MvPolynomial ℕ (ZMod (p ^ (n + 1))))
      (HPow.hPow (α := MvPolynomial ℕ (ZMod (p ^ (n + 1)))) (X x) (p ^ (n + 1 - x))) =
    (expand p : (a : MvPolynomial ℕ (ZMod (p ^ (n + 1)))) → MvPolynomial ℕ (ZMod (p ^ (n + 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))) x) :
          MvPolynomial ℕ (ZMod (p ^ (n + 1))))
        (HPow.hPow (α := MvPolynomial ℕ (ZMod (p ^ (n + 1)))) (X x) (p ^ (n - x))))
Tactic: rw [sum_range_succ, ← Nat.cast_pow, CharP.cast_eq_zero (ZMod (p ^ (n + 1))) (p ^ (n + 1)), C_0,
    zero_mul, add_zero, map_sum, sum_congr rfl]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p n k : ℕ
hk : k ∈ range (n + 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))) =
    (expand p : (a : MvPolynomial ℕ (ZMod (p ^ (n + 1)))) → MvPolynomial ℕ (ZMod (p ^ (n + 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 - k))))
have rw : 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: rw [map_mul (expand p), map_pow (expand p), expand_X, algHom_C, ← pow_mul, ← pow_succ']
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p n k : ℕ
hk : k ∈ range (n + 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)))
have e_a : n + 1 - k = n - k + 1
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (hypothesis)
Goal:
p n k : ℕ
hk : k ∈ range (n + 1)
⊢ n + 1 - k = n - k + 1
have hk₁ : k < n + 1
Tactic: rw [mem_range] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p n k : ℕ
hk : k < n + 1
⊢ n + 1 - k = n - k + 1
have e_a : 1 + n - k = n - k + 1
Tactic: rw [add_comm, add_tsub_assoc_of_le (Nat.lt_succ_iff.mp hk), ← add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p n k : ℕ
hk : k < n + 1
e_a : 1 + n - k = n - k + 1
⊢ n + 1 - k = n - k + 1
have e_a₁ : 1 + (n - k) = n - k + 1
Tactic: rw [add_comm, add_tsub_assoc_of_le (Nat.lt_succ_iff.mp hk), ← add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p n k : ℕ
hk : k < n + 1
e_a : 1 + n - k = n - k + 1
e_a₁ : 1 + (n - k) = n - k + 1
⊢ n + 1 - k = n - k + 1
have e_a₂ : n - k + 1 = n - k + 1
Tactic: rw [add_comm, add_tsub_assoc_of_le (Nat.lt_succ_iff.mp hk), ← add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
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}
have refine : HPow.hPow (α := R) (↑p : R) i ≠ 0
Tactic: refine vars_monomial_single i (pow_ne_zero _ hp.1) ?_
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (hypothesis)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : NeZero p
inst_1 : CharZero R
n : ℕ
⊢ vars (W_ R n) = range (n + 1)
have 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}
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
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
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}
⊢ vars (W_ R n) = range (n + 1)
have 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)
Tactic: rw [wittPolynomial, vars_sum_of_disjoint]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
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)
⊢ vars (W_ R n) = range (n + 1)
have 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)))
Tactic: rw [wittPolynomial, vars_sum_of_disjoint]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
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}
⊢ 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)))
have h : Pairwise (α := ℕ) (Function.onFun (β := Finset ℕ) Disjoint fun (i : ℕ) ↦ {i})
Tactic: simp only [this]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
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
⊢ Function.onFun (β := Finset ℕ) Disjoint (fun (i : ℕ) ↦ {i}) a b
have h₁ : a ∉ (fun (i : ℕ) ↦ ({i} : Finset ℕ)) b
Tactic: apply disjoint_singleton_left.mpr
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
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
⊢ a ∉ (fun (i : ℕ) ↦ ({i} : Finset ℕ)) b
have h₁ : ¬a = b
Tactic: rwa [mem_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : NeZero p
n : ℕ
⊢ vars (W_ R n) ⊆ range (n + 1)
have rw : vars.{u_1, 0} (R := R) ((map (Int.castRingHom R) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ R) (W_ ℤ n)) ⊆ vars (W_ ℤ n)
Tactic: rw [← map_wittPolynomial p (Int.castRingHom R), ← wittPolynomial_vars p ℤ]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) (↑p : R)
n : ℕ
⊢ 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)
have 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)
Tactic: rw [xInTermsOfW, ← Fin.sum_univ_eq_sum_range]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
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)
⊢ 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)
have 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)
Tactic: rw [xInTermsOfW, ← Fin.sum_univ_eq_sum_range]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
inst_1 : Invertible (α := R) (↑p : R)
n : ℕ
⊢ Eq (α := R) ((constantCoeff : (a : MvPolynomial ℕ R) → R) (xInTermsOfW p R n) : R) (0 : R)
have 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)
Tactic: induction n using Nat.strongRecOn with | ind n IH => ?_
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
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)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (hypothesis)
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
⊢ 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)
have H₁ : m < n
Tactic: rw [mem_range] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
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
⊢ 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)
have ind : HPow.hPow (α := R) (↑p : R) m * HPow.hPow (α := R) 0 (p ^ (n - m)) = 0
Tactic: simp only [map_mul, map_pow, map_natCast, IH m H]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
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
⊢ HPow.hPow (α := R) (↑p : R) m * HPow.hPow (α := R) 0 (p ^ (n - m)) = 0
have ind : p ^ (n - m) ≠ 0
Tactic: rw [zero_pow, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) (↑p : R)
⊢ Eq (α := MvPolynomial ℕ R) (xInTermsOfW p R 0) (X 0)
have 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
Tactic: rw [xInTermsOfW_eq, range_zero, sum_empty, pow_zero, C_1, mul_one, sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
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
⊢ Eq (α := MvPolynomial ℕ R) (xInTermsOfW p R 0) (X 0)
have 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
Tactic: rw [xInTermsOfW_eq, range_zero, sum_empty, pow_zero, C_1, mul_one, sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
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
⊢ Eq (α := MvPolynomial ℕ R) (xInTermsOfW p R 0) (X 0)
have 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
Tactic: rw [xInTermsOfW_eq, range_zero, sum_empty, pow_zero, C_1, mul_one, sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
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
⊢ Eq (α := MvPolynomial ℕ R) (xInTermsOfW p R 0) (X 0)
have rw₃ : HSub.hSub (α := MvPolynomial ℕ R) (X 0) 0 * (C : (a : R) → MvPolynomial ℕ R) 1 = X 0
Tactic: rw [xInTermsOfW_eq, range_zero, sum_empty, pow_zero, C_1, mul_one, sub_zero]