awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
refine_2 :
  Finsupp.support (Finsupp.single (1, x) (p ^ (n + 1 - x))) ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
⊢ vars (R := ℤ)
      ((rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄)
        ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ)
          (HPow.hPow (α := ℤ) (↑p : ℤ) x))) ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
have refine_2₁ : HPow.hPow (α := ℤ) (↑p : ℤ) x ≠ 0
Tactic: rw [rename_monomial, vars_monomial, Finsupp.mapDomain_single]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
⊢ Finsupp.support (Finsupp.single (1, x) (p ^ (n + 1 - x))) ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
have refine_2 : {(1, x)} ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
Tactic: apply Subset.trans Finsupp.support_single_subset
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) x ≠ 0
have refine_2 : Ne (α := ℤ) (↑p : ℤ) 0
Tactic: apply pow_ne_zero
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∑ i ∈ range (n + 1), HPow.hPow (α := 𝕄) (↑p : 𝕄) i * wittMul p i ^ p ^ (n - i) =
    HMul.hMul (α := 𝕄) (β := 𝕄) ((rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ n) : 𝕄)
      ((rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ n) : 𝕄)
have h : Eq (α := 𝕄) (∑ i ∈ range (n + 1), HPow.hPow (α := 𝕄) (↑p : 𝕄) i * wittMul p i ^ p ^ (n - i) : 𝕄)
  ((bind₁ (wittStructureInt p (HMul.hMul (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1))) : (a : MvPolynomial ℕ ℤ) → 𝕄)
      (wittPolynomial p ℤ n) :
    𝕄)
Tactic: convert! wittStructureInt_prop p (X (0 : Fin 2) * X 1) n using 1
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h :
  Eq (α := 𝕄) (∑ i ∈ range (n + 1), HPow.hPow (α := 𝕄) (↑p : 𝕄) i * wittMul p i ^ p ^ (n - i) : 𝕄)
    ((bind₁ (wittStructureInt p (HMul.hMul (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1))) : (a : MvPolynomial ℕ ℤ) → 𝕄)
        (wittPolynomial p ℤ n) :
      𝕄)
⊢ ∑ i ∈ range (n + 1), HPow.hPow (α := 𝕄) (↑p : 𝕄) i * wittMul p i ^ p ^ (n - i) =
    HMul.hMul (α := 𝕄) (β := 𝕄) ((rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ n) : 𝕄)
      ((rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ n) : 𝕄)
have h₁ : HMul.hMul (α := 𝕄) (β := 𝕄) ((rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ n) : 𝕄)
    ((rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ n) : 𝕄) =
  (bind₁ fun (i : Fin 2) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ n) :
      (a : MvPolynomial (Fin 2) ℤ) → 𝕄)
    (HMul.hMul (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1))
Tactic: convert! wittStructureInt_prop p (X (0 : Fin 2) * X 1) n using 1
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ Eq (α := 𝕄)
    (∑ x ∈ range (n + 1),
      HPow.hPow (α := 𝕄) (↑p : 𝕄) x *
        wittStructureInt p (HMul.hMul (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1)) x ^ p ^ (n - x))
    ((bind₁ (wittStructureInt p (HMul.hMul (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1))) : (a : MvPolynomial ℕ ℤ) → 𝕄)
      (∑ i ∈ range (n + 1),
        (monomial (Finsupp.single i (p ^ (n - i))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) i)))
have h : Eq (α := 𝕄)
  (∑ x ∈ range (n + 1),
    HPow.hPow (α := 𝕄) (↑p : 𝕄) x *
      wittStructureInt p (HMul.hMul (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1)) x ^ p ^ (n - x))
  (∑ x ∈ range (n + 1),
    (bind₁ (wittStructureInt p (HMul.hMul (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1))) : (a : MvPolynomial ℕ ℤ) → 𝕄)
      ((monomial (Finsupp.single x (p ^ (n - x))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) x)))
