awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
idx : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun (n : ℕ) ↦ peval (φ n) ![x.coeff, y.coeff]
R_1 : Type u_2
inst_2 : CommRing R_1
x : 𝕎 R_1
n : ℕ
h :
  Eq.{u_2 + 1} (α := R_1)
    (((aeval.{0, u_2, 0} (R := ℤ) (S₁ := R_1) fun (a : Fin 2 × ℕ) ↦ ![x.coeff, x.coeff] a.1 a.2 :
            MvPolynomial (Fin 2 × ℕ) ℤ →ₐ[ℤ] R_1) :
          (a : MvPolynomial (Fin 2 × ℕ) ℤ) → R_1)
        (φ n) :
      R_1)
    (((aeval.{0, u_2, 0} (R := ℤ) (S₁ := R_1) fun (i : Fin (Nat.succ 0).succ × ℕ) ↦
              ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1)
                (![X, X] i.1 i.2 : MvPolynomial ℕ ℤ) :
            MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ →ₐ[ℤ] R_1) :
          (a : MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ) → R_1)
        (φ n) :
      R_1)
⊢ (f x x).coeff n =
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1)
      ((fun (n : ℕ) ↦
          ((bind₁ (uncurry ![X, X]) : (a : MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ) → MvPolynomial ℕ ℤ) (φ n) :
            MvPolynomial ℕ ℤ))
        n)

Tactic:
simp +unfoldPartialApp only [hf, peval, uncurry, aeval_bind₁]

Premises used: WittVector.peval, MvPolynomial.aeval_bind₁, Function.uncurry
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
idx : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun (n : ℕ) ↦ peval (φ n) ![x.coeff, y.coeff]
R_1 : Type u_2
inst_2 : CommRing R_1
x : 𝕎 R_1
n : ℕ
apply :
  Eq.{max 1 (u_2 + 1)} (α := Fin 2 × ℕ → R_1) (fun (a : Fin 2 × ℕ) ↦ ![x.coeff, x.coeff] a.1 a.2)
    fun (i : Fin (Nat.succ 0).succ × ℕ) ↦
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1)
      (![X, X] i.1 i.2 : MvPolynomial ℕ ℤ)
⊢ Eq.{u_2 + 1} (α := R_1)
    (((aeval.{0, u_2, 0} (R := ℤ) (S₁ := R_1) fun (a : Fin 2 × ℕ) ↦ ![x.coeff, x.coeff] a.1 a.2 :
            MvPolynomial (Fin 2 × ℕ) ℤ →ₐ[ℤ] R_1) :
          (a : MvPolynomial (Fin 2 × ℕ) ℤ) → R_1)
        (φ n) :
      R_1)
    (((aeval.{0, u_2, 0} (R := ℤ) (S₁ := R_1) fun (i : Fin (Nat.succ 0).succ × ℕ) ↦
              ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1)
                (![X, X] i.1 i.2 : MvPolynomial ℕ ℤ) :
            MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ →ₐ[ℤ] R_1) :
          (a : MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ) → R_1)
        (φ n) :
      R_1)

Tactic:
apply eval₂Hom_congr rfl _ rfl

Premises used: MvPolynomial.eval₂Hom_congr, rfl
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
idx : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun (n : ℕ) ↦ peval (φ n) ![x.coeff, y.coeff]
R_1 : Type u_2
inst_2 : CommRing R_1
x : 𝕎 R_1
n : ℕ
h :
  ∀ (i : Fin 2) (k : ℕ),
    ![x.coeff, x.coeff] (i, k).1 (i, k).2 =
      ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1)
        (![X, X] (i, k).1 (i, k).2 : MvPolynomial ℕ ℤ)
⊢ Eq.{max 1 (u_2 + 1)} (α := Fin 2 × ℕ → R_1) (fun (a : Fin 2 × ℕ) ↦ ![x.coeff, x.coeff] a.1 a.2)
    fun (i : Fin (Nat.succ 0).succ × ℕ) ↦
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1)
      (![X, X] i.1 i.2 : MvPolynomial ℕ ℤ)

Tactic:
ext ⟨i, k⟩
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
idx : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun (n : ℕ) ↦ peval (φ n) ![x.coeff, y.coeff]
R_1 : Type u_2
inst_2 : CommRing R_1
x : 𝕎 R_1
n : ℕ
i : Fin 2
k : ℕ
h :
  ![x.coeff, x.coeff] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2), k).1 ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2), k).2 =
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1)
      (![X, X] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2), k).1 ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩, k).2 : MvPolynomial ℕ ℤ)
