-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    HPow.hPow (α := MvPolynomial ℕ ℚ) (X m) p +
        HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
          ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p m) :
            MvPolynomial ℕ ℚ) =
      (bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ m)
h1 :
  HPow.hPow (α := ℚ) (↑p : ℚ) n *
      HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n =
    1
rw :
  HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
        (∑ x ∈ range n,
            HMul.hMul (α := MvPolynomial ℕ ℚ)
              ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) x) : MvPolynomial ℕ ℚ)
              (HPow.hPow (α := MvPolynomial ℕ ℚ)
                ((bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ)
                    (xInTermsOfW p ℚ x) :
                  MvPolynomial ℕ ℚ)
                (p ^ (n - x))) :
          MvPolynomial ℕ ℚ)
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ)
            (HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n) :
          MvPolynomial ℕ ℚ) -
      HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
        (∑ x ∈ range n,
            HMul.hMul (α := MvPolynomial ℕ ℚ)
              ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) x) : MvPolynomial ℕ ℚ)
              (HPow.hPow (α := MvPolynomial ℕ ℚ) (X x) (p ^ (n + 1 - x))) :
          MvPolynomial ℕ ℚ)
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ)
            (HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n) :
          MvPolynomial ℕ ℚ) =
    HMul.hMul (α := MvPolynomial ℕ ℚ) ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ))
      ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ)
        (∑ i ∈ range n,
          ∑ j ∈ range (p ^ (n - i)),
            HPow.hPow (α := MvPolynomial ℕ ℤ) (X i) p ^ (p ^ (n - i) - (j + 1)) * frobeniusPolyAux p i ^ (j + 1) *
              (C : (a : ℤ) → MvPolynomial ℕ ℤ)
                (↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1))) : ℤ)))
⊢ HPow.hPow (α := MvPolynomial ℕ ℚ) (X n) p +
      HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
        ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p n) :
          MvPolynomial ℕ ℚ) =
    HMul.hMul (β := MvPolynomial ℕ ℚ)
      (HSub.hSub (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
        ((bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (X n) :
          MvPolynomial ℕ ℚ)
        (∑ x ∈ range n,
            HMul.hMul (α := MvPolynomial ℕ ℚ)
              ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) x) : MvPolynomial ℕ ℚ)
              (HPow.hPow (α := MvPolynomial ℕ ℚ)
                ((bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ)
                    (xInTermsOfW p ℚ x) :
                  MvPolynomial ℕ ℚ)
                (p ^ (n - x))) :
          MvPolynomial ℕ ℚ))
      ((C : (a : ℚ) → MvPolynomial ℕ ℚ)
          (HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n) :
        MvPolynomial ℕ ℚ)

Tactic:
rw [bind₁_X_right, Function.comp_apply, wittPolynomial_eq_sum_C_mul_X_pow, sum_range_succ,
    sum_range_succ, tsub_self, add_tsub_cancel_left, pow_zero, pow_one, pow_one, sub_mul, add_mul,
    add_mul, mul_right_comm, mul_right_comm (C ((p : ℚ) ^ (n + 1))), ← C_mul, ← C_mul, pow_succ',
    mul_assoc (p : ℚ) ((p : ℚ) ^ n), h1, mul_one, C_1, one_mul, add_comm _ (X n ^ p), add_assoc,
    ← add_sub, add_right_inj, frobeniusPolyAux_eq, map_sub, map_X, mul_sub, sub_eq_add_neg,
    add_comm _ (C (p : ℚ) * X (n + 1)), ← add_sub,
    add_right_inj, neg_eq_iff_eq_neg, neg_sub, eq_comm]

Premises used: add_mul, neg_sub, HMul.hMul, map_sub, mul_sub, add_assoc, add_sub, mul_assoc, tsub_self, sub_eq_add_neg, MvPolynomial.X, MvPolynomial.C_1, add_tsub_cancel_left, neg_eq_iff_eq_neg, eq_comm, Nat.cast, add_comm, pow_zero, sub_mul, WittVector.frobeniusPolyAux_eq, HPow.hPow, HAdd.hAdd, mul_right_comm, pow_one, MvPolynomial.C_mul, Function.comp_apply, mul_one, MvPolynomial.bind₁_X_right, OfNat.ofNat, MvPolynomial.C, DFunLike.coe, add_right_inj, Finset.sum_range_succ, MvPolynomial.map_X, pow_succ', wittPolynomial_eq_sum_C_mul_X_pow, one_mul