-- 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
rw :
  Eq (α := MvPolynomial ℕ ℚ)
    (∑ i_1 ∈ range (p ^ (n - i)),
      HMul.hMul (β := MvPolynomial ℕ ℚ)
        (HMul.hMul (α := MvPolynomial ℕ ℚ)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
          (HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
                  ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
                  ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ)
                      (frobeniusPolyAux p i) :
                    MvPolynomial ℕ ℚ) ^
                (i_1 + 1) *
              HPow.hPow (α := MvPolynomial ℕ ℚ) (X i) p ^ (p ^ (n - i) - (i_1 + 1)) *
            (↑((p ^ (n - i)).choose (i_1 + 1)) : MvPolynomial ℕ ℚ)))
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ)
            (HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n) :
          MvPolynomial ℕ ℚ))
    (∑ i_1 ∈ range (p ^ (n - i)),
      HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
        ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ)
            (HPow.hPow (α := MvPolynomial ℕ ℤ) (X i) p ^ (p ^ (n - i) - (i_1 + 1)) * frobeniusPolyAux p i ^ (i_1 + 1) *
              (C : (a : ℤ) → MvPolynomial ℕ ℤ)
                (↑((p ^ (n - i)).choose (i_1 + 1) / p ^ (n - i - v p (i_1 + 1)) * p ^ (i_1 - v p (i_1 + 1))) : ℤ)) :
          MvPolynomial ℕ ℚ))
⊢ HMul.hMul (β := MvPolynomial ℕ ℚ)
        (HMul.hMul (α := MvPolynomial ℕ ℚ)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
          ((HPow.hPow (α := MvPolynomial ℕ ℚ) (X i) p +
              HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
                ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
                ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ)
                    (frobeniusPolyAux p i) :
                  MvPolynomial ℕ ℚ)) ^
            p ^ (n - i)))
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ)
            (HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n) :
          MvPolynomial ℕ ℚ) -
      HMul.hMul (β := MvPolynomial ℕ ℚ)
        (HMul.hMul (α := MvPolynomial ℕ ℚ)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
          (HPow.hPow (α := MvPolynomial ℕ ℚ) (X i) (p ^ (n + 1 - i))))
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ)
            (HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n) :
          MvPolynomial ℕ ℚ) =
    ∑ i_1 ∈ range (p ^ (n - i)),
      HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
        ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ)
            (HPow.hPow (α := MvPolynomial ℕ ℤ) (X i) p ^ (p ^ (n - i) - (i_1 + 1)) * frobeniusPolyAux p i ^ (i_1 + 1) *
              (C : (a : ℤ) → MvPolynomial ℕ ℤ)
                (↑((p ^ (n - i)).choose (i_1 + 1) / p ^ (n - i - v p (i_1 + 1)) * p ^ (i_1 - v p (i_1 + 1))) : ℤ)) :
          MvPolynomial ℕ ℚ)

Tactic:
rw [add_comm (X i ^ p), add_pow, sum_range_succ', pow_zero, tsub_zero, Nat.choose_zero_right,
    one_mul, Nat.cast_one, mul_one, mul_add, add_mul, Nat.succ_sub (le_of_lt hi),
    Nat.succ_eq_add_one (n - i), pow_succ', pow_mul, add_sub_cancel_right, mul_sum, sum_mul]

Premises used: add_mul, Finset.mul_sum, Nat.succ_eq_add_one, HSub.hSub, MvPolynomial.X, le_of_lt, add_comm, pow_mul, pow_zero, tsub_zero, HPow.hPow, Nat.succ_sub, add_pow, mul_add, add_sub_cancel_right, mul_one, Nat.cast_one, Finset.sum_range_succ', Nat.choose_zero_right, pow_succ', one_mul, Finset.sum_mul