Tactic: rw [map_sum]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ Eq (α := 𝕄)
    (∑ x ∈ range (n + 1),
      HPow.hPow (α := 𝕄) (↑p : 𝕄) x *
        wittStructureInt p (HMul.hMul (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1)) x ^ p ^ (n - x))
    (∑ x ∈ range (n + 1),
      (bind₁ (wittStructureInt p (HMul.hMul (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1))) : (a : MvPolynomial ℕ ℤ) → 𝕄)
        ((monomial (Finsupp.single x (p ^ (n - x))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) x)))
have h : ∀ (i : ℕ) (m : Fin 2 × ℕ →₀ ℕ),
  MvPolynomial.coeff m
      (HPow.hPow (α := 𝕄) (↑p : 𝕄) i *
        wittStructureInt p (HMul.hMul (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1)) i ^ p ^ (n - i)) =
    MvPolynomial.coeff m
      ((bind₁ (wittStructureInt p (HMul.hMul (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1))) : (a : MvPolynomial ℕ ℤ) → 𝕄)
        ((monomial (Finsupp.single i (p ^ (n - i))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) i)))
Tactic: congr 1 with i
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n i : ℕ
m : Fin 2 × ℕ →₀ ℕ
⊢ MvPolynomial.coeff m
      (HPow.hPow (α := 𝕄) (↑p : 𝕄) i *
        wittStructureInt p (HMul.hMul (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1)) i ^ p ^ (n - i)) =
    MvPolynomial.coeff m
      ((bind₁ (wittStructureInt p (HMul.hMul (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1))) : (a : MvPolynomial ℕ ℤ) → 𝕄)
        ((monomial (Finsupp.single i (p ^ (n - i))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) i)))
have h : HPow.hPow (α := 𝕄) (↑p : 𝕄) i *
    wittStructureInt p (HMul.hMul (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1)) i ^ p ^ (n - i) =
  (bind₁ (wittStructureInt p (HMul.hMul (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1))) : (a : MvPolynomial ℕ ℤ) → 𝕄)
    ((monomial (Finsupp.single i (p ^ (n - i))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) i))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n i : ℕ
m : Fin 2 × ℕ →₀ ℕ
⊢ Finsupp.support (Finsupp.single i (p ^ (n - i))) = {i}
have rw : Ne (α := ℕ) ((Finsupp.single i (p ^ (n - i)) : (a : ℕ) → ℕ) i : ℕ) (0 : ℕ) ∧
  Eq (α := ℕ →₀ ℕ) (Finsupp.single i (p ^ (n - i)))
    (Finsupp.single i ((Finsupp.single i (p ^ (n - i)) : (a : ℕ) → ℕ) i))
