awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n i : ℕ
m : Fin 2 × ℕ →₀ ℕ
hsupp : Finsupp.support (Finsupp.single i (p ^ (n - i))) = {i}
⊢ 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:
simp only [bind₁_monomial, hsupp, Int.cast_natCast, prod_singleton, eq_intCast,
      Finsupp.single_eq_same, Int.cast_pow]

Premises used: Int.cast_natCast, Finsupp.single_eq_same, Finset.prod_singleton, Int.cast_pow, eq_intCast, MvPolynomial.bind₁_monomial
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ 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:
simp only [map_mul, bind₁_X_right]

Premises used: map_mul, MvPolynomial.bind₁_X_right
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∑ i ∈ range (n + 1), HPow.hPow (α := 𝕄) (↑p : 𝕄) i * wittMul p i ^ p ^ (n - i) = wittPolyProd p n

Tactic:
mul_polyOfInterest_aux1 p n

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

Tactic:
convert! mul_polyOfInterest_aux1 p n

Premises used: WittVector.mul_polyOfInterest_aux1
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
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
⊢ 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:
rw [sum_range_succ, add_comm, Nat.sub_self, pow_zero, pow_one]

Premises used: add_comm, pow_zero, Nat.sub_self, pow_one, Finset.sum_range_succ
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ 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:
rfl
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
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 n : ℕ
⊢ 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
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p n : ℕ
mvpz : HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) = (C : (a : ℤ) → 𝕄) (HPow.hPow (α := ℤ) (↑p : ℤ) (n + 1))
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
⊢ 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 [wittPolyProd, wittPolynomial, map_sum, map_sum]

Premises used: wittPolynomial, map_sum, WittVector.wittPolyProd
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p n : ℕ
mvpz : HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) = (C : (a : ℤ) → 𝕄) (HPow.hPow (α := ℤ) (↑p : ℤ) (n + 1))
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))
| 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)))

Tactic:
arg 1
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p n : ℕ
mvpz : HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) = (C : (a : ℤ) → 𝕄) (HPow.hPow (α := ℤ) (↑p : ℤ) (n + 1))
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)
| ∑ 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:
rw [sum_range_succ, ← C_mul_X_pow_eq_monomial, tsub_self, pow_zero, pow_one, map_mul,
      rename_C, rename_X, ← mvpz]

Premises used: tsub_self, pow_zero, map_mul, pow_one, MvPolynomial.rename_C, MvPolynomial.C_mul_X_pow_eq_monomial, MvPolynomial.rename_X, Finset.sum_range_succ
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p n : ℕ
mvpz : HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) = (C : (a : ℤ) → 𝕄) (HPow.hPow (α := ℤ) (↑p : ℤ) (n + 1))
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)
| 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)))

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]

Premises used: tsub_self, pow_zero, map_mul, pow_one, MvPolynomial.rename_C, MvPolynomial.C_mul_X_pow_eq_monomial, MvPolynomial.rename_X, Finset.sum_range_succ
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p n : ℕ
mvpz : HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) = (C : (a : ℤ) → 𝕄) (HPow.hPow (α := ℤ) (↑p : ℤ) (n + 1))
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
⊢ 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:
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]

Premises used: tsub_self, pow_zero, map_mul, pow_one, MvPolynomial.rename_C, MvPolynomial.C_mul_X_pow_eq_monomial, MvPolynomial.rename_X, Finset.sum_range_succ
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p n : ℕ
mvpz : HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) = (C : (a : ℤ) → 𝕄) (HPow.hPow (α := ℤ) (↑p : ℤ) (n + 1))
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))
| (∑ 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))

Tactic:
arg 2
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p n : ℕ
mvpz : HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) = (C : (a : ℤ) → 𝕄) (HPow.hPow (α := ℤ) (↑p : ℤ) (n + 1))
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)
| ∑ 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:
rw [sum_range_succ, ← C_mul_X_pow_eq_monomial, tsub_self, pow_zero, pow_one, map_mul,
      rename_C, rename_X, ← mvpz]

Premises used: tsub_self, pow_zero, map_mul, pow_one, MvPolynomial.rename_C, MvPolynomial.C_mul_X_pow_eq_monomial, MvPolynomial.rename_X, Finset.sum_range_succ
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p n : ℕ
mvpz : HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) = (C : (a : ℤ) → 𝕄) (HPow.hPow (α := ℤ) (↑p : ℤ) (n + 1))
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)
| (∑ 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))

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]

Premises used: tsub_self, pow_zero, map_mul, pow_one, MvPolynomial.rename_C, MvPolynomial.C_mul_X_pow_eq_monomial, MvPolynomial.rename_X, Finset.sum_range_succ
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p n : ℕ
mvpz : HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) = (C : (a : ℤ) → 𝕄) (HPow.hPow (α := ℤ) (↑p : ℤ) (n + 1))
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
⊢ (∑ 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 2
    rw [sum_range_succ, ← C_mul_X_pow_eq_monomial, tsub_self, pow_zero, pow_one, map_mul,
      rename_C, rename_X, ← mvpz]

Premises used: tsub_self, pow_zero, map_mul, pow_one, MvPolynomial.rename_C, MvPolynomial.C_mul_X_pow_eq_monomial, MvPolynomial.rename_X, Finset.sum_range_succ
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p n : ℕ
mvpz : HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) = (C : (a : ℤ) → 𝕄) (HPow.hPow (α := ℤ) (↑p : ℤ) (n + 1))
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))
| -(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:
enter [1, 1, 2, 2]
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p n : ℕ
mvpz : HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) = (C : (a : ℤ) → 𝕄) (HPow.hPow (α := ℤ) (↑p : ℤ) (n + 1))
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)
| -(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:
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]

Premises used: tsub_self, pow_zero, map_mul, pow_one, MvPolynomial.rename_C, MvPolynomial.C_mul_X_pow_eq_monomial, MvPolynomial.rename_X, Finset.sum_range_succ
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p n : ℕ
mvpz : HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) = (C : (a : ℤ) → 𝕄) (HPow.hPow (α := ℤ) (↑p : ℤ) (n + 1))
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))
| -(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:
enter [1, 2, 2]
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p n : ℕ
mvpz : HPow.hPow (α := 𝕄) (↑p : 𝕄) (n + 1) = (C : (a : ℤ) → 𝕄) (HPow.hPow (α := ℤ) (↑p : ℤ) (n + 1))
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)
| -(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:
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]

Premises used: tsub_self, pow_zero, map_mul, pow_one, MvPolynomial.rename_C, MvPolynomial.C_mul_X_pow_eq_monomial, MvPolynomial.rename_X, Finset.sum_range_succ