awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
w : 𝕎 R
h : Eq (α := 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) w : 𝕎 R) (0 : 𝕎 R)
⊢ w = 0
have h₁ : ∀ (n : ℕ), w.coeff n = coeff (p := p) 0 n
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
w : 𝕎 R
h : Eq (α := 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) w : 𝕎 R) (0 : 𝕎 R)
n : ℕ
⊢ w.coeff n = coeff (p := p) 0 n
have h₁ : Eq.{u_1 + 1} (α := R) (coeff (p := p) 0 n.succ) (coeff (p := p) 0 n)
Tactic: rw [← verschiebung_coeff_succ, h]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (bind₁ verschiebungPoly : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n) =
    if n = 0 then 0 else HMul.hMul (α := MvPolynomial ℕ ℤ) (↑p : MvPolynomial ℕ ℤ) (wittPolynomial p ℤ (n - 1))
have h : ∀ (x : ℕ → ℤ),
  Eq (α := ℤ)
    ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ)
        ((bind₁ verschiebungPoly : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n) :
          MvPolynomial ℕ ℤ) :
      ℤ)
    ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ)
        (if n = 0 then 0 else HMul.hMul (α := MvPolynomial ℕ ℤ) (↑p : MvPolynomial ℕ ℤ) (wittPolynomial p ℤ (n - 1))) :
      ℤ)
Tactic: apply MvPolynomial.funext
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℕ → ℤ
⊢ Eq (α := ℤ)
    ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ)
        ((bind₁ verschiebungPoly : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n) :
          MvPolynomial ℕ ℤ) :
      ℤ)
    ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ)
        (if n = 0 then 0 else HMul.hMul (α := MvPolynomial ℕ ℤ) (↑p : MvPolynomial ℕ ℤ) (wittPolynomial p ℤ (n - 1))) :
      ℤ)
have pos : ∀ (hn : n = 0),
  Eq (α := ℤ)
    ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ)
        ((bind₁ verschiebungPoly : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n) :
          MvPolynomial ℕ ℤ) :
      ℤ)
    ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) 0 : ℤ)
Tactic: split_ifs with hn
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℕ → ℤ
pos :
  ∀ (hn : n = 0),
    Eq (α := ℤ)
      ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ)
          ((bind₁ verschiebungPoly : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n) :
            MvPolynomial ℕ ℤ) :
        ℤ)
      ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) 0 : ℤ)
⊢ Eq (α := ℤ)
    ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ)
        ((bind₁ verschiebungPoly : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n) :
          MvPolynomial ℕ ℤ) :
      ℤ)
    ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ)
        (if n = 0 then 0 else HMul.hMul (α := MvPolynomial ℕ ℤ) (↑p : MvPolynomial ℕ ℤ) (wittPolynomial p ℤ (n - 1))) :
      ℤ)
have neg : ∀ (hn : ¬n = 0),
  Eq (α := ℤ)
    ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ)
        ((bind₁ verschiebungPoly : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n) :
          MvPolynomial ℕ ℤ) :
      ℤ)
    ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ)
        (HMul.hMul (α := MvPolynomial ℕ ℤ) (↑p : MvPolynomial ℕ ℤ) (wittPolynomial p ℤ (n - 1))) :
      ℤ)
Tactic: split_ifs with hn
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℕ → ℤ
hn : ¬n = 0
⊢ Eq (α := ℤ)
    ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ)
        ((bind₁ verschiebungPoly : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n) :
          MvPolynomial ℕ ℤ) :
      ℤ)
    ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ)
        (HMul.hMul (α := MvPolynomial ℕ ℤ) (↑p : MvPolynomial ℕ ℤ) (wittPolynomial p ℤ (n - 1))) :
      ℤ)
have neg : ∀ (n : ℕ) (hn : ¬n.succ = 0),
  Eq (α := ℤ)
    ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ)
        ((bind₁ verschiebungPoly : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n.succ) :
          MvPolynomial ℕ ℤ) :
      ℤ)
    ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ)
        (HMul.hMul (α := MvPolynomial ℕ ℤ) (↑p : MvPolynomial ℕ ℤ) (wittPolynomial p ℤ (n.succ - 1))) :
      ℤ)