Tactic: rw [Finsupp.support_eq_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n i : ℕ
m : Fin 2 × ℕ →₀ ℕ
⊢ Ne (α := ℕ) ((Finsupp.single i (p ^ (n - i)) : (a : ℕ) → ℕ) i : ℕ) (0 : ℕ) ∧
    Eq (α := ℕ →₀ ℕ) (Finsupp.single i (p ^ (n - i)))
      (Finsupp.single i ((Finsupp.single i (p ^ (n - i)) : (a : ℕ) → ℕ) i))
have simp : ¬p ^ (n - i) = 0
Tactic: simp only [and_true, Finsupp.single_eq_same, Ne]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n i : ℕ
m : Fin 2 × ℕ →₀ ℕ
⊢ HPow.hPow (α := 𝕄) (↑p : 𝕄) i *
      wittStructureInt p (HMul.hMul (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1)) i ^ p ^ (n - i) =
    (bind₁ (wittStructureInt p (HMul.hMul (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1))) : (a : MvPolynomial ℕ ℤ) → 𝕄)
      ((monomial (Finsupp.single i (p ^ (n - i))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) i))
have hsupp : Finsupp.support (Finsupp.single i (p ^ (n - i))) = {i}
Tactic: have hsupp : (Finsupp.single i (p ^ (n - i))).support = {i} := by
      rw [Finsupp.support_eq_singleton]
      simp only [and_true, Finsupp.single_eq_same, Ne]
      exact pow_ne_zero _ hp.out.ne_zero
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ HPow.hPow (α := 𝕄) (↑p : 𝕄) n * wittMul p n + wittPolyProdRemainder p n = wittPolyProd p n
have h : HPow.hPow (α := 𝕄) (↑p : 𝕄) n * wittMul p n + wittPolyProdRemainder p n =
  ∑ i ∈ range (n + 1), HPow.hPow (α := 𝕄) (↑p : 𝕄) i * wittMul p i ^ p ^ (n - i)
Tactic: convert! mul_polyOfInterest_aux1 p n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ HPow.hPow (α := 𝕄) (↑p : 𝕄) n * wittMul p n + wittPolyProdRemainder p n =
    ∑ i ∈ range (n + 1), HPow.hPow (α := 𝕄) (↑p : 𝕄) i * wittMul p i ^ p ^ (n - i)
have h : wittPolyProdRemainder p n + HPow.hPow (α := 𝕄) (↑p : 𝕄) n * wittMul p n =
  ∑ x ∈ range n, HPow.hPow (α := 𝕄) (↑p : 𝕄) x * wittMul p x ^ p ^ (n - x) + HPow.hPow (α := 𝕄) (↑p : 𝕄) n * wittMul p n
Tactic: rw [sum_range_succ, add_comm, Nat.sub_self, pow_zero, pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p n : ℕ
⊢ HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) = (C : (a : ℤ) → 𝕄) (HPow.hPow (α := ℤ) (↑p : ℤ) (n + 1))
have norm_cast : Eq (α := 𝕄) (↑(p ^ (n + 1)) : 𝕄) ((C : (a : ℤ) → 𝕄) (↑(p ^ (n + 1)) : ℤ))
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (hypothesis)
Goal:
p n : ℕ
⊢ wittPolyProd p (n + 1) =
    -(HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (0, n + 1)) * (HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (1, n + 1)) +
          HMul.hMul (β := 𝕄) (HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (0, n + 1))
            ((rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ (n + 1)) : 𝕄) +
        HMul.hMul (β := 𝕄) (HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (1, n + 1))
          ((rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ (n + 1)) : 𝕄) +
      remainder p n
have mvpz : HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) = (C : (a : ℤ) → 𝕄) (HPow.hPow (α := ℤ) (↑p : ℤ) (n + 1))
Tactic: have mvpz : (p : 𝕄) ^ (n + 1) = MvPolynomial.C ((p : ℤ) ^ (n + 1)) := by norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p n : ℕ
mvpz : HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) = (C : (a : ℤ) → 𝕄) (HPow.hPow (α := ℤ) (↑p : ℤ) (n + 1))
⊢ wittPolyProd p (n + 1) =
    -(HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (0, n + 1)) * (HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (1, n + 1)) +
          HMul.hMul (β := 𝕄) (HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (0, n + 1))
            ((rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ (n + 1)) : 𝕄) +
        HMul.hMul (β := 𝕄) (HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (1, n + 1))
          ((rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ (n + 1)) : 𝕄) +
      remainder p n
have rw : HMul.hMul (α := 𝕄)
    (∑ x ∈ range (n + 1 + 1),
      (rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄)
        ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) x)))
    (∑ x ∈ range (n + 1 + 1),
      (rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄)
        ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ)
          (HPow.hPow (α := ℤ) (↑p : ℤ) x))) =
  -(HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (0, n + 1)) * (HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (1, n + 1)) +
        HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (0, n + 1) *
          ∑ x ∈ range (n + 1 + 1),
            (rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄)
              ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ)
                (HPow.hPow (α := ℤ) (↑p : ℤ) x)) +
      HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (1, n + 1) *
        ∑ x ∈ range (n + 1 + 1),
          (rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄)
            ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ)
              (HPow.hPow (α := ℤ) (↑p : ℤ) x)) +
    remainder p n
Tactic: rw [wittPolyProd, wittPolynomial, map_sum, map_sum]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p n : ℕ
mvpz : HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) = (C : (a : ℤ) → 𝕄) (HPow.hPow (α := ℤ) (↑p : ℤ) (n + 1))
| HMul.hMul (α := 𝕄)
    (∑ x ∈ range (n + 1 + 1),
      (rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄)
        ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) x)))
    (∑ x ∈ range (n + 1 + 1),
      (rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄)
        ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) x)))
have arg : ∑ x ∈ range (n + 1 + 1),
  (rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄)
    ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) x))
