-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
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 × ℕ) ℚ)
⊢ (↑(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)
have 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) : ℤ) : ℚ) : ℚ)
Tactic: rw [show (p : ℚ) ^ n = ((↑(p ^ n) : ℤ) : ℚ) by norm_cast]