awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ (↑(p ^ k * p ^ (n - k + 1)) : MvPolynomial (idx × ℕ) ℤ) ∣
    (↑(p ^ k) : MvPolynomial (idx × ℕ) ℤ) *
      (HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ)
          ((expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ k) :
            MvPolynomial (idx × ℕ) ℤ)
          (p ^ (n - k)) -
        wittStructureInt p Φ k ^ p ^ (n + 1 - k))
have succ : HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ) (↑p : MvPolynomial (idx × ℕ) ℤ) k *
    HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ) (↑p : MvPolynomial (idx × ℕ) ℤ) (n - k + 1) ∣
  HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ) (↑p : MvPolynomial (idx × ℕ) ℤ) k *
    (HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ)
        ((expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ k) :
          MvPolynomial (idx × ℕ) ℤ)
        (p ^ (n - k)) -
      wittStructureInt p Φ k ^ p ^ (n + 1 - k))
Tactic: rw [Nat.cast_mul, Nat.cast_pow, Nat.cast_pow]
-- 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)
⊢ HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ) (↑p : MvPolynomial (idx × ℕ) ℤ) k *
      HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ) (↑p : MvPolynomial (idx × ℕ) ℤ) (n - k + 1) ∣
    HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ) (↑p : MvPolynomial (idx × ℕ) ℤ) k *
      (HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ)
          ((expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ k) :
            MvPolynomial (idx × ℕ) ℤ)
          (p ^ (n - k)) -
        wittStructureInt p Φ k ^ p ^ (n + 1 - k))
have succ : HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ) (↑p : MvPolynomial (idx × ℕ) ℤ) (n - k + 1) ∣
  HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ)
      ((expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ k) :
        MvPolynomial (idx × ℕ) ℤ)
      (p ^ (n - k)) -
    wittStructureInt p Φ k ^ p ^ (n + 1 - k)
Tactic: apply mul_dvd_mul_left ((p : MvPolynomial (idx × ℕ) ℤ) ^ k)
-- 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)
⊢ p ^ (n + 1 - k) = p * p ^ (n - k)
have rw : p ^ (n + 1 - k) = p ^ (n - k + 1)
Tactic: rw [← pow_succ', ← tsub_add_eq_add_tsub hk]
-- 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)
rw : p ^ (n + 1 - k) = p ^ (n - k + 1)
⊢ p ^ (n + 1 - k) = p * p ^ (n - k)
have rw₁ : p ^ (n - k + 1) = p ^ (n - k + 1)
Tactic: rw [← pow_succ', ← tsub_add_eq_add_tsub hk]
-- 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)
⊢ HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ) (↑p : MvPolynomial (idx × ℕ) ℤ) (n - k + 1) ∣
    HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ)
        ((expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ k) :
          MvPolynomial (idx × ℕ) ℤ)
        (p ^ (n - k)) -
      wittStructureInt p Φ k ^ p ^ (n + 1 - k)
have succ : HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ) (↑p : MvPolynomial (idx × ℕ) ℤ) (n - k + 1) ∣
  HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ)
      ((expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ k) :
        MvPolynomial (idx × ℕ) ℤ)
      (p ^ (n - k)) -
    wittStructureInt p Φ k ^ (p * p ^ (n - k))
Tactic: rw [show p ^ (n + 1 - k) = p * p ^ (n - k) by rw [← pow_succ', ← tsub_add_eq_add_tsub hk]]
-- 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)
⊢ HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ) (↑p : MvPolynomial (idx × ℕ) ℤ) (n - k + 1) ∣
    HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ)
        ((expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ k) :
          MvPolynomial (idx × ℕ) ℤ)
        (p ^ (n - k)) -
      wittStructureInt p Φ k ^ (p * p ^ (n - k))
have succ : HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ) (↑p : MvPolynomial (idx × ℕ) ℤ) (n - k + 1) ∣
  HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ)
      ((expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ k) :
        MvPolynomial (idx × ℕ) ℤ)
      (p ^ (n - k)) -
    (wittStructureInt p Φ k ^ p) ^ p ^ (n - k)
