-- 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 × ℕ) ℚ)
zero :
  ∀
    (IH :
      ∀ m < 0,
        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 : (a : ℤ) → MvPolynomial (idx × ℕ) ℤ) (↑(HPow.hPow (β := ℕ) p 0) : ℤ) ∣
      HSub.hSub (α := MvPolynomial (idx × ℕ) ℤ) (β := MvPolynomial (idx × ℕ) ℤ)
        ((bind₁ fun (b : idx) ↦
                (rename fun (i : ℕ) ↦ (b, i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (W_ ℤ 0) :
              (a : MvPolynomial idx ℤ) → MvPolynomial (idx × ℕ) ℤ)
            Φ :
          MvPolynomial (idx × ℕ) ℤ)
        (∑ i ∈ Finset.range 0,
            HMul.hMul (α := MvPolynomial (idx × ℕ) ℤ)
              ((C : (a : ℤ) → MvPolynomial (idx × ℕ) ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) i) : MvPolynomial (idx × ℕ) ℤ)
              (wittStructureInt p Φ i ^ p ^ (0 - i)) :
          MvPolynomial (idx × ℕ) ℤ)
⊢ (C : (a : ℤ) → MvPolynomial (idx × ℕ) ℤ) (↑(p ^ n) : ℤ) ∣
    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 × ℕ) ℤ)
          Φ :
        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 × ℕ) ℤ)
have succ : ∀ (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 × ℕ) ℚ)),
  (C : (a : ℤ) → MvPolynomial (idx × ℕ) ℤ) (↑(p ^ (n + 1)) : ℤ) ∣
    HSub.hSub (α := MvPolynomial (idx × ℕ) ℤ) (β := MvPolynomial (idx × ℕ) ℤ)
      ((bind₁ fun (b : idx) ↦
              (rename fun (i : ℕ) ↦ (b, i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (W_ ℤ (n + 1)) :
            (a : MvPolynomial idx ℤ) → MvPolynomial (idx × ℕ) ℤ)
          Φ :
        MvPolynomial (idx × ℕ) ℤ)
      (∑ 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 × ℕ) ℤ)
Tactic: rcases n with - | n
Cleared hypotheses: n, IH