awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
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) *
        ∑ x ∈ range (n + 1),
          (rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄)
            ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ)
              (HPow.hPow (α := ℤ) (↑p : ℤ) x)) +
      ((∑ 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 (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)) * (HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (1, n + 1)) +
      (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 (0, n + 1) * (HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (1, n + 1)) +
          (HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (1, 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 (1, n + 1) * (HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (0, n + 1)))))

Tactic:
ring
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
rw :
  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
⊢ HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * wittMul 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 - wittPolyProdRemainder p (n + 1))

Tactic:
rw [← add_sub_assoc, eq_sub_iff_add_eq, mul_polyOfInterest_aux2]

Premises used: add_sub_assoc, WittVector.mul_polyOfInterest_aux2, eq_sub_iff_add_eq
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime 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

Tactic:
mul_polyOfInterest_aux3 _ _

Premises used: WittVector.mul_polyOfInterest_aux3
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime 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

Tactic:
exact mul_polyOfInterest_aux3 _ _

Premises used: WittVector.mul_polyOfInterest_aux3
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
simp :
  HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * wittMul p (n + 1) +
      HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * (HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (0, n + 1) * X (1, n + 1)) =
    HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) *
        HMul.hMul (α := 𝕄) (β := 𝕄) (X (0, n + 1))
          ((rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ (n + 1)) : 𝕄) +
      (HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) *
          HMul.hMul (α := 𝕄) (β := 𝕄) (X (1, n + 1))
            ((rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ (n + 1)) : 𝕄) +
        (remainder p n - wittPolyProdRemainder p (n + 1)))
⊢ HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * polyOfInterest p n = remainder p n - wittPolyProdRemainder p (n + 1)

Tactic:
simp only [polyOfInterest, mul_sub, mul_add, sub_eq_iff_eq_add']

Premises used: mul_sub, mul_add, sub_eq_iff_eq_add', WittVector.polyOfInterest
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
rw :
  -(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 - wittPolyProdRemainder p (n + 1)) +
      HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * (HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (0, n + 1) * X (1, n + 1)) =
    HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) *
        HMul.hMul (α := 𝕄) (β := 𝕄) (X (0, n + 1))
          ((rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ (n + 1)) : 𝕄) +
      (HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) *
          HMul.hMul (α := 𝕄) (β := 𝕄) (X (1, n + 1))
            ((rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ (n + 1)) : 𝕄) +
        (remainder p n - wittPolyProdRemainder p (n + 1)))
⊢ HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * wittMul p (n + 1) +
      HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * (HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (0, n + 1) * X (1, n + 1)) =
    HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) *
        HMul.hMul (α := 𝕄) (β := 𝕄) (X (0, n + 1))
          ((rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ (n + 1)) : 𝕄) +
      (HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) *
          HMul.hMul (α := 𝕄) (β := 𝕄) (X (1, n + 1))
            ((rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ (n + 1)) : 𝕄) +
        (remainder p n - wittPolyProdRemainder p (n + 1)))

Tactic:
rw [mul_polyOfInterest_aux4 p n]

Premises used: WittVector.mul_polyOfInterest_aux4
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ -(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 - wittPolyProdRemainder p (n + 1)) +
      HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * (HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (0, n + 1) * X (1, n + 1)) =
    HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) *
        HMul.hMul (α := 𝕄) (β := 𝕄) (X (0, n + 1))
          ((rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ (n + 1)) : 𝕄) +
      (HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) *
          HMul.hMul (α := 𝕄) (β := 𝕄) (X (1, n + 1))
            ((rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ (n + 1)) : 𝕄) +
        (remainder p n - wittPolyProdRemainder p (n + 1)))

Tactic:
ring
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
rw : (remainder p n - wittPolyProdRemainder p (n + 1)).vars ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
⊢ (HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * polyOfInterest p n).vars ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))

Tactic:
rw [mul_polyOfInterest_aux5]

Premises used: WittVector.mul_polyOfInterest_aux5
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
apply :
  (remainder p n).vars ∪ (wittPolyProdRemainder p (n + 1)).vars ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
⊢ (remainder p n - wittPolyProdRemainder p (n + 1)).vars ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))

