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

Tactic:
apply sum_congr rfl

Premises used: Finset.sum_congr, rfl