-- 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 × ℕ) ℚ)
⊢ (fun (x : ℤ) ↦ ((↑x : ℚ) : ℚ))
      (coeff c
            (HSub.hSub (α := MvPolynomial (idx × ℕ) ℚ) (β := MvPolynomial (idx × ℕ) ℚ)
              ((bind₁ fun (b : idx) ↦
                      (rename fun (i : ℕ) ↦ (b, i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) :
                    (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
                  ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ : MvPolynomial idx ℚ) :
                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 × ℕ) ℚ)) /
          HPow.hPow (α := ℚ) (↑p : ℚ) n).num =
    coeff c
        (HSub.hSub (α := MvPolynomial (idx × ℕ) ℚ) (β := MvPolynomial (idx × ℕ) ℚ)
          ((bind₁ fun (b : idx) ↦
                  (rename fun (i : ℕ) ↦ (b, i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) :
                (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
              ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ : MvPolynomial idx ℚ) :
            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 × ℕ) ℚ)) /
      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 × ℕ) ℤ))) :
            ℚ)
          (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: simp only [← sum_induction_steps, ← map_wittPolynomial p (Int.castRingHom ℚ), ← map_rename, ←
    map_bind₁, ← map_sub, coeff_map]