h₁ :
  ![x.coeff, x.coeff] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2), k).1 ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2), k).2 =
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1)
      (![X, X] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2), k).1 ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩, k).2 : MvPolynomial ℕ ℤ)
⊢ ![x.coeff, x.coeff] (i, k).1 (i, k).2 =
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1)
      (![X, X] (i, k).1 (i, k).2 : MvPolynomial ℕ ℤ)

Tactic:
fin_cases i
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
idx : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun (n : ℕ) ↦ peval (φ n) ![x.coeff, y.coeff]
R_1 : Type u_2
inst_2 : CommRing R_1
x : 𝕎 R_1
n k : ℕ
⊢ ![x.coeff, x.coeff] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2), k).1 ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2), k).2 =
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1)
      (![X, X] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2), k).1 ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩, k).2 : MvPolynomial ℕ ℤ)

Tactic:
simp
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
idx : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun (n : ℕ) ↦ peval (φ n) ![x.coeff, y.coeff]
R_1 : Type u_2
inst_2 : CommRing R_1
x : 𝕎 R_1
n k : ℕ
⊢ ![x.coeff, x.coeff] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2), k).1 ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2), k).2 =
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1)
      (![X, X] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2), k).1 ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩, k).2 : MvPolynomial ℕ ℤ)

Tactic:
simp
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
idx : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
R_1 : Type u_2
inst_3 : CommRing R_1
x : 𝕎 R_1
h :
  ∀ (n : ℕ),
    (-x).coeff n =
      ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1)
        ((fun (n : ℕ) ↦
            ((rename Prod.snd : (a : MvPolynomial (Fin 1 × ℕ) ℤ) → MvPolynomial ℕ ℤ) (wittNeg p n) : MvPolynomial ℕ ℤ))
          n)
⊢ (-x).coeff = fun (n : ℕ) ↦
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1)
      ((fun (n : ℕ) ↦
          ((rename Prod.snd : (a : MvPolynomial (Fin 1 × ℕ) ℤ) → MvPolynomial ℕ ℤ) (wittNeg p n) : MvPolynomial ℕ ℤ))
        n)

Tactic:
funext n
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
idx : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
R_1 : Type u_2
inst_3 : CommRing R_1
x : 𝕎 R_1
n : ℕ
h :
  peval (wittNeg p n) ![x.coeff] =
    (eval₂Hom (algebraMap ℤ R_1) (x.coeff ∘ Prod.snd) : (a : MvPolynomial (Fin 1 × ℕ) ℤ) → R_1) (wittNeg p n)
⊢ (-x).coeff n =
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1)
      ((fun (n : ℕ) ↦
          ((rename Prod.snd : (a : MvPolynomial (Fin 1 × ℕ) ℤ) → MvPolynomial ℕ ℤ) (wittNeg p n) : MvPolynomial ℕ ℤ))
        n)

Tactic:
rw [neg_coeff, aeval_eq_eval₂Hom, eval₂Hom_rename]

Premises used: MvPolynomial.eval₂Hom_rename, MvPolynomial.aeval_eq_eval₂Hom, WittVector.neg_coeff
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
idx : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
R_1 : Type u_2
inst_3 : CommRing R_1
x : 𝕎 R_1
n : ℕ
apply : uncurry ![x.coeff] = x.coeff ∘ Prod.snd
⊢ peval (wittNeg p n) ![x.coeff] =
    (eval₂Hom (algebraMap ℤ R_1) (x.coeff ∘ Prod.snd) : (a : MvPolynomial (Fin 1 × ℕ) ℤ) → R_1) (wittNeg p n)

Tactic:
apply eval₂Hom_congr rfl _ rfl

Premises used: MvPolynomial.eval₂Hom_congr, rfl
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
idx : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
R_1 : Type u_2
inst_3 : CommRing R_1
x : 𝕎 R_1
n : ℕ
h : ∀ (i : Fin 1) (k : ℕ), uncurry ![x.coeff] (i, k) = (x.coeff ∘ Prod.snd) (i, k)
⊢ uncurry ![x.coeff] = x.coeff ∘ Prod.snd

