awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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),
    (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: enter [1, 1, 2, 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),
          (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
have conv_rhs : (∑ 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),
              (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 (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_rhs =>
    enter [1, 1, 2, 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),
              (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 (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 0) : (a : MvPolynomial ℕ ℤ) → 𝕄)
    ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) x))
Tactic: enter [1, 2, 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))
| -(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 (1, n + 1)) +
      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),
    (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: enter [1, 2, 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),
          (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),
                (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 (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_rhs : (∑ 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),
              (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 (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 (0, n + 1)) +
    remainder p n
Tactic: conv_rhs =>
    enter [1, 2, 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 : ℕ
hp : Fact (Nat.Prime 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))
have 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
Tactic: rw [← add_sub_assoc, eq_sub_iff_add_eq, mul_polyOfInterest_aux2]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * polyOfInterest p n = remainder p n - wittPolyProdRemainder p (n + 1)
have 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)))
Tactic: simp only [polyOfInterest, mul_sub, mul_add, sub_eq_iff_eq_add']
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ 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)))
have 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)))
Tactic: rw [mul_polyOfInterest_aux4 p n]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) * polyOfInterest p n).vars ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
have rw : (remainder p n - wittPolyProdRemainder p (n + 1)).vars ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
Tactic: rw [mul_polyOfInterest_aux5]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (remainder p n - wittPolyProdRemainder p (n + 1)).vars ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
have apply : (remainder p n).vars ∪ (wittPolyProdRemainder p (n + 1)).vars ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
Tactic: apply Subset.trans (vars_sub_subset _)
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
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))
have refine_1 : (remainder p n).vars ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
Tactic: refine union_subset ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
refine_1 : (remainder p n).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))
have refine_2 : (wittPolyProdRemainder p (n + 1)).vars ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
Tactic: refine union_subset ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime 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 : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (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
have this : HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) = (C : (a : ℤ) → 𝕄) (HPow.hPow (α := ℤ) (↑p : ℤ) (n + 1))
Tactic: have : (p : 𝕄) ^ (n + 1) = C ((p : ℤ) ^ (n + 1)) := by norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
this : HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) = (C : (a : ℤ) → 𝕄) (HPow.hPow (α := ℤ) (↑p : ℤ) (n + 1))
⊢ (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
have ha : HPow.hPow (α := ℤ) (↑p : ℤ) (n + 1) ≠ 0
Tactic: rw [polyOfInterest, this, vars_C_mul]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
this : HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) = (C : (a : ℤ) → 𝕄) (HPow.hPow (α := ℤ) (↑p : ℤ) (n + 1))
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) (n + 1) ≠ 0
have ha : 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 : ℕ
⊢ (polyOfInterest p n).vars ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
have 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))
Tactic: rw [polyOfInterest_vars_eq]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
n : ℕ
x y : 𝕎 k
⊢ 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)
have 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)
Tactic: simp only [polyOfInterest, peval,
    Function.uncurry_apply_pair, aeval_X, Matrix.cons_val_one, map_mul, Matrix.cons_val_zero,
    map_sub]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
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) (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)
have 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)
Tactic: rw [sub_sub, add_comm (_ * _), ← sub_sub]