-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) (↑p : R)
n : ℕ
H :
  ∀ m < n,
    Eq (α := MvPolynomial ℕ R)
      ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R m) : MvPolynomial ℕ R)
      (X m : MvPolynomial ℕ R)
i : ℕ
h : i < n
ind :
  HMul.hMul (α := MvPolynomial ℕ R)
      ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
      (HPow.hPow (α := MvPolynomial ℕ R) (X i) (p ^ (n - i))) =
    HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R)
      ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R)
          ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i)) :
        MvPolynomial ℕ R)
      ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R)
          (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R i) (p ^ (n - i))) :
        MvPolynomial ℕ R)
ind₁ :
  HMul.hMul (α := MvPolynomial ℕ R)
      ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
      (HPow.hPow (α := MvPolynomial ℕ R) (X i) (p ^ (n - i))) =
    HMul.hMul (α := MvPolynomial ℕ R)
      ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R)
          ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i)) :
        MvPolynomial ℕ R)
      (HPow.hPow (α := MvPolynomial ℕ R)
        ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R i) : MvPolynomial ℕ R)
        (p ^ (n - i)))
ind₂ :
  HMul.hMul (α := MvPolynomial ℕ R)
      ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
      (HPow.hPow (α := MvPolynomial ℕ R) (X i) (p ^ (n - i))) =
    HMul.hMul (α := MvPolynomial ℕ R)
      ((algebraMap R (MvPolynomial ℕ R) : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) :
        MvPolynomial ℕ R)
      (HPow.hPow (α := MvPolynomial ℕ R)
        ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R i) : MvPolynomial ℕ R)
        (p ^ (n - i)))
ind₃ :
  HMul.hMul (α := MvPolynomial ℕ R)
      ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
      (HPow.hPow (α := MvPolynomial ℕ R) (X i) (p ^ (n - i))) =
    HMul.hMul (α := MvPolynomial ℕ R)
      ((algebraMap R (MvPolynomial ℕ R) : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) :
        MvPolynomial ℕ R)
      (HPow.hPow (α := MvPolynomial ℕ R) (X i) (p ^ (n - i)))
ind₄ ind₅ :
  HMul.hMul (α := MvPolynomial ℕ R)
      ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
      (HPow.hPow (α := MvPolynomial ℕ R) (X i) (p ^ (n - i))) =
    HMul.hMul (α := MvPolynomial ℕ R)
      ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
      (HPow.hPow (α := MvPolynomial ℕ R) (X i) (p ^ (n - i)))
⊢ HMul.hMul (α := MvPolynomial ℕ R)
      ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
      (HPow.hPow (α := MvPolynomial ℕ R) (X i) (p ^ (n - i))) =
    (bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R)
      (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 [map_mul, map_pow (bind₁ _), algHom_C, H i h, algebraMap_eq]

Premises used: map_pow, MvPolynomial.algHom_C, MvPolynomial.bind₁, map_mul, MvPolynomial.algebraMap_eq