awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℕ → ℤ
hn : ¬n = 0
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))) :
        ℤ)
⊢ 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:
obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hn

Premises used: Nat.exists_eq_succ_of_ne_zero, rfl
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
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)) :
      ℤ)
⊢ 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:
rw [Nat.succ_eq_add_one, add_tsub_cancel_right]

Premises used: Nat.succ_eq_add_one, add_tsub_cancel_right
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
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) : ℤ)
⊢ 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:
simp only [map_mul]

Premises used: map_mul
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
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) : ℤ)
⊢ (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:
rw [map_natCast, hom_bind₁]

Premises used: map_natCast, MvPolynomial.hom_bind₁
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
apply :
  Eq (α := ℕ → ℤ) (fun (i : ℕ) ↦ (MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (verschiebungPoly i))
    (coeff (p := p) ((verschiebung : (a : 𝕎 ℤ) → 𝕎 ℤ) (mk p x)))
⊢ 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:
apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl

Premises used: MvPolynomial.eval₂Hom_congr, RingHom.ext_int, rfl
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
h :
  ∀ (k : ℕ),
    Eq (α := ℤ) ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (verschiebungPoly k) : ℤ)
      (coeff (p := p) ((verschiebung : (a : 𝕎 ℤ) → 𝕎 ℤ) (mk p x)) k : ℤ)
⊢ Eq (α := ℕ → ℤ) (fun (i : ℕ) ↦ (MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (verschiebungPoly i))
    (coeff (p := p) ((verschiebung : (a : 𝕎 ℤ) → 𝕎 ℤ) (mk p x)))

Tactic:
funext k
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
k : ℕ
h :
  Eq (α := ℤ) ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (verschiebungPoly k) : ℤ)
    ((aeval (mk p x).coeff : (a : MvPolynomial ℕ ℤ) → ℤ) (verschiebungPoly k) : ℤ)
⊢ Eq (α := ℤ) ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (verschiebungPoly k) : ℤ)
    (coeff (p := p) ((verschiebung : (a : 𝕎 ℤ) → 𝕎 ℤ) (mk p x)) k : ℤ)

Tactic:
simp only [← aeval_verschiebungPoly]

Premises used: WittVector.aeval_verschiebungPoly
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
k : ℕ
⊢ Eq (α := ℤ) ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (verschiebungPoly k) : ℤ)
    ((aeval (mk p x).coeff : (a : MvPolynomial ℕ ℤ) → ℤ) (verschiebungPoly k) : ℤ)

Tactic:
eval₂Hom_congr (RingHom.ext_int _ _) rfl rfl

Premises used: MvPolynomial.eval₂Hom_congr, RingHom.ext_int, rfl
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
k : ℕ
⊢ Eq (α := ℤ) ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (verschiebungPoly k) : ℤ)
    ((aeval (mk p x).coeff : (a : MvPolynomial ℕ ℤ) → ℤ) (verschiebungPoly k) : ℤ)

Tactic:
exact eval₂Hom_congr (RingHom.ext_int _ _) rfl rfl

Premises used: MvPolynomial.eval₂Hom_congr, RingHom.ext_int, rfl
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
rw :
  HMul.hMul (α := ℤ) (β := ℤ) ((↑p : ℤ) : ℤ) ((ghostComponent n : (a : 𝕎 ℤ) → ℤ) (mk p x) : ℤ) =
    HMul.hMul (α := ℤ) (β := ℤ) ((↑p : ℤ) : ℤ)
      ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (wittPolynomial p ℤ n) : ℤ)
⊢ (ghostComponent (n + 1) : (a : 𝕎 ℤ) → ℤ) ((verschiebung : (a : 𝕎 ℤ) → 𝕎 ℤ) (mk p x) : 𝕎 ℤ) =
    HMul.hMul (α := ℤ) (β := ℤ) ((↑p : ℤ) : ℤ)
      ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (wittPolynomial p ℤ n) : ℤ)

Tactic:
rw [ghostComponent_verschiebung]

Premises used: WittVector.ghostComponent_verschiebung
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
⊢ HMul.hMul (α := ℤ) (β := ℤ) ((↑p : ℤ) : ℤ) ((ghostComponent n : (a : 𝕎 ℤ) → ℤ) (mk p x) : ℤ) =
    HMul.hMul (α := ℤ) (β := ℤ) ((↑p : ℤ) : ℤ)
      ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (wittPolynomial p ℤ n) : ℤ)

