-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ m < n,
    Eq (α := MvPolynomial (idx × ℕ) ℚ)
      ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (wittStructureInt p Φ m) :
        MvPolynomial (idx × ℕ) ℚ)
      (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) m :
        MvPolynomial (idx × ℕ) ℚ)
c : idx × ℕ →₀ ℕ
sum_induction_steps :
  Eq.{u_2 + 1} (α := MvPolynomial (idx × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ)
        (∑ i ∈ Finset.range n,
          HMul.hMul (α := MvPolynomial (idx × ℕ) ℤ)
            ((C : (a : ℤ) → MvPolynomial (idx × ℕ) ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) i) : MvPolynomial (idx × ℕ) ℤ)
            (wittStructureInt p Φ i ^ p ^ (n - i))) :
      MvPolynomial (idx × ℕ) ℚ)
    (∑ i ∈ Finset.range n,
        HMul.hMul (α := MvPolynomial (idx × ℕ) ℚ)
          ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial (idx × ℕ) ℚ)
          (HPow.hPow (α := MvPolynomial (idx × ℕ) ℚ)
            (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) i)
            (p ^ (n - i))) :
      MvPolynomial (idx × ℕ) ℚ)
h :
  (↑(HDiv.hDiv (α := ℚ) (β := ℚ)
            ((Int.castRingHom ℚ : (a : ℤ) → ℚ)
                (coeff c
                  (HSub.hSub (α := MvPolynomial (idx × ℕ) ℤ) (β := MvPolynomial (idx × ℕ) ℤ)
                    ((bind₁ fun (i : idx) ↦
                            (rename fun (i_1 : ℕ) ↦ (i, i_1) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ)
                              (W_ ℤ n) :
                          (a : MvPolynomial idx ℤ) → MvPolynomial (idx × ℕ) ℤ)
                        Φ :
                      MvPolynomial (idx × ℕ) ℤ)
                    (∑ i ∈ Finset.range n,
                        HMul.hMul (α := MvPolynomial (idx × ℕ) ℤ)
                          ((C : (a : ℤ) → MvPolynomial (idx × ℕ) ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) i) :
                            MvPolynomial (idx × ℕ) ℤ)
                          (wittStructureInt p Φ i ^ p ^ (n - i)) :
                      MvPolynomial (idx × ℕ) ℤ))) :
              ℚ)
            ((↑(↑(p ^ n) : ℤ) : ℚ) : ℚ)).num :
      ℚ) =
    HDiv.hDiv (α := ℚ) (β := ℚ)
      ((Int.castRingHom ℚ : (a : ℤ) → ℚ)
          (coeff c
            (HSub.hSub (α := MvPolynomial (idx × ℕ) ℤ) (β := MvPolynomial (idx × ℕ) ℤ)
              ((bind₁ fun (i : idx) ↦
                      (rename fun (i_1 : ℕ) ↦ (i, i_1) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (W_ ℤ n) :
                    (a : MvPolynomial idx ℤ) → MvPolynomial (idx × ℕ) ℤ)
                  Φ :
                MvPolynomial (idx × ℕ) ℤ)
              (∑ i ∈ Finset.range n,
                  HMul.hMul (α := MvPolynomial (idx × ℕ) ℤ)
                    ((C : (a : ℤ) → MvPolynomial (idx × ℕ) ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) i) :
                      MvPolynomial (idx × ℕ) ℤ)
                    (wittStructureInt p Φ i ^ p ^ (n - i)) :
                MvPolynomial (idx × ℕ) ℤ))) :
        ℚ)
      ((↑(↑(p ^ n) : ℤ) : ℚ) : ℚ)
⊢ (↑(HDiv.hDiv (α := ℚ)
            ((Int.castRingHom ℚ : (a : ℤ) → ℚ)
                (coeff c
                  (HSub.hSub (α := MvPolynomial (idx × ℕ) ℤ) (β := MvPolynomial (idx × ℕ) ℤ)
                    ((bind₁ fun (i : idx) ↦
                            (rename fun (i_1 : ℕ) ↦ (i, i_1) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ)
                              (W_ ℤ n) :
                          (a : MvPolynomial idx ℤ) → MvPolynomial (idx × ℕ) ℤ)
                        Φ :
                      MvPolynomial (idx × ℕ) ℤ)
                    (∑ i ∈ Finset.range n,
                        HMul.hMul (α := MvPolynomial (idx × ℕ) ℤ)
                          ((C : (a : ℤ) → MvPolynomial (idx × ℕ) ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) i) :
                            MvPolynomial (idx × ℕ) ℤ)
                          (wittStructureInt p Φ i ^ p ^ (n - i)) :
                      MvPolynomial (idx × ℕ) ℤ))) :
              ℚ)
            (HPow.hPow (α := ℚ) (↑p : ℚ) n)).num :
      ℚ) =
    HDiv.hDiv (α := ℚ)
      ((Int.castRingHom ℚ : (a : ℤ) → ℚ)
          (coeff c
            (HSub.hSub (α := MvPolynomial (idx × ℕ) ℤ) (β := MvPolynomial (idx × ℕ) ℤ)
              ((bind₁ fun (i : idx) ↦
                      (rename fun (i_1 : ℕ) ↦ (i, i_1) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (W_ ℤ n) :
                    (a : MvPolynomial idx ℤ) → MvPolynomial (idx × ℕ) ℤ)
                  Φ :
                MvPolynomial (idx × ℕ) ℤ)
              (∑ i ∈ Finset.range n,
                  HMul.hMul (α := MvPolynomial (idx × ℕ) ℤ)
                    ((C : (a : ℤ) → MvPolynomial (idx × ℕ) ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) i) :
                      MvPolynomial (idx × ℕ) ℤ)
                    (wittStructureInt p Φ i ^ p ^ (n - i)) :
                MvPolynomial (idx × ℕ) ℤ))) :
        ℚ)
      (HPow.hPow (α := ℚ) (↑p : ℚ) n)

Tactic:
rw [show (p : ℚ) ^ n = ((↑(p ^ n) : ℤ) : ℚ) by norm_cast]