-- Mathlib/RingTheory/WittVector/MulCoeff.lean
theorem mul_polyOfInterest_aux3 (p n : ℕ) : wittPolyProd p (n + 1) =
    -((p : 𝕄) ^ (n + 1) * X (0, n + 1)) * ((p : 𝕄) ^ (n + 1) * X (1, n + 1)) +
    (p : 𝕄) ^ (n + 1) * X (0, n + 1) * rename (Prod.mk (1 : Fin 2)) (wittPolynomial p ℤ (n + 1)) +
    (p : 𝕄) ^ (n + 1) * X (1, n + 1) * rename (Prod.mk (0 : Fin 2)) (wittPolynomial p ℤ (n + 1)) +
    remainder p n

Proof state:
p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
⊢ (∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) *
          ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
        ↑p ^ (n + 1) * X (0, n + 1) *
          ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
      ((∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) *
          (↑p ^ (n + 1) * X (1, n + 1)) +
        ↑p ^ (n + 1) * X (0, n + 1) * (↑p ^ (n + 1) * X (1, n + 1))) =
    remainder p n +
      (-(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
          (↑p ^ (n + 1) * X (0, n + 1) *
              ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
            ↑p ^ (n + 1) * X (0, n + 1) * (↑p ^ (n + 1) * X (1, n + 1))) +
        (↑p ^ (n + 1) * X (1, n + 1) *
            ∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
          ↑p ^ (n + 1) * X (1, n + 1) * (↑p ^ (n + 1) * X (0, n + 1))))

Tactic:
simp only [add_assoc]

Result:
p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
⊢ (∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) *
        ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
      (↑p ^ (n + 1) * X (0, n + 1) *
          ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
        ((∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) *
            (↑p ^ (n + 1) * X (1, n + 1)) +
          ↑p ^ (n + 1) * X (0, n + 1) * (↑p ^ (n + 1) * X (1, n + 1)))) =
    remainder p n +
      (-(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
        (↑p ^ (n + 1) * X (0, n + 1) *
            ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
          (↑p ^ (n + 1) * X (0, n + 1) * (↑p ^ (n + 1) * X (1, n + 1)) +
            (↑p ^ (n + 1) * X (1, n + 1) *
                ∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
              ↑p ^ (n + 1) * X (1, n + 1) * (↑p ^ (n + 1) * X (0, n + 1))))))

Proof state:
p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
⊢ (∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) *
          ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
        ↑p ^ (n + 1) * X (0, n + 1) *
          ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
      ((∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) *
          (↑p ^ (n + 1) * X (1, n + 1)) +
        ↑p ^ (n + 1) * X (0, n + 1) * (↑p ^ (n + 1) * X (1, n + 1))) =
    -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
          (↑p ^ (n + 1) * X (0, n + 1) *
              ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
            ↑p ^ (n + 1) * X (0, n + 1) * (↑p ^ (n + 1) * X (1, n + 1))) +
        (↑p ^ (n + 1) * X (1, n + 1) *
            ∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
          ↑p ^ (n + 1) * X (1, n + 1) * (↑p ^ (n + 1) * X (0, n + 1))) +
      remainder p n

Tactic:
rw [add_comm _ (remainder p n)]

Result:
p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
⊢ (∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) *
          ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
        ↑p ^ (n + 1) * X (0, n + 1) *
          ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
      ((∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) *
          (↑p ^ (n + 1) * X (1, n + 1)) +
        ↑p ^ (n + 1) * X (0, n + 1) * (↑p ^ (n + 1) * X (1, n + 1))) =
    remainder p n +
      (-(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
          (↑p ^ (n + 1) * X (0, n + 1) *
              ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
            ↑p ^ (n + 1) * X (0, n + 1) * (↑p ^ (n + 1) * X (1, n + 1))) +
        (↑p ^ (n + 1) * X (1, n + 1) *
            ∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
          ↑p ^ (n + 1) * X (1, n + 1) * (↑p ^ (n + 1) * X (0, n + 1))))

Proof state:
p n : ℕ
⊢ wittPolyProd p (n + 1) =
    -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
          ↑p ^ (n + 1) * X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) +
        ↑p ^ (n + 1) * X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)) +
      remainder p n

Tactic:
have mvpz : (p : 𝕄) ^ (n + 1) = MvPolynomial.C ((p : ℤ) ^ (n + 1)) := by norm_cast

Result:
p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
⊢ wittPolyProd p (n + 1) =
    -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
          ↑p ^ (n + 1) * X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) +
        ↑p ^ (n + 1) * X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)) +
      remainder p n

Proof state:
p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
⊢ ↑p ^ (n + 1) * X (0, n + 1) *
        ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
      ((∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) *
          (↑p ^ (n + 1) * X (1, n + 1)) +
        ↑p ^ (n + 1) * X (0, n + 1) * (↑p ^ (n + 1) * X (1, n + 1))) =
    -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
      (↑p ^ (n + 1) * X (0, n + 1) *
          ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
        (↑p ^ (n + 1) * X (0, n + 1) * (↑p ^ (n + 1) * X (1, n + 1)) +
          (↑p ^ (n + 1) * X (1, n + 1) *
              ∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
            ↑p ^ (n + 1) * X (1, n + 1) * (↑p ^ (n + 1) * X (0, n + 1)))))

Tactic:
ring

Result:
no goals