Tactic:
rfl
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
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) : 𝕎 ℤ) : ℤ)
_₁ :
  (ghostComponent (n + 1) : (a : 𝕎 ℤ) → ℤ) ((verschiebung : (a : 𝕎 ℤ) → 𝕎 ℤ) (mk p x) : 𝕎 ℤ) =
    HMul.hMul (α := ℤ) (β := ℤ) ((↑p : ℤ) : ℤ)
      ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (wittPolynomial p ℤ n) : ℤ)
⊢ (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:
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

Premises used: WittVector.mk, WittVector.ghostComponent, HAdd.hAdd, OfNat.ofNat, DFunLike.coe, WittVector.verschiebung
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
n : ℕ
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)))
⊢ 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))))

Tactic:
apply sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
n i : ℕ
rw : HPow.hPow (α := MvPolynomial ℕ R) (β := ℕ) (X i) 0 = 1
⊢ (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)))

Tactic:
rw [monomial_eq, Finsupp.prod_single_index]

Premises used: MvPolynomial.monomial_eq, Finsupp.prod_single_index
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
n i : ℕ
rw rw₁ : Eq.{u_1 + 1} (α := MvPolynomial ℕ R) 1 1
⊢ HPow.hPow (α := MvPolynomial ℕ R) (β := ℕ) (X i) 0 = 1

Tactic:
rw [pow_zero]

Premises used: pow_zero
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
n : ℕ
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))
⊢ 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)

Tactic:
rw [wittPolynomial, map_sum, wittPolynomial]

Premises used: wittPolynomial, map_sum
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
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))

Tactic:
sum_congr rfl fun i _ => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
n : ℕ
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)
⊢ 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:
refine sum_congr rfl fun i _ => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
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)
rw₂ 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)
⊢ 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:
rw [map_monomial, map_pow, map_natCast]

Premises used: map_pow, MvPolynomial.map_monomial, map_natCast
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
n : ℕ
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
⊢ Eq (α := R) ((constantCoeff : (a : MvPolynomial ℕ R) → R) (W_ R n) : R) (0 : R)

Tactic:
simp only [wittPolynomial, map_sum, constantCoeff_monomial]

Premises used: wittPolynomial, map_sum, MvPolynomial.constantCoeff_monomial
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
n : ℕ
rw : ∀ x ∈ range (n + 1), (if Eq (α := ℕ →₀ ℕ) (single x (p ^ (n - x))) 0 then HPow.hPow (α := R) (↑p : R) x else 0) = 0
⊢ 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:
rw [sum_eq_zero]

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
n i : ℕ
h : i ∈ range (n + 1)
hnc : ¬Eq (α := ℕ →₀ ℕ) (single i (p ^ (n - i))) 0
⊢ (if Eq (α := ℕ →₀ ℕ) (single i (p ^ (n - i))) 0 then HPow.hPow (α := R) (↑p : R) i else 0) = 0

Tactic:
rw [if_neg]

Premises used: if_neg
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
n i : ℕ
h : i ∈ range (n + 1)
hnc : ¬p ^ (n - i) = 0
⊢ ¬Eq (α := ℕ →₀ ℕ) (single i (p ^ (n - i))) 0

Tactic:
rw [Finsupp.single_eq_zero]

Premises used: Finsupp.single_eq_zero
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
n i : ℕ
h : i ∈ range (n + 1)
⊢ ¬p ^ (n - i) = 0

Tactic:
ne_of_gt (pow_pos hp.1.pos _)

Premises used: pow_pos, ne_of_gt, Nat.Prime.pos, Fact.out
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
n i : ℕ
h : i ∈ range (n + 1)
⊢ ¬p ^ (n - i) = 0

Tactic:
exact ne_of_gt (pow_pos hp.1.pos _)

Premises used: pow_pos, ne_of_gt, Nat.Prime.pos, Fact.out
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
⊢ Eq (α := MvPolynomial ℕ R) (W_ R 0) (X 0)

Tactic:
simp only [wittPolynomial, X, sum_singleton, range_one, pow_zero, zero_add, tsub_self]

Premises used: wittPolynomial, tsub_self, MvPolynomial.X, zero_add, pow_zero, Finset.sum_singleton, Finset.range_one
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
⊢ W_ R 1 =
    HMul.hMul (α := MvPolynomial ℕ R) ((C : (a : R) → MvPolynomial ℕ R) (↑p : R)) (X 1) +
      HPow.hPow (α := MvPolynomial ℕ R) (X 0) p

