-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ m < n + 1,
    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 × ℕ) ℚ)
key :
  Eq (α := MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
    ((bind₁ fun (i : idx) ↦
            (rename fun (i_1 : ℕ) ↦ (i, i_1) :
                (a : MvPolynomial ℕ (ZMod (p ^ (n + 1)))) → MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
              ((expand p : (a : MvPolynomial ℕ (ZMod (p ^ (n + 1)))) → MvPolynomial ℕ (ZMod (p ^ (n + 1))))
                (W_ (ZMod (p ^ (n + 1))) n)) :
          (a : MvPolynomial idx (ZMod (p ^ (n + 1)))) → MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
        ((map (Int.castRingHom (ZMod (p ^ (n + 1)))) : (a : MvPolynomial idx ℤ) → MvPolynomial idx (ZMod (p ^ (n + 1))))
            Φ :
          MvPolynomial idx (ZMod (p ^ (n + 1)))) :
      MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
    ((map (Int.castRingHom (ZMod (p ^ (n + 1)))) :
          (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
        ((bind₁ fun (i : ℕ) ↦
                (expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ i) :
              (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ)
            (W_ ℤ n) :
          MvPolynomial (idx × ℕ) ℤ) :
      MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
succ :
  Eq.{u_2 + 1} (α := MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
    ((map (Int.castRingHom (ZMod (p ^ (n + 1)))) :
          (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
        ((bind₁ fun (i : ℕ) ↦
                (expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ i) :
              (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ)
            (W_ ℤ n) :
          MvPolynomial (idx × ℕ) ℤ) :
      MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
    ((map (Int.castRingHom (ZMod (p ^ (n + 1)))) :
          (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
        (∑ i ∈ Finset.range (n + 1),
          HMul.hMul (α := MvPolynomial (idx × ℕ) ℤ)
            ((C : (a : ℤ) → MvPolynomial (idx × ℕ) ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) i) : MvPolynomial (idx × ℕ) ℤ)
            (wittStructureInt p Φ i ^ p ^ (n + 1 - i))) :
      MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
⊢ Eq (α := MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
    ((bind₁ fun (i : idx) ↦
            (rename fun (i_1 : ℕ) ↦ (i, i_1) :
                (a : MvPolynomial ℕ (ZMod (p ^ (n + 1)))) → MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
              ((expand p : (a : MvPolynomial ℕ (ZMod (p ^ (n + 1)))) → MvPolynomial ℕ (ZMod (p ^ (n + 1))))
                (W_ (ZMod (p ^ (n + 1))) n)) :
          (a : MvPolynomial idx (ZMod (p ^ (n + 1)))) → MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
        ((map (Int.castRingHom (ZMod (p ^ (n + 1)))) : (a : MvPolynomial idx ℤ) → MvPolynomial idx (ZMod (p ^ (n + 1))))
            Φ :
          MvPolynomial idx (ZMod (p ^ (n + 1)))) :
      MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
    ((map (Int.castRingHom (ZMod (p ^ (n + 1)))) :
          (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
        (∑ i ∈ Finset.range (n + 1),
          HMul.hMul (α := MvPolynomial (idx × ℕ) ℤ)
            ((C : (a : ℤ) → MvPolynomial (idx × ℕ) ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) i) : MvPolynomial (idx × ℕ) ℤ)
            (wittStructureInt p Φ i ^ p ^ (n + 1 - i))) :
      MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))

Tactic:
rw [key]