-- 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 × ℕ) ℤ))) :
              ℚ)
            (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)
⊢ (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

Tactic:
simp only [← sum_induction_steps, ← map_wittPolynomial p (Int.castRingHom ℚ), ← map_rename, ←
    map_bind₁, ← map_sub, coeff_map]

Premises used: MvPolynomial.map_bind₁, map_sub, MvPolynomial.map_rename, Rat, MvPolynomial.coeff_map, Int.castRingHom, map_wittPolynomial