Tactic:
ext ⟨i, k⟩
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
idx : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
R_1 : Type u_2
inst_3 : CommRing R_1
x : 𝕎 R_1
n : ℕ
i : Fin 1
k : ℕ
h :
  uncurry ![x.coeff] ((fun (i : Fin 1) ↦ i) (⟨0, ⋯⟩ : Fin 1), k) =
    Function.comp (α := Fin 1 × ℕ) x.coeff Prod.snd ((fun (i : Fin 1) ↦ i) ⟨0, ⋯⟩, k)
⊢ uncurry ![x.coeff] (i, k) = (x.coeff ∘ Prod.snd) (i, k)

Tactic:
fin_cases i
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
idx : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
R_1 : Type u_2
inst_3 : CommRing R_1
x : 𝕎 R_1
n k : ℕ
⊢ uncurry ![x.coeff] ((fun (i : Fin 1) ↦ i) (⟨0, ⋯⟩ : Fin 1), k) =
    Function.comp (α := Fin 1 × ℕ) x.coeff Prod.snd ((fun (i : Fin 1) ↦ i) ⟨0, ⋯⟩, k)

Tactic:
rfl
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
idx : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
R_1 : Type u_2
inst_3 : CommRing R_1
x : 𝕎 R_1
h :
  ∀ (n : ℕ),
    Eq (α := R_1) (coeff (p := p) 0 n : R_1)
      (((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1) (0 n) : R_1)
⊢ Eq.{u_2 + 1} (α := ℕ → R_1) (coeff (p := p) 0) fun (n : ℕ) ↦
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1) (0 n)