Tactic: arg 1
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p n : ℕ
mvpz : HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) = (C : (a : ℤ) → 𝕄) (HPow.hPow (α := ℤ) (↑p : ℤ) (n + 1))
| ∑ x ∈ range (n + 1 + 1),
    (rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄)
      ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) x))
have rw : ∑ x ∈ range (n + 1),
    (rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄)
      ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) x)) +
  HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (0, n + 1)
Tactic: rw [sum_range_succ, ← C_mul_X_pow_eq_monomial, tsub_self, pow_zero, pow_one, map_mul,
      rename_C, rename_X, ← mvpz]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p n : ℕ
mvpz : HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) = (C : (a : ℤ) → 𝕄) (HPow.hPow (α := ℤ) (↑p : ℤ) (n + 1))
| HMul.hMul (α := 𝕄)
    (∑ x ∈ range (n + 1 + 1),
      (rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄)
        ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) x)))
    (∑ x ∈ range (n + 1 + 1),
      (rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄)
        ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) x)))
have arg : ∑ x ∈ range (n + 1),
    (rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄)
      ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) x)) +
  HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (0, n + 1)
Tactic: arg 1
    rw [sum_range_succ, ← C_mul_X_pow_eq_monomial, tsub_self, pow_zero, pow_one, map_mul,
      rename_C, rename_X, ← mvpz]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p n : ℕ
mvpz : HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) = (C : (a : ℤ) → 𝕄) (HPow.hPow (α := ℤ) (↑p : ℤ) (n + 1))
⊢ HMul.hMul (α := 𝕄)
      (∑ x ∈ range (n + 1 + 1),
        (rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄)
          ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ)
            (HPow.hPow (α := ℤ) (↑p : ℤ) x)))
      (∑ x ∈ range (n + 1 + 1),
        (rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄)
          ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ)
            (HPow.hPow (α := ℤ) (↑p : ℤ) x))) =
    -(HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (0, n + 1)) * (HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (1, n + 1)) +
          HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (0, n + 1) *
            ∑ x ∈ range (n + 1 + 1),
              (rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄)
                ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ)
                  (HPow.hPow (α := ℤ) (↑p : ℤ) x)) +
        HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (1, n + 1) *
          ∑ x ∈ range (n + 1 + 1),
            (rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄)
              ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ)
                (HPow.hPow (α := ℤ) (↑p : ℤ) x)) +
      remainder p n
have conv_lhs : (∑ x ∈ range (n + 1),
        (rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄)
          ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ)
            (HPow.hPow (α := ℤ) (↑p : ℤ) x)) +
      HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (0, n + 1)) *
    ∑ x ∈ range (n + 1 + 1),
      (rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄)
        ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) x)) =
  -(HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (0, n + 1)) * (HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (1, n + 1)) +
        HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (0, n + 1) *
          ∑ x ∈ range (n + 1 + 1),
            (rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄)
              ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ)
                (HPow.hPow (α := ℤ) (↑p : ℤ) x)) +
      HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (1, n + 1) *
        ∑ x ∈ range (n + 1 + 1),
          (rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄)
            ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ)
              (HPow.hPow (α := ℤ) (↑p : ℤ) x)) +
    remainder p n
Tactic: conv_lhs =>
    arg 1
    rw [sum_range_succ, ← C_mul_X_pow_eq_monomial, tsub_self, pow_zero, pow_one, map_mul,
      rename_C, rename_X, ← mvpz]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p n : ℕ
mvpz : HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) = (C : (a : ℤ) → 𝕄) (HPow.hPow (α := ℤ) (↑p : ℤ) (n + 1))
| (∑ x ∈ range (n + 1),
        (rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄)
          ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ)
            (HPow.hPow (α := ℤ) (↑p : ℤ) x)) +
      HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (0, n + 1)) *
    ∑ x ∈ range (n + 1 + 1),
      (rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄)
        ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) x))
have arg : ∑ x ∈ range (n + 1 + 1),
  (rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄)
    ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) x))
Tactic: arg 2
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p n : ℕ
mvpz : HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) = (C : (a : ℤ) → 𝕄) (HPow.hPow (α := ℤ) (↑p : ℤ) (n + 1))
| ∑ x ∈ range (n + 1 + 1),
    (rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄)
      ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) x))