Tactic: obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
⊢ Eq (α := ℤ)
    ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ)
        ((bind₁ verschiebungPoly : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n.succ) :
          MvPolynomial ℕ ℤ) :
      ℤ)
    ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ)
        (HMul.hMul (α := MvPolynomial ℕ ℤ) (↑p : MvPolynomial ℕ ℤ) (wittPolynomial p ℤ (n.succ - 1))) :
      ℤ)
have neg : Eq (α := ℤ)
  ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ)
      ((bind₁ verschiebungPoly : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ (n + 1)) :
        MvPolynomial ℕ ℤ) :
    ℤ)
  ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ)
      (HMul.hMul (α := MvPolynomial ℕ ℤ) (↑p : MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n)) :
    ℤ)
Tactic: rw [Nat.succ_eq_add_one, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
⊢ Eq (α := ℤ)
    ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ)
        ((bind₁ verschiebungPoly : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ (n + 1)) :
          MvPolynomial ℕ ℤ) :
      ℤ)
    ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ)
        (HMul.hMul (α := MvPolynomial ℕ ℤ) (↑p : MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n)) :
      ℤ)
have neg : (MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ)
    ((bind₁ verschiebungPoly : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ (n + 1)) :
      MvPolynomial ℕ ℤ) =
  HMul.hMul (α := ℤ) (β := ℤ) ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (↑p : MvPolynomial ℕ ℤ) : ℤ)
    ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (wittPolynomial p ℤ n) : ℤ)
Tactic: simp only [map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
⊢ (MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ)
      ((bind₁ verschiebungPoly : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ (n + 1)) :
        MvPolynomial ℕ ℤ) =
    HMul.hMul (α := ℤ) (β := ℤ) ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (↑p : MvPolynomial ℕ ℤ) : ℤ)
      ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (wittPolynomial p ℤ n) : ℤ)
have neg : (eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun (i : ℕ) ↦
        (MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (verschiebungPoly i) :
      (a : MvPolynomial ℕ ℤ) → ℤ)
    (wittPolynomial p ℤ (n + 1)) =
  HMul.hMul (α := ℤ) (β := ℤ) ((↑p : ℤ) : ℤ)
    ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (wittPolynomial p ℤ n) : ℤ)
Tactic: rw [map_natCast, hom_bind₁]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
⊢ Eq (α := ℤ)
    ((eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun (i : ℕ) ↦
            (MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (verschiebungPoly i) :
          (a : MvPolynomial ℕ ℤ) → ℤ)
        (wittPolynomial p ℤ (n + 1)) :
      ℤ)
    ((ghostComponent (n + 1) : (a : 𝕎 ℤ) → ℤ) ((verschiebung : (a : 𝕎 ℤ) → 𝕎 ℤ) (mk p x) : 𝕎 ℤ) : ℤ)
have apply : Eq (α := ℕ → ℤ) (fun (i : ℕ) ↦ (MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (verschiebungPoly i))
  (coeff (p := p) ((verschiebung : (a : 𝕎 ℤ) → 𝕎 ℤ) (mk p x)))
Tactic: apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
⊢ Eq (α := ℕ → ℤ) (fun (i : ℕ) ↦ (MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (verschiebungPoly i))
    (coeff (p := p) ((verschiebung : (a : 𝕎 ℤ) → 𝕎 ℤ) (mk p x)))
have h : ∀ (k : ℕ),
  Eq (α := ℤ) ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (verschiebungPoly k) : ℤ)
    (coeff (p := p) ((verschiebung : (a : 𝕎 ℤ) → 𝕎 ℤ) (mk p x)) k : ℤ)
Tactic: funext k
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
k : ℕ
⊢ Eq (α := ℤ) ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (verschiebungPoly k) : ℤ)
    (coeff (p := p) ((verschiebung : (a : 𝕎 ℤ) → 𝕎 ℤ) (mk p x)) k : ℤ)
have h : Eq (α := ℤ) ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (verschiebungPoly k) : ℤ)
  ((aeval (mk p x).coeff : (a : MvPolynomial ℕ ℤ) → ℤ) (verschiebungPoly k) : ℤ)