Tactic:
apply Subset.trans (vars_sub_subset _)

Premises used: Finset.Subset.trans, MvPolynomial.vars_sub_subset
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (remainder p n).vars ∪ (wittPolyProdRemainder p (n + 1)).vars ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))

Tactic:
union_subset ?_ ?_

Premises used: Finset.union_subset
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
refine_1 : (remainder p n).vars ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
refine_2 : (wittPolyProdRemainder p (n + 1)).vars ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
⊢ (remainder p n).vars ∪ (wittPolyProdRemainder p (n + 1)).vars ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))

Tactic:
refine union_subset ?_ ?_

Premises used: Finset.union_subset
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (remainder p n).vars ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))

Tactic:
apply remainder_vars

Premises used: WittVector.remainder_vars
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (wittPolyProdRemainder p (n + 1)).vars ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))

Tactic:
apply wittPolyProdRemainder_vars

Premises used: WittVector.wittPolyProdRemainder_vars
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : Eq (α := 𝕄) (↑(p ^ (n + 1)) : 𝕄) ((C : (a : ℤ) → 𝕄) (↑(p ^ (n + 1)) : ℤ))
⊢ HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) = (C : (a : ℤ) → 𝕄) (HPow.hPow (α := ℤ) (↑p : ℤ) (n + 1))

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) = (C : (a : ℤ) → 𝕄) (HPow.hPow (α := ℤ) (↑p : ℤ) (n + 1))

Tactic:
have : (p : 𝕄) ^ (n + 1) = C ((p : ℤ) ^ (n + 1)) := by norm_cast
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
this : HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) = (C : (a : ℤ) → 𝕄) (HPow.hPow (α := ℤ) (↑p : ℤ) (n + 1))
ha : HPow.hPow (α := ℤ) (↑p : ℤ) (n + 1) ≠ 0
⊢ (polyOfInterest p n).vars =
    (HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) *
        (wittMul p (n + 1) + HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (0, n + 1) * X (1, n + 1) -
            HMul.hMul (α := 𝕄) (β := 𝕄) (X (0, n + 1))
              ((rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ (n + 1)) : 𝕄) -
          HMul.hMul (α := 𝕄) (β := 𝕄) (X (1, n + 1))
            ((rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ (n + 1)) : 𝕄))).vars

Tactic:
rw [polyOfInterest, this, vars_C_mul]

Premises used: MvPolynomial.vars_C_mul, WittVector.polyOfInterest
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
this : HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) = (C : (a : ℤ) → 𝕄) (HPow.hPow (α := ℤ) (↑p : ℤ) (n + 1))
ha : Ne (α := ℤ) (↑p : ℤ) 0
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) (n + 1) ≠ 0

Tactic:
apply pow_ne_zero

Premises used: pow_ne_zero
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
this : HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) = (C : (a : ℤ) → 𝕄) (HPow.hPow (α := ℤ) (↑p : ℤ) (n + 1))
⊢ Ne (α := ℤ) (↑p : ℤ) 0

Tactic:
mod_cast hp.out.ne_zero

Premises used: congrArg, cast, Ne, Nat.cast, Nat.Prime.ne_zero, Nat.cast_inj._simp_1, Nat.cast_zero, Eq.symm, Not, Fact.out, Eq.trans
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
this : HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) = (C : (a : ℤ) → 𝕄) (HPow.hPow (α := ℤ) (↑p : ℤ) (n + 1))
⊢ Ne (α := ℤ) (↑p : ℤ) 0

Tactic:
exact mod_cast hp.out.ne_zero

Premises used: Nat.Prime.ne_zero, Fact.out
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
rw :
  (HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) *
        (wittMul p (n + 1) + HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (0, n + 1) * X (1, n + 1) -
            HMul.hMul (α := 𝕄) (β := 𝕄) (X (0, n + 1))
              ((rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ (n + 1)) : 𝕄) -
          HMul.hMul (α := 𝕄) (β := 𝕄) (X (1, n + 1))
            ((rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ (n + 1)) : 𝕄))).vars ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
⊢ (polyOfInterest p n).vars ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))

Tactic:
rw [polyOfInterest_vars_eq]