Tactic:
funext n
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
idx : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
R_1 : Type u_2
inst_3 : CommRing R_1
x : 𝕎 R_1
n : ℕ
⊢ Eq (α := R_1) (coeff (p := p) 0 n : R_1)
    (((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1) (0 n) : R_1)

Tactic:
simp only [Pi.zero_apply, map_zero, zero_coeff]

Premises used: Pi.zero_apply, map_zero, WittVector.zero_coeff
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R : Type u
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
n : ℕ
rw :
  Eq (α := MvPolynomial ℕ R)
    ((aeval 0 : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (wittPolynomial p R n) : MvPolynomial ℕ R)
    (0 : MvPolynomial ℕ R)
rw₁ :
  Eq (α := MvPolynomial ℕ R)
    ((algebraMap R (MvPolynomial ℕ R) : (a : R) → MvPolynomial ℕ R)
        ((MvPolynomial.constantCoeff : (a : MvPolynomial ℕ R) → R) (wittPolynomial p R n)) :
      MvPolynomial ℕ R)
    (0 : MvPolynomial ℕ R)
rw₂ : Eq (α := MvPolynomial ℕ R) ((algebraMap R (MvPolynomial ℕ R) : (a : R) → MvPolynomial ℕ R) 0) 0
rw₃ rw₄ : Eq.{u + 1} (α := MvPolynomial ℕ R) 0 0
⊢ Eq (α := MvPolynomial ℕ R)
    ((bind₁ 0 : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (wittPolynomial p R n) : MvPolynomial ℕ R)
    (0 : MvPolynomial ℕ R)

Tactic:
rw [← aeval_eq_bind₁, aeval_zero, constantCoeff_wittPolynomial, map_zero]

Premises used: map_zero, constantCoeff_wittPolynomial, MvPolynomial.aeval_zero, MvPolynomial.aeval_eq_bind₁
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
rw :
  Eq (α := MvPolynomial ℕ ℤ)
    ((bind₁ onePoly : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ)
        (HMul.hMul (α := MvPolynomial ℕ ℤ)
          ((C : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 0) : MvPolynomial ℕ ℤ)
          (HPow.hPow (α := MvPolynomial ℕ ℤ) (X 0) (p ^ (n - 0)))) :
      MvPolynomial ℕ ℤ)
    (1 : MvPolynomial ℕ ℤ)
h₀ :
  ∀ b ∈ Finset.range (n + 1),
    b ≠ 0 →
      Eq (α := MvPolynomial ℕ ℤ)
        ((bind₁ onePoly : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ)
            (HMul.hMul (α := MvPolynomial ℕ ℤ)
              ((C : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) b) : MvPolynomial ℕ ℤ)
              (HPow.hPow (α := MvPolynomial ℕ ℤ) (X b) (p ^ (n - b)))) :
          MvPolynomial ℕ ℤ)
        (0 : MvPolynomial ℕ ℤ)
h₁ :
  0 ∉ Finset.range (n + 1) →
    Eq (α := MvPolynomial ℕ ℤ)
      ((bind₁ onePoly : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ)
          (HMul.hMul (α := MvPolynomial ℕ ℤ)
            ((C : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 0) : MvPolynomial ℕ ℤ)
            (HPow.hPow (α := MvPolynomial ℕ ℤ) (X 0) (p ^ (n - 0)))) :
        MvPolynomial ℕ ℤ)
      (0 : MvPolynomial ℕ ℤ)
⊢ Eq (α := MvPolynomial ℕ ℤ)
    ((bind₁ onePoly : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n) : MvPolynomial ℕ ℤ)
    (1 : MvPolynomial ℕ ℤ)

Tactic:
rw [wittPolynomial_eq_sum_C_mul_X_pow, map_sum, Finset.sum_eq_single 0]

Premises used: map_sum, Finset.sum_eq_single, OfNat.ofNat, wittPolynomial_eq_sum_C_mul_X_pow
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ Eq (α := MvPolynomial ℕ ℤ)
    ((bind₁ onePoly : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ)
        (HMul.hMul (α := MvPolynomial ℕ ℤ)
          ((C : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 0) : MvPolynomial ℕ ℤ)
          (HPow.hPow (α := MvPolynomial ℕ ℤ) (X 0) (p ^ (n - 0)))) :
      MvPolynomial ℕ ℤ)
    (1 : MvPolynomial ℕ ℤ)

Tactic:
simp only [onePoly, one_pow, one_mul, map_pow, C_1, pow_zero, bind₁_X_right, if_true]

Premises used: one_pow, if_true, MvPolynomial.C_1, map_pow, pow_zero, WittVector.onePoly, MvPolynomial.bind₁_X_right, one_mul
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n i : ℕ
_hi : i ∈ Finset.range (n + 1)
hi0 : i ≠ 0
⊢ Eq (α := MvPolynomial ℕ ℤ)
    ((bind₁ onePoly : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ)
        (HMul.hMul (α := MvPolynomial ℕ ℤ)
          ((C : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) i) : MvPolynomial ℕ ℤ)
          (HPow.hPow (α := MvPolynomial ℕ ℤ) (X i) (p ^ (n - i)))) :
      MvPolynomial ℕ ℤ)
    (0 : MvPolynomial ℕ ℤ)

Tactic:
simp only [onePoly, if_neg hi0, zero_pow (pow_ne_zero _ hp.1.ne_zero), mul_zero, map_pow,
      bind₁_X_right, map_mul]

Premises used: pow_ne_zero, map_pow, MulZeroClass.mul_zero, map_mul, WittVector.onePoly, Nat.Prime.ne_zero, MvPolynomial.bind₁_X_right, if_neg, zero_pow, Fact.out
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ 0 ∉ Finset.range (n + 1) →
    Eq (α := MvPolynomial ℕ ℤ)
      ((bind₁ onePoly : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ)
          (HMul.hMul (α := MvPolynomial ℕ ℤ)
            ((C : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 0) : MvPolynomial ℕ ℤ)
            (HPow.hPow (α := MvPolynomial ℕ ℤ) (X 0) (p ^ (n - 0)))) :
        MvPolynomial ℕ ℤ)
      (0 : MvPolynomial ℕ ℤ)

Tactic:
simp
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
idx : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
R_1 : Type u_2
inst_3 : CommRing R_1
x : 𝕎 R_1
h :
  ∀ (n : ℕ),
    Eq (α := R_1) (coeff (p := p) 1 n : R_1)
      (((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1) (onePoly n) : R_1)
⊢ Eq.{u_2 + 1} (α := ℕ → R_1) (coeff (p := p) 1) fun (n : ℕ) ↦
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1) (onePoly n)

Tactic:
funext n
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
idx : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
R_1 : Type u_2
inst_3 : CommRing R_1
x : 𝕎 R_1
n : ℕ
h :
  Eq (α := R_1) (coeff (p := p) 1 0 : R_1)
    (((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1) (onePoly 0) : R_1)
h₁ :
  ∀ (n : ℕ),
    Eq (α := R_1) (coeff (p := p) 1 (n + 1) : R_1)
      (((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1) (onePoly (n + 1)) : R_1)
⊢ Eq (α := R_1) (coeff (p := p) 1 n : R_1)
    (((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1) (onePoly n) : R_1)

Tactic:
cases n
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
idx : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
R_1 : Type u_2
inst_3 : CommRing R_1
x : 𝕎 R_1
⊢ Eq (α := R_1) (coeff (p := p) 1 0 : R_1)
    (((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1) (onePoly 0) : R_1)

Tactic:
simp only [one_coeff_zero, onePoly, ite_true, map_one]

Premises used: ite_true, WittVector.one_coeff_zero, map_one, WittVector.onePoly
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
idx : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
R_1 : Type u_2
inst_3 : CommRing R_1
x : 𝕎 R_1
n : ℕ
⊢ Eq (α := R_1) (coeff (p := p) 1 (n + 1) : R_1)
    (((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1) (onePoly (n + 1)) : R_1)

Tactic:
simp only [Nat.succ_pos', one_coeff_eq_of_pos, onePoly, Nat.succ_ne_zero, ite_false,
          map_zero]

Premises used: Nat.succ_pos', ite_false, map_zero, Nat.succ_ne_zero, WittVector.onePoly, WittVector.one_coeff_eq_of_pos
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
idx : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
R_1 : Type u_2
inst_3 : CommRing R_1
x y : 𝕎 R_1
h : ∀ (x_1 : ℕ), (x + y).coeff x_1 = peval (wittAdd p x_1) ![x.coeff, y.coeff]
⊢ (x + y).coeff = fun (n : ℕ) ↦ peval (wittAdd p n) ![x.coeff, y.coeff]

Tactic:
ext
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
idx : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
R_1 : Type u_2
inst_3 : CommRing R_1
x y : 𝕎 R_1
x_1 : ℕ
⊢ (x + y).coeff x_1 = peval (wittAdd p x_1) ![x.coeff, y.coeff]

Tactic:
add_coeff _ _ _

Premises used: WittVector.add_coeff
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
idx : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
R_1 : Type u_2
inst_3 : CommRing R_1
x y : 𝕎 R_1
x_1 : ℕ
⊢ (x + y).coeff x_1 = peval (wittAdd p x_1) ![x.coeff, y.coeff]

Tactic:
exact add_coeff _ _ _

Premises used: WittVector.add_coeff
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
idx : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
R_1 : Type u_2
inst_3 : CommRing R_1
x y : 𝕎 R_1
h : ∀ (x_1 : ℕ), (x * y).coeff x_1 = peval (wittMul p x_1) ![x.coeff, y.coeff]
⊢ (x * y).coeff = fun (n : ℕ) ↦ peval (wittMul p n) ![x.coeff, y.coeff]

Tactic:
ext
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
idx : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
R_1 : Type u_2
inst_3 : CommRing R_1
x y : 𝕎 R_1
x_1 : ℕ
⊢ (x * y).coeff x_1 = peval (wittMul p x_1) ![x.coeff, y.coeff]

Tactic:
mul_coeff _ _ _

Premises used: WittVector.mul_coeff
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
idx : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
R_1 : Type u_2
inst_3 : CommRing R_1
x y : 𝕎 R_1
x_1 : ℕ
⊢ (x * y).coeff x_1 = peval (wittMul p x_1) ![x.coeff, y.coeff]

Tactic:
exact mul_coeff _ _ _

Premises used: WittVector.mul_coeff
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R
hf : IsPoly p f
g : R →+* S
x : 𝕎 R
obtain :
  ∀ (φ : ℕ → MvPolynomial ℕ ℤ)
    (hf :
      ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R),
        (f x).coeff = fun (n : ℕ) ↦ (aeval x.coeff : (a : MvPolynomial ℕ ℤ) → R) (φ n)),
    Eq (α := 𝕎 S) ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) (f x) : 𝕎 S) (f ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) x) : 𝕎 S)
⊢ Eq (α := 𝕎 S) ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) (f x) : 𝕎 S) (f ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) x) : 𝕎 S)