Tactic: simp only [← aeval_verschiebungPoly]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
⊢ (ghostComponent (n + 1) : (a : 𝕎 ℤ) → ℤ) ((verschiebung : (a : 𝕎 ℤ) → 𝕎 ℤ) (mk p x) : 𝕎 ℤ) =
    HMul.hMul (α := ℤ) (β := ℤ) ((↑p : ℤ) : ℤ)
      ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (wittPolynomial p ℤ n) : ℤ)
have rw : HMul.hMul (α := ℤ) (β := ℤ) ((↑p : ℤ) : ℤ) ((ghostComponent n : (a : 𝕎 ℤ) → ℤ) (mk p x) : ℤ) =
  HMul.hMul (α := ℤ) (β := ℤ) ((↑p : ℤ) : ℤ)
    ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (wittPolynomial p ℤ n) : ℤ)
Tactic: rw [ghostComponent_verschiebung]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
⊢ (eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun (i : ℕ) ↦
          (MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (verschiebungPoly i) :
        (a : MvPolynomial ℕ ℤ) → ℤ)
      (wittPolynomial p ℤ (n + 1)) =
    HMul.hMul (α := ℤ) (β := ℤ) ((↑p : ℤ) : ℤ)
      ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (wittPolynomial p ℤ n) : ℤ)
have _ : Eq (α := ℤ)
  ((eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun (i : ℕ) ↦
          (MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (verschiebungPoly i) :
        (a : MvPolynomial ℕ ℤ) → ℤ)
      (wittPolynomial p ℤ (n + 1)) :
    ℤ)
  ((ghostComponent (n + 1) : (a : 𝕎 ℤ) → ℤ) ((verschiebung : (a : 𝕎 ℤ) → 𝕎 ℤ) (mk p x) : 𝕎 ℤ) : ℤ)
Tactic: calc
      _ = ghostComponent (n + 1) (verschiebung <| mk p x) := by
       apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
       funext k
       simp only [← aeval_verschiebungPoly]
       exact eval₂Hom_congr (RingHom.ext_int _ _) rfl rfl
      _ = _ := by rw [ghostComponent_verschiebung]; rfl
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
_ :
  Eq (α := ℤ)
    ((eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun (i : ℕ) ↦
            (MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (verschiebungPoly i) :
          (a : MvPolynomial ℕ ℤ) → ℤ)
        (wittPolynomial p ℤ (n + 1)) :
      ℤ)
    ((ghostComponent (n + 1) : (a : 𝕎 ℤ) → ℤ) ((verschiebung : (a : 𝕎 ℤ) → 𝕎 ℤ) (mk p x) : 𝕎 ℤ) : ℤ)
⊢ (eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun (i : ℕ) ↦
          (MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (verschiebungPoly i) :
        (a : MvPolynomial ℕ ℤ) → ℤ)
      (wittPolynomial p ℤ (n + 1)) =
    HMul.hMul (α := ℤ) (β := ℤ) ((↑p : ℤ) : ℤ)
      ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (wittPolynomial p ℤ n) : ℤ)
have _₁ : (ghostComponent (n + 1) : (a : 𝕎 ℤ) → ℤ) ((verschiebung : (a : 𝕎 ℤ) → 𝕎 ℤ) (mk p x) : 𝕎 ℤ) =
  HMul.hMul (α := ℤ) (β := ℤ) ((↑p : ℤ) : ℤ)
    ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (wittPolynomial p ℤ n) : ℤ)
Tactic: calc
      _ = ghostComponent (n + 1) (verschiebung <| mk p x) := by
       apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
       funext k
       simp only [← aeval_verschiebungPoly]
       exact eval₂Hom_congr (RingHom.ext_int _ _) rfl rfl
      _ = _ := by rw [ghostComponent_verschiebung]; rfl
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
n : ℕ
⊢ Eq (α := MvPolynomial ℕ R) (wittPolynomial p R n)
    (∑ i ∈ range (n + 1),
      HMul.hMul (α := MvPolynomial ℕ R)
        ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
        (HPow.hPow (α := MvPolynomial ℕ R) (X i) (p ^ (n - i))))
have apply : ∀ x ∈ range (n + 1),
  (monomial (single x (p ^ (n - x))) : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) x) =
    HMul.hMul (α := MvPolynomial ℕ R)
      ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) x) : MvPolynomial ℕ R)
      (HPow.hPow (α := MvPolynomial ℕ R) (X x) (p ^ (n - x)))