Premises used: WittVector.polyOfInterest_vars_eq
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) *
        (wittMul p (n + 1) + HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (0, n + 1) * X (1, n + 1) -
            HMul.hMul (α := 𝕄) (β := 𝕄) (X (0, n + 1))
              ((rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ (n + 1)) : 𝕄) -
          HMul.hMul (α := 𝕄) (β := 𝕄) (X (1, n + 1))
            ((rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ (n + 1)) : 𝕄))).vars ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))

Tactic:
apply mul_polyOfInterest_vars

Premises used: WittVector.mul_polyOfInterest_vars
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
n : ℕ
x y : 𝕎 k
simp :
  HSub.hSub (α := k)
        (((aeval.{0, u_1, 0} (R := ℤ) (S₁ := k) (σ := Fin 2 × ℕ)
                  (Function.uncurry ![fun (i : ℕ) ↦ x.coeff i, fun (i : ℕ) ↦ y.coeff i]) :
                𝕄 →ₐ[ℤ] k) :
              (a : 𝕄) → k)
            (wittMul p (n + 1) + HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (0, n + 1) * X (1, n + 1)) :
          k)
        (HMul.hMul (β := k) (x.coeff (n + 1))
          (((aeval.{0, u_1, 0} (R := ℤ) (S₁ := k) (σ := Fin 2 × ℕ)
                    (Function.uncurry ![fun (i : ℕ) ↦ x.coeff i, fun (i : ℕ) ↦ y.coeff i]) :
                  𝕄 →ₐ[ℤ] k) :
                (a : 𝕄) → k)
              ((rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ (n + 1)) : 𝕄) :
            k)) -
      HMul.hMul (β := k) (y.coeff (n + 1))
        (((aeval.{0, u_1, 0} (R := ℤ) (S₁ := k) (σ := Fin 2 × ℕ)
                  (Function.uncurry ![fun (i : ℕ) ↦ x.coeff i, fun (i : ℕ) ↦ y.coeff i]) :
                𝕄 →ₐ[ℤ] k) :
              (a : 𝕄) → k)
            ((rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ (n + 1)) : 𝕄) :
          k) =
    (x * y).coeff (n + 1) + HPow.hPow (α := k) (↑p : k) (n + 1) * x.coeff (n + 1) * y.coeff (n + 1) -
        y.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), HPow.hPow (α := k) (↑p : k) i * x.coeff i ^ p ^ (n + 1 - i) -
      x.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), HPow.hPow (α := k) (↑p : k) i * y.coeff i ^ p ^ (n + 1 - i)
⊢ peval (polyOfInterest p n) ![fun (i : ℕ) ↦ x.coeff i, fun (i : ℕ) ↦ y.coeff i] =
    (x * y).coeff (n + 1) + HPow.hPow (α := k) (↑p : k) (n + 1) * x.coeff (n + 1) * y.coeff (n + 1) -
        y.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), HPow.hPow (α := k) (↑p : k) i * x.coeff i ^ p ^ (n + 1 - i) -
      x.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), HPow.hPow (α := k) (↑p : k) i * y.coeff i ^ p ^ (n + 1 - i)

Tactic:
simp only [polyOfInterest, peval,
    Function.uncurry_apply_pair, aeval_X, Matrix.cons_val_one, map_mul, Matrix.cons_val_zero,
    map_sub]

