-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 :
  HPow.hPow (α := ℚ) (↑p : ℚ) n *
      HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n =
    1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
rw :
  HPow.hPow (α := MvPolynomial ℕ ℚ) (X i) p ^ (p ^ (n - i) - (j + 1)) *
            (HPow.hPow (α := MvPolynomial ℕ ℚ)
                ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ)
                    (frobeniusPolyAux p i) :
                  MvPolynomial ℕ ℚ)
                (j + 1) *
              HPow.hPow (α := MvPolynomial ℕ ℚ) ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ)) (j + 1)) *
          (↑((p ^ (n - i)).choose (j + 1)) : MvPolynomial ℕ ℚ) *
        HPow.hPow (α := MvPolynomial ℕ ℚ) ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ)) i *
      HPow.hPow (α := MvPolynomial ℕ ℚ)
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _)) n =
    HMul.hMul (β := MvPolynomial ℕ ℚ)
        (HPow.hPow (α := MvPolynomial ℕ ℚ) (X i) p ^ (p ^ (n - i) - (j + 1)) *
          HPow.hPow (α := MvPolynomial ℕ ℚ)
            ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p i) :
              MvPolynomial ℕ ℚ)
            (j + 1))
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ)
            ((Int.castRingHom ℚ : (a : ℤ) → ℚ)
              (↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1))) : ℤ)) :
          MvPolynomial ℕ ℚ) *
      (C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ)
⊢ HPow.hPow (α := MvPolynomial ℕ ℚ) ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ)) i *
        (HPow.hPow (α := MvPolynomial ℕ ℚ) ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ)) (j + 1) *
              HPow.hPow (α := MvPolynomial ℕ ℚ)
                ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ)
                    (frobeniusPolyAux p i) :
                  MvPolynomial ℕ ℚ)
                (j + 1) *
            HPow.hPow (α := MvPolynomial ℕ ℚ) (X i) p ^ (p ^ (n - i) - (j + 1)) *
          (↑((p ^ (n - i)).choose (j + 1)) : MvPolynomial ℕ ℚ)) *
      HPow.hPow (α := MvPolynomial ℕ ℚ)
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _)) n =
    (C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) *
      HMul.hMul (β := MvPolynomial ℕ ℚ)
        (HPow.hPow (α := MvPolynomial ℕ ℚ) (X i) p ^ (p ^ (n - i) - (j + 1)) *
          HPow.hPow (α := MvPolynomial ℕ ℚ)
            ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p i) :
              MvPolynomial ℕ ℚ)
            (j + 1))
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ)
            ((Int.castRingHom ℚ : (a : ℤ) → ℚ)
              (↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1))) : ℤ)) :
          MvPolynomial ℕ ℚ)

Tactic:
rw [mul_comm (C (p : ℚ) ^ i), mul_comm _ ((X i ^ p) ^ _), mul_comm (C (p : ℚ) ^ (j + 1)),
    mul_comm (C (p : ℚ))]

Premises used: MvPolynomial.X, Nat.cast, HPow.hPow, HAdd.hAdd, mul_comm, OfNat.ofNat, MvPolynomial.C, DFunLike.coe