Tactic: apply sum_congr rfl
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
n i : ℕ
⊢ (monomial (single i (p ^ (n - i))) : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) =
    HMul.hMul (α := MvPolynomial ℕ R)
      ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
      (HPow.hPow (α := MvPolynomial ℕ R) (X i) (p ^ (n - i)))
have rw : HPow.hPow (α := MvPolynomial ℕ R) (β := ℕ) (X i) 0 = 1
Tactic: rw [monomial_eq, Finsupp.prod_single_index]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
n i : ℕ
⊢ HPow.hPow (α := MvPolynomial ℕ R) (β := ℕ) (X i) 0 = 1
have rw : Eq.{u_1 + 1} (α := MvPolynomial ℕ R) 1 1
Tactic: rw [pow_zero]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
n : ℕ
⊢ Eq.{u_2 + 1} (α := MvPolynomial ℕ S)
    (((map f : RingHom.{u_1, u_2} (MvPolynomial ℕ R) (MvPolynomial ℕ S)) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ S)
        (W_ R n) :
      MvPolynomial ℕ S)
    (W_ S n : MvPolynomial ℕ S)
have rw : Eq.{u_2 + 1} (α := MvPolynomial ℕ S)
  (∑ x ∈ range (n + 1),
    ((map f : RingHom.{u_1, u_2} (MvPolynomial ℕ R) (MvPolynomial ℕ S)) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ S)
      ((monomial (single x (p ^ (n - x))) : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) x)))
  (∑ i ∈ range (n + 1),
    (monomial (single i (p ^ (n - i))) : (a : S) → MvPolynomial ℕ S) (HPow.hPow (α := S) (↑p : S) i))
Tactic: rw [wittPolynomial, map_sum, wittPolynomial]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
n : ℕ
⊢ Eq.{u_2 + 1} (α := MvPolynomial ℕ S)
    (∑ x ∈ range (n + 1),
      ((map f : RingHom.{u_1, u_2} (MvPolynomial ℕ R) (MvPolynomial ℕ S)) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ S)
        ((monomial (single x (p ^ (n - x))) : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) x)))
    (∑ i ∈ range (n + 1),
      (monomial (single i (p ^ (n - i))) : (a : S) → MvPolynomial ℕ S) (HPow.hPow (α := S) (↑p : S) i))
have refine : ∀ i ∈ range (n + 1),
  Eq.{u_2 + 1} (α := MvPolynomial ℕ S)
    (((map f : RingHom.{u_1, u_2} (MvPolynomial ℕ R) (MvPolynomial ℕ S)) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ S)
        ((monomial (single i (p ^ (n - i))) : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i)) :
      MvPolynomial ℕ S)
    ((monomial (single i (p ^ (n - i))) : (a : S) → MvPolynomial ℕ S) (HPow.hPow (α := S) (↑p : S) i) :
      MvPolynomial ℕ S)
Tactic: refine sum_congr rfl fun i _ => ?_
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
n i : ℕ
h : i ∈ range (n + 1)
⊢ Eq.{u_2 + 1} (α := MvPolynomial ℕ S)
    (((map f : RingHom.{u_1, u_2} (MvPolynomial ℕ R) (MvPolynomial ℕ S)) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ S)
        ((monomial (single i (p ^ (n - i))) : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i)) :
      MvPolynomial ℕ S)
    ((monomial (single i (p ^ (n - i))) : (a : S) → MvPolynomial ℕ S) (HPow.hPow (α := S) (↑p : S) i) :
      MvPolynomial ℕ S)