Premises used: MvPolynomial.aeval_X, map_sub, WittVector.peval, Matrix.cons_val_one, Matrix.cons_val_zero, map_mul, Function.uncurry_apply_pair, WittVector.polyOfInterest
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
n : ℕ
x y : 𝕎 k
rw :
  HSub.hSub (α := k)
        (((aeval.{0, u_1, 0} (R := ℤ) (S₁ := k) (σ := Fin 2 × ℕ)
                  (Function.uncurry ![fun (i : ℕ) ↦ x.coeff i, fun (i : ℕ) ↦ y.coeff i]) :
                𝕄 →ₐ[ℤ] k) :
              (a : 𝕄) → k)
            (wittMul p (n + 1) + HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (0, n + 1) * X (1, n + 1)) :
          k)
        (HMul.hMul (β := k) (y.coeff (n + 1))
          (((aeval.{0, u_1, 0} (R := ℤ) (S₁ := k) (σ := Fin 2 × ℕ)
                    (Function.uncurry ![fun (i : ℕ) ↦ x.coeff i, fun (i : ℕ) ↦ y.coeff i]) :
                  𝕄 →ₐ[ℤ] k) :
                (a : 𝕄) → k)
              ((rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ (n + 1)) : 𝕄) :
            k)) -
      HMul.hMul (β := k) (x.coeff (n + 1))
        (((aeval.{0, u_1, 0} (R := ℤ) (S₁ := k) (σ := Fin 2 × ℕ)
                  (Function.uncurry ![fun (i : ℕ) ↦ x.coeff i, fun (i : ℕ) ↦ y.coeff i]) :
                𝕄 →ₐ[ℤ] k) :
              (a : 𝕄) → k)
            ((rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ (n + 1)) : 𝕄) :
          k) =
    (x * y).coeff (n + 1) + HPow.hPow (α := k) (↑p : k) (n + 1) * x.coeff (n + 1) * y.coeff (n + 1) -
        y.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), HPow.hPow (α := k) (↑p : k) i * x.coeff i ^ p ^ (n + 1 - i) -
      x.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), HPow.hPow (α := k) (↑p : k) i * y.coeff i ^ p ^ (n + 1 - i)
⊢ HSub.hSub (α := k)
        (((aeval.{0, u_1, 0} (R := ℤ) (S₁ := k) (σ := Fin 2 × ℕ)
                  (Function.uncurry ![fun (i : ℕ) ↦ x.coeff i, fun (i : ℕ) ↦ y.coeff i]) :
                𝕄 →ₐ[ℤ] k) :
              (a : 𝕄) → k)
            (wittMul p (n + 1) + HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (0, n + 1) * X (1, n + 1)) :
          k)
        (HMul.hMul (β := k) (x.coeff (n + 1))
          (((aeval.{0, u_1, 0} (R := ℤ) (S₁ := k) (σ := Fin 2 × ℕ)
                    (Function.uncurry ![fun (i : ℕ) ↦ x.coeff i, fun (i : ℕ) ↦ y.coeff i]) :
                  𝕄 →ₐ[ℤ] k) :
                (a : 𝕄) → k)
              ((rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ (n + 1)) : 𝕄) :
            k)) -
      HMul.hMul (β := k) (y.coeff (n + 1))
        (((aeval.{0, u_1, 0} (R := ℤ) (S₁ := k) (σ := Fin 2 × ℕ)
                  (Function.uncurry ![fun (i : ℕ) ↦ x.coeff i, fun (i : ℕ) ↦ y.coeff i]) :
                𝕄 →ₐ[ℤ] k) :
              (a : 𝕄) → k)
            ((rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ (n + 1)) : 𝕄) :
          k) =
    (x * y).coeff (n + 1) + HPow.hPow (α := k) (↑p : k) (n + 1) * x.coeff (n + 1) * y.coeff (n + 1) -
        y.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), HPow.hPow (α := k) (↑p : k) i * x.coeff i ^ p ^ (n + 1 - i) -
      x.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), HPow.hPow (α := k) (↑p : k) i * y.coeff i ^ p ^ (n + 1 - i)

Tactic:
rw [sub_sub, add_comm (_ * _), ← sub_sub]

