-- 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),
          (rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄)
            ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ)
              (HPow.hPow (α := ℤ) (↑p : ℤ) x)))
        (∑ 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) *
          ∑ 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)))) =
    remainder p n +
      (-(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))))))
have apply : 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: apply congrArg (Add.add _)