have rw : Eq.{u_2 + 1} (α := MvPolynomial ℕ S)
  ((monomial (single i (p ^ (n - i))) : (a : S) → MvPolynomial ℕ S)
      ((f : (a : R) → S) (HPow.hPow (α := R) (↑p : R) i)) :
    MvPolynomial ℕ S)
  ((monomial (single i (p ^ (n - i))) : (a : S) → MvPolynomial ℕ S) (HPow.hPow (α := S) (↑p : S) i) : MvPolynomial ℕ S)
Tactic: rw [map_monomial, map_pow, map_natCast]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
n i : ℕ
h : i ∈ range (n + 1)
rw :
  Eq.{u_2 + 1} (α := MvPolynomial ℕ S)
    ((monomial (single i (p ^ (n - i))) : (a : S) → MvPolynomial ℕ S)
        ((f : (a : R) → S) (HPow.hPow (α := R) (↑p : R) i)) :
      MvPolynomial ℕ S)
    ((monomial (single i (p ^ (n - i))) : (a : S) → MvPolynomial ℕ S) (HPow.hPow (α := S) (↑p : S) i) :
      MvPolynomial ℕ S)
⊢ Eq.{u_2 + 1} (α := MvPolynomial ℕ S)
    (((map f : RingHom.{u_1, u_2} (MvPolynomial ℕ R) (MvPolynomial ℕ S)) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ S)
        ((monomial (single i (p ^ (n - i))) : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i)) :
      MvPolynomial ℕ S)
    ((monomial (single i (p ^ (n - i))) : (a : S) → MvPolynomial ℕ S) (HPow.hPow (α := S) (↑p : S) i) :
      MvPolynomial ℕ S)
have rw₁ : Eq (α := MvPolynomial ℕ S)
  ((monomial (single i (p ^ (n - i))) : (a : S) → MvPolynomial ℕ S)
      (HPow.hPow (α := S) ((f : (a : R) → S) (↑p : R) : S) i) :
    MvPolynomial ℕ S)
  ((monomial (single i (p ^ (n - i))) : (a : S) → MvPolynomial ℕ S) (HPow.hPow (α := S) (↑p : S) i) : MvPolynomial ℕ S)
Tactic: rw [map_monomial, map_pow, map_natCast]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
n i : ℕ
h : i ∈ range (n + 1)
rw :
  Eq.{u_2 + 1} (α := MvPolynomial ℕ S)
    ((monomial (single i (p ^ (n - i))) : (a : S) → MvPolynomial ℕ S)
        ((f : (a : R) → S) (HPow.hPow (α := R) (↑p : R) i)) :
      MvPolynomial ℕ S)
    ((monomial (single i (p ^ (n - i))) : (a : S) → MvPolynomial ℕ S) (HPow.hPow (α := S) (↑p : S) i) :
      MvPolynomial ℕ S)
rw₁ :
  Eq (α := MvPolynomial ℕ S)
    ((monomial (single i (p ^ (n - i))) : (a : S) → MvPolynomial ℕ S)
        (HPow.hPow (α := S) ((f : (a : R) → S) (↑p : R) : S) i) :
      MvPolynomial ℕ S)
    ((monomial (single i (p ^ (n - i))) : (a : S) → MvPolynomial ℕ S) (HPow.hPow (α := S) (↑p : S) i) :
      MvPolynomial ℕ S)
⊢ Eq.{u_2 + 1} (α := MvPolynomial ℕ S)
    (((map f : RingHom.{u_1, u_2} (MvPolynomial ℕ R) (MvPolynomial ℕ S)) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ S)
        ((monomial (single i (p ^ (n - i))) : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i)) :
      MvPolynomial ℕ S)
    ((monomial (single i (p ^ (n - i))) : (a : S) → MvPolynomial ℕ S) (HPow.hPow (α := S) (↑p : S) i) :
      MvPolynomial ℕ S)