Tactic:
simp only [wittPolynomial_eq_sum_C_mul_X_pow, sum_range_succ_comm, range_one, sum_singleton,
    one_mul, pow_one, C_1, pow_zero, tsub_self, tsub_zero]

Premises used: tsub_self, Finset.sum_range_succ_comm, MvPolynomial.C_1, pow_zero, Finset.sum_singleton, tsub_zero, pow_one, Finset.range_one, wittPolynomial_eq_sum_C_mul_X_pow, one_mul
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
f : ℕ → A
n : ℕ
⊢ Eq.{u_3 + 1} (α := A) ((aeval f : (a : MvPolynomial ℕ R) → A) (W_ R n) : A)
    (∑ i ∈ range (n + 1), HPow.hPow (α := A) (↑p : A) i * f i ^ p ^ (n - i) : A)

Tactic:
simp [wittPolynomial, map_sum, aeval_monomial, Finsupp.prod_single_index]

Premises used: wittPolynomial, map_sum, MvPolynomial.aeval_monomial, Finsupp.prod_single_index
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p n : ℕ
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)))))
⊢ 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))

Tactic:
simp only [wittPolynomial_eq_sum_C_mul_X_pow]

Premises used: wittPolynomial_eq_sum_C_mul_X_pow
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p n : ℕ
rw :
  ∀ x ∈ 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))) x) :
          MvPolynomial ℕ (ZMod (p ^ (n + 1))))
        (HPow.hPow (α := MvPolynomial ℕ (ZMod (p ^ (n + 1)))) (X x) (p ^ (n + 1 - x))) =
      (expand p : (a : MvPolynomial ℕ (ZMod (p ^ (n + 1)))) → MvPolynomial ℕ (ZMod (p ^ (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))) x) :
            MvPolynomial ℕ (ZMod (p ^ (n + 1))))
          (HPow.hPow (α := MvPolynomial ℕ (ZMod (p ^ (n + 1)))) (X x) (p ^ (n - x))))
⊢ 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:
rw [sum_range_succ, ← Nat.cast_pow, CharP.cast_eq_zero (ZMod (p ^ (n + 1))) (p ^ (n + 1)), C_0,
    zero_mul, add_zero, map_sum, sum_congr rfl]

Premises used: CharP.cast_eq_zero, MulZeroClass.zero_mul, MvPolynomial.C_0, map_sum, ZMod, HPow.hPow, HAdd.hAdd, Nat.cast_pow, add_zero, OfNat.ofNat, Finset.sum_range_succ, Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p n k : ℕ
hk : k ∈ range (n + 1)
rw :
  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))) k) :
        MvPolynomial ℕ (ZMod (p ^ (n + 1))))
      (HPow.hPow (α := MvPolynomial ℕ (ZMod (p ^ (n + 1)))) (X k) (p ^ (n + 1 - k))) =
    HMul.hMul (α := MvPolynomial ℕ (ZMod (p ^ (n + 1))))
      ((algebraMap (ZMod (p ^ (n + 1))) (MvPolynomial ℕ (ZMod (p ^ (n + 1)))) :
            (a : ZMod (p ^ (n + 1))) → MvPolynomial ℕ (ZMod (p ^ (n + 1))))
          (HPow.hPow (α := ZMod (p ^ (n + 1))) (↑p : ZMod (p ^ (n + 1))) k) :
        MvPolynomial ℕ (ZMod (p ^ (n + 1))))
      (HPow.hPow (α := MvPolynomial ℕ (ZMod (p ^ (n + 1)))) (X k) (p ^ (n - k + 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))) k) :
        MvPolynomial ℕ (ZMod (p ^ (n + 1))))
      (HPow.hPow (α := MvPolynomial ℕ (ZMod (p ^ (n + 1)))) (X k) (p ^ (n + 1 - k))) =
    (expand p : (a : MvPolynomial ℕ (ZMod (p ^ (n + 1)))) → MvPolynomial ℕ (ZMod (p ^ (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))) k) :
          MvPolynomial ℕ (ZMod (p ^ (n + 1))))
        (HPow.hPow (α := MvPolynomial ℕ (ZMod (p ^ (n + 1)))) (X k) (p ^ (n - k))))

Tactic:
rw [map_mul (expand p), map_pow (expand p), expand_X, algHom_C, ← pow_mul, ← pow_succ']

Premises used: MvPolynomial.expand_X, map_pow, MvPolynomial.algHom_C, pow_mul, map_mul, MvPolynomial.expand, pow_succ'