have rw : ∑ x ∈ range (n + 1),
    (rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄)
      ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) x)) +
  HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (1, n + 1)
Tactic: rw [sum_range_succ, ← C_mul_X_pow_eq_monomial, tsub_self, pow_zero, pow_one, map_mul,
      rename_C, rename_X, ← mvpz]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p n : ℕ
mvpz : HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) = (C : (a : ℤ) → 𝕄) (HPow.hPow (α := ℤ) (↑p : ℤ) (n + 1))
| (∑ x ∈ range (n + 1),
        (rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄)
          ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ)
            (HPow.hPow (α := ℤ) (↑p : ℤ) x)) +
      HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (0, n + 1)) *
    ∑ x ∈ range (n + 1 + 1),
      (rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄)
        ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) x))
have arg : ∑ x ∈ range (n + 1),
    (rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄)
      ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) x)) +
  HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (1, n + 1)
Tactic: arg 2
    rw [sum_range_succ, ← C_mul_X_pow_eq_monomial, tsub_self, pow_zero, pow_one, map_mul,
      rename_C, rename_X, ← mvpz]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p n : ℕ
mvpz : HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) = (C : (a : ℤ) → 𝕄) (HPow.hPow (α := ℤ) (↑p : ℤ) (n + 1))
⊢ (∑ x ∈ range (n + 1),
          (rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄)
            ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ)
              (HPow.hPow (α := ℤ) (↑p : ℤ) x)) +
        HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (0, n + 1)) *
      ∑ x ∈ range (n + 1 + 1),
        (rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄)
          ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ)
            (HPow.hPow (α := ℤ) (↑p : ℤ) x)) =
    -(HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (0, n + 1)) * (HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (1, n + 1)) +
          HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (0, n + 1) *
            ∑ x ∈ range (n + 1 + 1),
              (rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄)
                ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ)
                  (HPow.hPow (α := ℤ) (↑p : ℤ) x)) +
        HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (1, n + 1) *
          ∑ x ∈ range (n + 1 + 1),
            (rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄)
              ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ)
                (HPow.hPow (α := ℤ) (↑p : ℤ) x)) +
      remainder p n
have conv_lhs : (∑ x ∈ range (n + 1),
        (rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄)
          ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ)
            (HPow.hPow (α := ℤ) (↑p : ℤ) x)) +
      HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (0, n + 1)) *
    (∑ x ∈ range (n + 1),
        (rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄)
          ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ)
            (HPow.hPow (α := ℤ) (↑p : ℤ) x)) +
      HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (1, n + 1)) =
  -(HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (0, n + 1)) * (HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (1, n + 1)) +
        HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (0, n + 1) *
          ∑ x ∈ range (n + 1 + 1),
            (rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄)
              ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ)
                (HPow.hPow (α := ℤ) (↑p : ℤ) x)) +
      HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (1, n + 1) *
        ∑ x ∈ range (n + 1 + 1),
          (rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄)
            ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ)
              (HPow.hPow (α := ℤ) (↑p : ℤ) x)) +
    remainder p n
Tactic: conv_lhs =>
    arg 2
    rw [sum_range_succ, ← C_mul_X_pow_eq_monomial, tsub_self, pow_zero, pow_one, map_mul,
      rename_C, rename_X, ← mvpz]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p n : ℕ
mvpz : HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) = (C : (a : ℤ) → 𝕄) (HPow.hPow (α := ℤ) (↑p : ℤ) (n + 1))
| -(HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (0, n + 1)) * (HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (1, n + 1)) +
        HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (0, n + 1) *
          ∑ x ∈ range (n + 1 + 1),
            (rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄)
              ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ)
                (HPow.hPow (α := ℤ) (↑p : ℤ) x)) +
      HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (1, n + 1) *
        ∑ x ∈ range (n + 1 + 1),
          (rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄)
            ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ)
              (HPow.hPow (α := ℤ) (↑p : ℤ) x)) +
    remainder p n
have enter : ∑ x ∈ range (n + 1 + 1),
  (rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄)
    ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) x))
Tactic: enter [1, 1, 2, 2]