have rw₂ : Eq (α := MvPolynomial ℕ S)
  ((monomial (single i (p ^ (n - i))) : (a : S) → MvPolynomial ℕ S) (HPow.hPow (α := S) (↑p : S) i) : MvPolynomial ℕ S)
  ((monomial (single i (p ^ (n - i))) : (a : S) → MvPolynomial ℕ S) (HPow.hPow (α := S) (↑p : S) i) : MvPolynomial ℕ S)
Tactic: rw [map_monomial, map_pow, map_natCast]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
n : ℕ
⊢ Eq (α := R) ((constantCoeff : (a : MvPolynomial ℕ R) → R) (W_ R n) : R) (0 : R)
have simp : Eq.{u_1 + 1} (α := R)
  (∑ x ∈ range (n + 1), if Eq (α := ℕ →₀ ℕ) (single x (p ^ (n - x))) 0 then HPow.hPow (α := R) (↑p : R) x else 0) 0
Tactic: simp only [wittPolynomial, map_sum, constantCoeff_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
n : ℕ
⊢ Eq.{u_1 + 1} (α := R)
    (∑ x ∈ range (n + 1), if Eq (α := ℕ →₀ ℕ) (single x (p ^ (n - x))) 0 then HPow.hPow (α := R) (↑p : R) x else 0) 0
have rw : ∀ x ∈ range (n + 1), (if Eq (α := ℕ →₀ ℕ) (single x (p ^ (n - x))) 0 then HPow.hPow (α := R) (↑p : R) x else 0) = 0
Tactic: rw [sum_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
n i : ℕ
h : i ∈ range (n + 1)
⊢ (if Eq (α := ℕ →₀ ℕ) (single i (p ^ (n - i))) 0 then HPow.hPow (α := R) (↑p : R) i else 0) = 0
have hnc : ¬Eq (α := ℕ →₀ ℕ) (single i (p ^ (n - i))) 0
Tactic: rw [if_neg]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
n i : ℕ
h : i ∈ range (n + 1)
⊢ ¬Eq (α := ℕ →₀ ℕ) (single i (p ^ (n - i))) 0
have hnc : ¬p ^ (n - i) = 0
Tactic: rw [Finsupp.single_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p n : ℕ
⊢ Eq (α := MvPolynomial ℕ (ZMod (p ^ (n + 1)))) (W_ (ZMod (p ^ (n + 1))) (n + 1))
    ((expand p : (a : MvPolynomial ℕ (ZMod (p ^ (n + 1)))) → MvPolynomial ℕ (ZMod (p ^ (n + 1))))
      (W_ (ZMod (p ^ (n + 1))) n))
have simp : Eq (α := MvPolynomial ℕ (ZMod (p ^ (n + 1))))
  (∑ i ∈ range (n + 1 + 1),
    HMul.hMul (α := MvPolynomial ℕ (ZMod (p ^ (n + 1))))
      ((C : (a : ZMod (p ^ (n + 1))) → MvPolynomial ℕ (ZMod (p ^ (n + 1))))
          (HPow.hPow (α := ZMod (p ^ (n + 1))) (↑p : ZMod (p ^ (n + 1))) i) :
        MvPolynomial ℕ (ZMod (p ^ (n + 1))))
      (HPow.hPow (α := MvPolynomial ℕ (ZMod (p ^ (n + 1)))) (X i) (p ^ (n + 1 - i))))
  ((expand p : (a : MvPolynomial ℕ (ZMod (p ^ (n + 1)))) → MvPolynomial ℕ (ZMod (p ^ (n + 1))))
    (∑ i ∈ range (n + 1),
      HMul.hMul (α := MvPolynomial ℕ (ZMod (p ^ (n + 1))))
        ((C : (a : ZMod (p ^ (n + 1))) → MvPolynomial ℕ (ZMod (p ^ (n + 1))))
            (HPow.hPow (α := ZMod (p ^ (n + 1))) (↑p : ZMod (p ^ (n + 1))) i) :
          MvPolynomial ℕ (ZMod (p ^ (n + 1))))
        (HPow.hPow (α := MvPolynomial ℕ (ZMod (p ^ (n + 1)))) (X i) (p ^ (n - i)))))
Tactic: simp only [wittPolynomial_eq_sum_C_mul_X_pow]