Tactic:
obtain ⟨φ, hf⟩ := hf
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R
g : R →+* S
x : 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf :
  ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R),
    (f x).coeff = fun (n : ℕ) ↦ (aeval x.coeff : (a : MvPolynomial ℕ ℤ) → R) (φ n)
h :
  ∀ (n : ℕ),
    Eq.{u + 1} (α := S) (coeff (p := p) ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) (f x)) n)
      (coeff (f ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) x)) n)
⊢ Eq (α := 𝕎 S) ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) (f x) : 𝕎 S) (f ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) x) : 𝕎 S)

Tactic:
ext n
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R
g : R →+* S
x : 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf :
  ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R),
    (f x).coeff = fun (n : ℕ) ↦ (aeval x.coeff : (a : MvPolynomial ℕ ℤ) → R) (φ n)
n : ℕ
h : Eq (α := S) ((g : (a : R) → S) ((f x).coeff n) : S) (coeff (f ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) x)) n : S)
h₁ :
  Eq (α := S)
    ((g : (a : R) → S) (((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (φ n) : R) :
      S)
    (((aeval.{0, u, 0} (R := ℤ) (S₁ := S) (coeff (p := p) ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) x)) :
            MvPolynomial ℕ ℤ →ₐ[ℤ] S) :
          (a : MvPolynomial ℕ ℤ) → S)
        (φ n) :
      S)