Premises used: HMul.hMul, add_comm, sub_sub
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
n : ℕ
x y : 𝕎 k
⊢ HSub.hSub (α := k)
        (((aeval.{0, u_1, 0} (R := ℤ) (S₁ := k) (σ := Fin 2 × ℕ)
                  (Function.uncurry ![fun (i : ℕ) ↦ x.coeff i, fun (i : ℕ) ↦ y.coeff i]) :
                𝕄 →ₐ[ℤ] k) :
              (a : 𝕄) → k)
            (wittMul p (n + 1) + HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * X (0, n + 1) * X (1, n + 1)) :
          k)
        (HMul.hMul (β := k) (y.coeff (n + 1))
          (((aeval.{0, u_1, 0} (R := ℤ) (S₁ := k) (σ := Fin 2 × ℕ)
                    (Function.uncurry ![fun (i : ℕ) ↦ x.coeff i, fun (i : ℕ) ↦ y.coeff i]) :
                  𝕄 →ₐ[ℤ] k) :
                (a : 𝕄) → k)
              ((rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ (n + 1)) : 𝕄) :
            k)) -
      HMul.hMul (β := k) (x.coeff (n + 1))
        (((aeval.{0, u_1, 0} (R := ℤ) (S₁ := k) (σ := Fin 2 × ℕ)
                  (Function.uncurry ![fun (i : ℕ) ↦ x.coeff i, fun (i : ℕ) ↦ y.coeff i]) :
                𝕄 →ₐ[ℤ] k) :
              (a : 𝕄) → k)
            ((rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ (n + 1)) : 𝕄) :
          k) =
    (x * y).coeff (n + 1) + HPow.hPow (α := k) (↑p : k) (n + 1) * x.coeff (n + 1) * y.coeff (n + 1) -
        y.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), HPow.hPow (α := k) (↑p : k) i * x.coeff i ^ p ^ (n + 1 - i) -
      x.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), HPow.hPow (α := k) (↑p : k) i * y.coeff i ^ p ^ (n + 1 - i)

Tactic:
simp [wittPolynomial_eq_sum_C_mul_X_pow, aeval, mul_coeff, peval, map_natCast,
    map_add, map_pow, map_mul]

Premises used: MvPolynomial.aeval, WittVector.peval, map_add, map_pow, WittVector.mul_coeff, map_mul, map_natCast, wittPolynomial_eq_sum_C_mul_X_pow
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
n : ℕ
x y : 𝕎 k
rw :
  (x * y).coeff (n + 1) + HPow.hPow (α := k) (↑p : k) (n + 1) * x.coeff (n + 1) * y.coeff (n + 1) -
        y.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), HPow.hPow (α := k) (↑p : k) i * x.coeff i ^ p ^ (n + 1 - i) -
      x.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), HPow.hPow (α := k) (↑p : k) i * y.coeff i ^ p ^ (n + 1 - i) =
    (x * y).coeff (n + 1) - y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) - x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1)
⊢ peval (polyOfInterest p n) ![fun (i : ℕ) ↦ x.coeff i, fun (i : ℕ) ↦ y.coeff i] =
    (x * y).coeff (n + 1) - y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) - x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1)

Tactic:
rw [peval_polyOfInterest]

Premises used: WittVector.peval_polyOfInterest
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
n : ℕ
x y : 𝕎 k
⊢ Eq.{u_1 + 1} (α := k) (↑p : k) 0

Tactic:
have : (p : k) = 0 := CharP.cast_eq_zero k p
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
n : ℕ
x y : 𝕎 k
this : Eq.{u_1 + 1} (α := k) (↑p : k) 0
simp :
  (x * y).coeff (n + 1) -
        y.coeff (n + 1) * ∑ x_1 ∈ range (n + 1 + 1), HPow.hPow (α := k) 0 x_1 * x.coeff x_1 ^ p ^ (n + 1 - x_1) -
      x.coeff (n + 1) * ∑ x ∈ range (n + 1 + 1), HPow.hPow (α := k) 0 x * y.coeff x ^ p ^ (n + 1 - x) =
    (x * y).coeff (n + 1) - y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) - x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1)
⊢ (x * y).coeff (n + 1) + HPow.hPow (α := k) (↑p : k) (n + 1) * x.coeff (n + 1) * y.coeff (n + 1) -
        y.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), HPow.hPow (α := k) (↑p : k) i * x.coeff i ^ p ^ (n + 1 - i) -
      x.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), HPow.hPow (α := k) (↑p : k) i * y.coeff i ^ p ^ (n + 1 - i) =
    (x * y).coeff (n + 1) - y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) - x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1)

Tactic:
simp only [this, ne_eq, add_eq_zero, and_false, zero_pow, zero_mul, add_zero,
    not_false_eq_true, reduceCtorEq]

Premises used: reduceCtorEq, MulZeroClass.zero_mul, ne_eq, and_false, add_eq_zero, add_zero, not_false_eq_true, zero_pow