Tactic: rw [pow_mul]
-- 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)
⊢ HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ) (↑p : MvPolynomial (idx × ℕ) ℤ) (n - k + 1) ∣
    HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ)
        ((expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ k) :
          MvPolynomial (idx × ℕ) ℤ)
        (p ^ (n - k)) -
      (wittStructureInt p Φ k ^ p) ^ p ^ (n - k)
have succ : (↑p : MvPolynomial (idx × ℕ) ℤ) ∣
  HSub.hSub (α := MvPolynomial (idx × ℕ) ℤ)
    ((expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ k) :
      MvPolynomial (idx × ℕ) ℤ)
    (wittStructureInt p Φ k ^ p)
Tactic: apply dvd_sub_pow_of_dvd_sub
-- 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)
⊢ (↑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 : (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)
Tactic: rw [← C_eq_coe_nat, C_dvd_iff_zmod, map_sub, sub_eq_zero, map_expand, map_pow,
    MvPolynomial.expand_zmod]
-- 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)
⊢ (↑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₁ : 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))
Tactic: rw [← C_eq_coe_nat, C_dvd_iff_zmod, map_sub, sub_eq_zero, map_expand, map_pow,
    MvPolynomial.expand_zmod]
-- 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))
⊢ (↑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₂ : 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
Tactic: rw [← C_eq_coe_nat, C_dvd_iff_zmod, map_sub, sub_eq_zero, map_expand, map_pow,
    MvPolynomial.expand_zmod]
-- 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
⊢ (↑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₃ : 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))
Tactic: rw [← C_eq_coe_nat, C_dvd_iff_zmod, map_sub, sub_eq_zero, map_expand, map_pow,
    MvPolynomial.expand_zmod]
-- 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))
⊢ (↑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₄ : 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))
Tactic: rw [← C_eq_coe_nat, C_dvd_iff_zmod, map_sub, sub_eq_zero, map_expand, map_pow,
    MvPolynomial.expand_zmod]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ Eq (α := MvPolynomial (idx × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (wittStructureInt p Φ n) :
      MvPolynomial (idx × ℕ) ℚ)
    (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) n :
      MvPolynomial (idx × ℕ) ℚ)
have h : ∀ (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 × ℕ) ℚ)),
  Eq (α := MvPolynomial (idx × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (wittStructureInt p Φ n) :
      MvPolynomial (idx × ℕ) ℚ)
    (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) n :
      MvPolynomial (idx × ℕ) ℚ)
Tactic: induction n using Nat.strong_induction_on with | h n IH => ?_
Cleared hypotheses: n
-- 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 × ℕ) ℚ)
⊢ Eq (α := MvPolynomial (idx × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (wittStructureInt p Φ n) :
      MvPolynomial (idx × ℕ) ℚ)
    (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) n :
      MvPolynomial (idx × ℕ) ℚ)
have h : ∀ (d : idx × ℕ →₀ ℕ),
  (fun (x : ℤ) ↦ ((↑x : ℚ) : ℚ))
      (coeff d
          (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) n)).num =
    coeff d (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) n)
Tactic: rw [wittStructureInt, map_mapRange_eq_iff, Int.coe_castRingHom]
-- 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 × ℕ →₀ ℕ
⊢ (fun (x : ℤ) ↦ ((↑x : ℚ) : ℚ))
      (coeff c
          (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) n)).num =
    coeff c (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) n)
have h : (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: rw [wittStructureRat_rec, coeff_C_mul, mul_comm, mul_div_assoc', mul_one]
-- 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 × ℕ →₀ ℕ
⊢ 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 × ℕ) ℚ)
have rw : Eq.{u_2 + 1} (α := MvPolynomial (idx × ℕ) ℚ)
  (∑ x ∈ Finset.range n,
    (map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ)
      (HMul.hMul (α := MvPolynomial (idx × ℕ) ℤ)
        ((C : (a : ℤ) → MvPolynomial (idx × ℕ) ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) x) : MvPolynomial (idx × ℕ) ℤ)
        (wittStructureInt p Φ x ^ p ^ (n - x))))
  (∑ 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))))
Tactic: rw [map_sum]