h₂ :
  Eq (α := S)
    ((eval₂Hom (g.comp (algebraMap ℤ R)) fun (i : ℕ) ↦ (g : (a : R) → S) (x.coeff i) : (a : MvPolynomial ℕ ℤ) → S)
        (φ n) :
      S)
    (((aeval.{0, u, 0} (R := ℤ) (S₁ := S) (coeff (p := p) ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) x)) :
            MvPolynomial ℕ ℤ →ₐ[ℤ] S) :
          (a : MvPolynomial ℕ ℤ) → S)
        (φ n) :
      S)
h₃ :
  Eq (α := S)
    ((eval₂Hom (g.comp (algebraMap ℤ R)) fun (i : ℕ) ↦ (g : (a : R) → S) (x.coeff i) : (a : MvPolynomial ℕ ℤ) → S)
        (φ n) :
      S)
    (((aeval.{0, u, 0} (R := ℤ) (S₁ := S) fun (i : ℕ) ↦ (g : (a : R) → S) (x.coeff i) : MvPolynomial ℕ ℤ →ₐ[ℤ] S) :
          (a : MvPolynomial ℕ ℤ) → S)
        (φ n) :
      S)
h₄ :
  Eq (α := S)
    ((eval₂Hom (algebraMap ℤ S) fun (i : ℕ) ↦ (g : (a : R) → S) (x.coeff i) : (a : MvPolynomial ℕ ℤ) → S) (φ n) : S)
    (((aeval.{0, u, 0} (R := ℤ) (S₁ := S) fun (i : ℕ) ↦ (g : (a : R) → S) (x.coeff i) : MvPolynomial ℕ ℤ →ₐ[ℤ] S) :
          (a : MvPolynomial ℕ ℤ) → S)
        (φ n) :
      S)
⊢ Eq.{u + 1} (α := S) (coeff (p := p) ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) (f x)) n)
    (coeff (f ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) x)) n)

Tactic:
simp_rw [map_coeff, hf, map_aeval, funext (map_coeff g _), RingHom.ext_int _ (algebraMap ℤ S),
    aeval_eq_eval₂Hom]

Premises used: WittVector.map_coeff, Algebra.algebraMap, MvPolynomial.map_aeval, Int, RingHom.ext_int, funext, MvPolynomial.aeval_eq_eval₂Hom
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
hf : IsPoly₂ p f
hg : IsPoly₂ p g
h :
  ∀ (R : Type u) [_Rcr : CommRing R] (x y : 𝕎 R) (n : ℕ),
    Eq (α := R) ((ghostComponent n : (a : 𝕎 R) → R) (f x y) : R) ((ghostComponent n : (a : 𝕎 R) → R) (g x y) : R)
obtain :
  ∀ (φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ)
    (hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun (n : ℕ) ↦ peval (φ n) ![x.coeff, y.coeff])
    (R : Type u) [_Rcr : CommRing R] (x y : 𝕎 R), f x y = g x y
⊢ ∀ (R : Type u) [_Rcr : CommRing R] (x y : 𝕎 R), f x y = g x y

Tactic:
obtain ⟨φ, hf⟩ := hf