-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) (↑p : R)
n : ℕ
rw :
  HMul.hMul (β := MvPolynomial ℕ R)
      (HMul.hMul (β := MvPolynomial ℕ R)
        (HSub.hSub (α := MvPolynomial ℕ R) (X n)
          (∑ i ∈ range n,
            HMul.hMul (α := MvPolynomial ℕ R)
              ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
              (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R i) (p ^ (n - i)))))
        ((C : (a : R) → MvPolynomial ℕ R)
            (HPow.hPow (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) n) :
          MvPolynomial ℕ R))
      ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) n) : MvPolynomial ℕ R) =
    HSub.hSub (α := MvPolynomial ℕ R) (X n)
      (∑ i ∈ range n,
        HMul.hMul (α := MvPolynomial ℕ R)
          ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
          (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R i) (p ^ (n - i))))
rw₁ :
  HSub.hSub (α := MvPolynomial ℕ R) (X n)
        (∑ i ∈ range n,
          HMul.hMul (α := MvPolynomial ℕ R)
            ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
            (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R i) (p ^ (n - i)))) *
      HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R)
        ((C : (a : R) → MvPolynomial ℕ R)
            (HPow.hPow (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) n) :
          MvPolynomial ℕ R)
        ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) n) : MvPolynomial ℕ R) =
    HSub.hSub (α := MvPolynomial ℕ R) (X n)
      (∑ i ∈ range n,
        HMul.hMul (α := MvPolynomial ℕ R)
          ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
          (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R i) (p ^ (n - i))))
rw₂ :
  HMul.hMul (β := MvPolynomial ℕ R)
      (HSub.hSub (α := MvPolynomial ℕ R) (X n)
        (∑ i ∈ range n,
          HMul.hMul (α := MvPolynomial ℕ R)
            ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
            (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R i) (p ^ (n - i)))))
      ((C : (a : R) → MvPolynomial ℕ R)
          (HPow.hPow (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) n *
            HPow.hPow (α := R) (↑p : R) n) :
        MvPolynomial ℕ R) =
    HSub.hSub (α := MvPolynomial ℕ R) (X n)
      (∑ i ∈ range n,
        HMul.hMul (α := MvPolynomial ℕ R)
          ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
          (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R i) (p ^ (n - i))))
rw₃ :
  HMul.hMul (β := MvPolynomial ℕ R)
      (HSub.hSub (α := MvPolynomial ℕ R) (X n)
        (∑ i ∈ range n,
          HMul.hMul (α := MvPolynomial ℕ R)
            ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
            (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R i) (p ^ (n - i)))))
      ((C : (a : R) → MvPolynomial ℕ R)
          (HMul.hMul (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) (↑p : R) ^ n) :
        MvPolynomial ℕ R) =
    HSub.hSub (α := MvPolynomial ℕ R) (X n)
      (∑ i ∈ range n,
        HMul.hMul (α := MvPolynomial ℕ R)
          ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
          (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R i) (p ^ (n - i))))
rw₄ :
  HMul.hMul (β := MvPolynomial ℕ R)
      (HSub.hSub (α := MvPolynomial ℕ R) (X n)
        (∑ i ∈ range n,
          HMul.hMul (α := MvPolynomial ℕ R)
            ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
            (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R i) (p ^ (n - i)))))
      ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) 1 n) : MvPolynomial ℕ R) =
    HSub.hSub (α := MvPolynomial ℕ R) (X n)
      (∑ i ∈ range n,
        HMul.hMul (α := MvPolynomial ℕ R)
          ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
          (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R i) (p ^ (n - i))))
rw₅ :
  HSub.hSub (α := MvPolynomial ℕ R) (X n)
        (∑ i ∈ range n,
          HMul.hMul (α := MvPolynomial ℕ R)
            ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
            (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R i) (p ^ (n - i)))) *
      (C : (a : R) → MvPolynomial ℕ R) 1 =
    HSub.hSub (α := MvPolynomial ℕ R) (X n)
      (∑ i ∈ range n,
        HMul.hMul (α := MvPolynomial ℕ R)
          ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
          (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R i) (p ^ (n - i))))
rw₆ :
  HSub.hSub (α := MvPolynomial ℕ R) (X n)
        (∑ i ∈ range n,
          HMul.hMul (α := MvPolynomial ℕ R)
            ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
            (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R i) (p ^ (n - i)))) *
      1 =
    HSub.hSub (α := MvPolynomial ℕ R) (X n)
      (∑ i ∈ range n,
        HMul.hMul (α := MvPolynomial ℕ R)
          ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
          (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R i) (p ^ (n - i))))
rw₇ rw₈ :
  HSub.hSub (α := MvPolynomial ℕ R) (X n)
      (∑ i ∈ range n,
        HMul.hMul (α := MvPolynomial ℕ R)
          ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
          (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R i) (p ^ (n - i)))) =
    HSub.hSub (α := MvPolynomial ℕ R) (X n)
      (∑ i ∈ range n,
        HMul.hMul (α := MvPolynomial ℕ R)
          ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
          (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R i) (p ^ (n - i))))
⊢ HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R) (xInTermsOfW p R n)
      ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) n) : MvPolynomial ℕ R) =
    HSub.hSub (α := MvPolynomial ℕ R) (X n)
      (∑ i ∈ range n,
        HMul.hMul (α := MvPolynomial ℕ R)
          ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
          (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R i) (p ^ (n - i))))

Tactic:
rw [xInTermsOfW_eq, mul_assoc, ← C_mul, ← mul_pow, invOf_mul_self,
    one_pow, C_1, mul_one]

Premises used: one_pow, mul_assoc, xInTermsOfW_eq, MvPolynomial.C_1, invOf_mul_self, MvPolynomial.C_mul, mul_one, mul_pow