-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
this : p ^ (n + 1) = p ^ k * p ^ (n - k + 1)
succ :
  (C : (a : ℤ) → MvPolynomial (idx × ℕ) ℤ) (↑p : ℤ) ∣
    HSub.hSub (α := MvPolynomial (idx × ℕ) ℤ)
      ((expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ k) :
        MvPolynomial (idx × ℕ) ℤ)
      (wittStructureInt p Φ k ^ p)
succ₁ :
  Eq (α := MvPolynomial (idx × ℕ) (ZMod p))
    ((map (Int.castRingHom (ZMod p)) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) (ZMod p))
        (HSub.hSub (α := MvPolynomial (idx × ℕ) ℤ)
          ((expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ k) :
            MvPolynomial (idx × ℕ) ℤ)
          (wittStructureInt p Φ k ^ p)) :
      MvPolynomial (idx × ℕ) (ZMod p))
    (0 : MvPolynomial (idx × ℕ) (ZMod p))
succ₂ :
  HSub.hSub (α := MvPolynomial (idx × ℕ) (ZMod p)) (β := MvPolynomial (idx × ℕ) (ZMod p))
      ((map (Int.castRingHom (ZMod p)) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) (ZMod p))
          ((expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ k) :
            MvPolynomial (idx × ℕ) ℤ) :
        MvPolynomial (idx × ℕ) (ZMod p))
      ((map (Int.castRingHom (ZMod p)) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) (ZMod p))
          (wittStructureInt p Φ k ^ p) :
        MvPolynomial (idx × ℕ) (ZMod p)) =
    0
succ₃ :
  Eq (α := MvPolynomial (idx × ℕ) (ZMod p))
    ((map (Int.castRingHom (ZMod p)) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) (ZMod p))
        ((expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ k) :
          MvPolynomial (idx × ℕ) ℤ) :
      MvPolynomial (idx × ℕ) (ZMod p))
    ((map (Int.castRingHom (ZMod p)) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) (ZMod p))
        (wittStructureInt p Φ k ^ p) :
      MvPolynomial (idx × ℕ) (ZMod p))
succ₄ :
  Eq (α := MvPolynomial (idx × ℕ) (ZMod p))
    ((expand p : (a : MvPolynomial (idx × ℕ) (ZMod p)) → MvPolynomial (idx × ℕ) (ZMod p))
        ((map (Int.castRingHom (ZMod p)) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) (ZMod p))
            (wittStructureInt p Φ k) :
          MvPolynomial (idx × ℕ) (ZMod p)) :
      MvPolynomial (idx × ℕ) (ZMod p))
    ((map (Int.castRingHom (ZMod p)) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) (ZMod p))
        (wittStructureInt p Φ k ^ p) :
      MvPolynomial (idx × ℕ) (ZMod p))
succ₅ :
  (expand p : (a : MvPolynomial (idx × ℕ) (ZMod p)) → MvPolynomial (idx × ℕ) (ZMod p))
      ((map (Int.castRingHom (ZMod p)) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) (ZMod p))
          (wittStructureInt p Φ k) :
        MvPolynomial (idx × ℕ) (ZMod p)) =
    HPow.hPow (α := MvPolynomial (idx × ℕ) (ZMod p))
      ((map (Int.castRingHom (ZMod p)) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) (ZMod p))
          (wittStructureInt p Φ k) :
        MvPolynomial (idx × ℕ) (ZMod p))
      p
⊢ (↑p : MvPolynomial (idx × ℕ) ℤ) ∣
    HSub.hSub (α := MvPolynomial (idx × ℕ) ℤ)
      ((expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ k) :
        MvPolynomial (idx × ℕ) ℤ)
      (wittStructureInt p Φ k ^ p)
have succ₆ : HPow.hPow (α := MvPolynomial (idx × ℕ) (ZMod p))
    ((map (Int.castRingHom (ZMod p)) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) (ZMod p))
        (wittStructureInt p Φ k) :
      MvPolynomial (idx × ℕ) (ZMod p))
    p =
  HPow.hPow (α := MvPolynomial (idx × ℕ) (ZMod p))
    ((map (Int.castRingHom (ZMod p)) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) (ZMod p))
        (wittStructureInt p Φ k) :
      MvPolynomial (idx × ℕ) (ZMod p))
    p
Tactic: rw [← C_eq_coe_nat, C_dvd_iff_zmod, map_sub, sub_eq_zero, map_expand, map_pow,
    MvPolynomial.expand_zmod]