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