awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
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 ℕ ℤ)
⊢ ![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 ℕ ℤ)
have h₁ : ![x.coeff, x.coeff] ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2), k).1 ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2), k).2 =
  ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1)
    (![X, X] ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2), k).1 ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩, k).2 : MvPolynomial ℕ ℤ)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
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
⊢ (-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)
have 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)
Tactic: funext n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
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 : ℕ
⊢ (-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)
have 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)
Tactic: rw [neg_coeff, aeval_eq_eval₂Hom, eval₂Hom_rename]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
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 : ℕ
⊢ peval (wittNeg p n) ![x.coeff] =
    (eval₂Hom (algebraMap ℤ R_1) (x.coeff ∘ Prod.snd) : (a : MvPolynomial (Fin 1 × ℕ) ℤ) → R_1) (wittNeg p n)
have apply : uncurry ![x.coeff] = x.coeff ∘ Prod.snd
Tactic: apply eval₂Hom_congr rfl _ rfl
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
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 : ℕ
⊢ uncurry ![x.coeff] = x.coeff ∘ Prod.snd
have h : ∀ (i : Fin 1) (k : ℕ), uncurry ![x.coeff] (i, k) = (x.coeff ∘ Prod.snd) (i, k)
Tactic: ext ⟨i, k⟩
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
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 : ℕ
⊢ uncurry ![x.coeff] (i, k) = (x.coeff ∘ Prod.snd) (i, k)
have h : uncurry ![x.coeff] ((fun (i : Fin 1) ↦ i) (⟨0, sorry⟩ : Fin 1), k) =
  Function.comp (α := Fin 1 × ℕ) x.coeff Prod.snd ((fun (i : Fin 1) ↦ i) ⟨0, sorry⟩, k)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
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.{u_2 + 1} (α := ℕ → R_1) (coeff (p := p) 0) fun (n : ℕ) ↦
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1) (0 n)
have 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)
Tactic: funext n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
Goal:
p : ℕ
R : Type u
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
n : ℕ
⊢ Eq (α := MvPolynomial ℕ R)
    ((bind₁ 0 : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (wittPolynomial p R n) : MvPolynomial ℕ R)
    (0 : MvPolynomial ℕ R)
have rw : Eq (α := MvPolynomial ℕ R)
  ((aeval 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]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
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)
⊢ Eq (α := MvPolynomial ℕ R)
    ((bind₁ 0 : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (wittPolynomial p R n) : MvPolynomial ℕ R)
    (0 : MvPolynomial ℕ R)
have 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)
Tactic: rw [← aeval_eq_bind₁, aeval_zero, constantCoeff_wittPolynomial, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
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)
⊢ Eq (α := MvPolynomial ℕ R)
    ((bind₁ 0 : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (wittPolynomial p R n) : MvPolynomial ℕ R)
    (0 : MvPolynomial ℕ R)
have rw₂ : Eq (α := MvPolynomial ℕ R) ((algebraMap R (MvPolynomial ℕ R) : (a : R) → MvPolynomial ℕ R) 0) 0
Tactic: rw [← aeval_eq_bind₁, aeval_zero, constantCoeff_wittPolynomial, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
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
⊢ Eq (α := MvPolynomial ℕ R)
    ((bind₁ 0 : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (wittPolynomial p R n) : MvPolynomial ℕ R)
    (0 : MvPolynomial ℕ R)
have rw₃ : Eq.{u + 1} (α := MvPolynomial ℕ R) 0 0
Tactic: rw [← aeval_eq_bind₁, aeval_zero, constantCoeff_wittPolynomial, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ Eq (α := MvPolynomial ℕ ℤ)
    ((bind₁ onePoly : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n) : MvPolynomial ℕ ℤ)
    (1 : MvPolynomial ℕ ℤ)
have 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 ℕ ℤ)
Tactic: rw [wittPolynomial_eq_sum_C_mul_X_pow, map_sum, Finset.sum_eq_single 0]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
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 ℕ ℤ)
⊢ Eq (α := MvPolynomial ℕ ℤ)
    ((bind₁ onePoly : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n) : MvPolynomial ℕ ℤ)
    (1 : MvPolynomial ℕ ℤ)
have 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 ℕ ℤ)
Tactic: rw [wittPolynomial_eq_sum_C_mul_X_pow, map_sum, Finset.sum_eq_single 0]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
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 ℕ ℤ)
⊢ Eq (α := MvPolynomial ℕ ℤ)
    ((bind₁ onePoly : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n) : MvPolynomial ℕ ℤ)
    (1 : MvPolynomial ℕ ℤ)
have 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 ℕ ℤ)
Tactic: rw [wittPolynomial_eq_sum_C_mul_X_pow, map_sum, Finset.sum_eq_single 0]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
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.{u_2 + 1} (α := ℕ → R_1) (coeff (p := p) 1) fun (n : ℕ) ↦
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1) (onePoly n)
have 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)
Tactic: funext n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
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 : R_1)
    (((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1) (onePoly n) : R_1)
have 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)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
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)
⊢ 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)
have 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)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
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 + y).coeff = fun (n : ℕ) ↦ peval (wittAdd p n) ![x.coeff, y.coeff]
have h : ∀ (x_1 : ℕ), (x + y).coeff x_1 = peval (wittAdd p x_1) ![x.coeff, y.coeff]
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
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 * y).coeff = fun (n : ℕ) ↦ peval (wittMul p n) ![x.coeff, y.coeff]
have h : ∀ (x_1 : ℕ), (x * y).coeff x_1 = peval (wittMul p x_1) ![x.coeff, y.coeff]
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
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
⊢ Eq (α := 𝕎 S) ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) (f x) : 𝕎 S) (f ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) x) : 𝕎 S)
have 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)
Tactic: obtain ⟨φ, hf⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
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)
⊢ Eq (α := 𝕎 S) ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) (f x) : 𝕎 S) (f ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) x) : 𝕎 S)
have 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)
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
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 : ℕ
⊢ 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)
have h : Eq (α := S) ((g : (a : R) → S) ((f x).coeff n) : S) (coeff (f ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) x)) n : S)
Tactic: simp_rw [map_coeff, hf, map_aeval, funext (map_coeff g _), RingHom.ext_int _ (algebraMap ℤ S),
    aeval_eq_eval₂Hom]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
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)
⊢ 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)
have 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)
Tactic: simp_rw [map_coeff, hf, map_aeval, funext (map_coeff g _), RingHom.ext_int _ (algebraMap ℤ S),
    aeval_eq_eval₂Hom]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
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)
⊢ 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)
have 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)
Tactic: simp_rw [map_coeff, hf, map_aeval, funext (map_coeff g _), RingHom.ext_int _ (algebraMap ℤ S),
    aeval_eq_eval₂Hom]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
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)
⊢ 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)
have 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)
Tactic: simp_rw [map_coeff, hf, map_aeval, funext (map_coeff g _), RingHom.ext_int _ (algebraMap ℤ S),
    aeval_eq_eval₂Hom]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
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)
⊢ 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)
have 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)
Tactic: simp_rw [map_coeff, hf, map_aeval, funext (map_coeff g _), RingHom.ext_int _ (algebraMap ℤ S),
    aeval_eq_eval₂Hom]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
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)
⊢ ∀ (R : Type u) [_Rcr : CommRing R] (x y : 𝕎 R), f x y = g x y
have 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
Tactic: obtain ⟨φ, hf⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
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)
φ : ℕ → 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
have obtain : ∀ (ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ)
  (hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g 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
Tactic: obtain ⟨ψ, hg⟩ := hg
Cleared hypotheses: hg