awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.WittVector.IsPoly
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]
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
⊢ ∀ (R : Type u) [_Rcr : CommRing R] (x y : 𝕎 R), f x y = g x y

Tactic:
obtain ⟨ψ, hg⟩ := hg
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
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]
ψ : ℕ → 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
h₁ : ∀ (n : ℕ), (f x y).coeff n = (g x y).coeff n
⊢ f x y = g x y

Tactic:
ext n
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
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]
ψ : ℕ → 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
n : ℕ
h₁ :
  ∀ (n : ℕ),
    Eq (α := MvPolynomial (Fin 2 × ℕ) ℤ)
      ((bind₁ φ : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (wittPolynomial p ℤ n) :
        MvPolynomial (Fin 2 × ℕ) ℤ)
      ((bind₁ ψ : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (wittPolynomial p ℤ n) :
        MvPolynomial (Fin 2 × ℕ) ℤ)
⊢ (f x y).coeff n = (g x y).coeff n

Tactic:
rw [hf, hg, poly_eq_of_wittPolynomial_bind_eq' p φ ψ]

Premises used: WittVector.poly_eq_of_wittPolynomial_bind_eq'
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
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]
ψ : ℕ → 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
n k : ℕ
h₁ :
  ∀ (x : Fin 2 × ℕ → ℤ),
    Eq (α := ℤ)
      ((MvPolynomial.eval x : (a : MvPolynomial (Fin 2 × ℕ) ℤ) → ℤ)
          ((bind₁ φ : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (wittPolynomial p ℤ k) :
            MvPolynomial (Fin 2 × ℕ) ℤ) :
        ℤ)
      ((MvPolynomial.eval x : (a : MvPolynomial (Fin 2 × ℕ) ℤ) → ℤ)
          ((bind₁ ψ : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (wittPolynomial p ℤ k) :
            MvPolynomial (Fin 2 × ℕ) ℤ) :
        ℤ)
⊢ Eq (α := MvPolynomial (Fin 2 × ℕ) ℤ)
    ((bind₁ φ : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (wittPolynomial p ℤ k) :
      MvPolynomial (Fin 2 × ℕ) ℤ)
    ((bind₁ ψ : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (wittPolynomial p ℤ k) :
      MvPolynomial (Fin 2 × ℕ) ℤ)

Tactic:
apply MvPolynomial.funext

Premises used: MvPolynomial.funext
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
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]
ψ : ℕ → 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_1 y : 𝕎 R
n k : ℕ
x : Fin 2 × ℕ → ℤ
h₁ :
  Eq (α := ℤ)
    ((eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun (i : ℕ) ↦
            (MvPolynomial.eval x : (a : MvPolynomial (Fin 2 × ℕ) ℤ) → ℤ) (φ i) :
          (a : MvPolynomial ℕ ℤ) → ℤ)
        (wittPolynomial p ℤ k) :
      ℤ)
    ((eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun (i : ℕ) ↦
            (MvPolynomial.eval x : (a : MvPolynomial (Fin 2 × ℕ) ℤ) → ℤ) (ψ i) :
          (a : MvPolynomial ℕ ℤ) → ℤ)
        (wittPolynomial p ℤ k) :
      ℤ)
⊢ Eq (α := ℤ)
    ((MvPolynomial.eval x : (a : MvPolynomial (Fin 2 × ℕ) ℤ) → ℤ)
        ((bind₁ φ : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (wittPolynomial p ℤ k) :
          MvPolynomial (Fin 2 × ℕ) ℤ) :
      ℤ)
    ((MvPolynomial.eval x : (a : MvPolynomial (Fin 2 × ℕ) ℤ) → ℤ)
        ((bind₁ ψ : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (wittPolynomial p ℤ k) :
          MvPolynomial (Fin 2 × ℕ) ℤ) :
      ℤ)

Tactic:
simp only [hom_bind₁]

Premises used: MvPolynomial.hom_bind₁
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
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]
ψ : ℕ → 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_1 y : 𝕎 R
n k : ℕ
x : Fin 2 × ℕ → ℤ
⊢ Eq.{u + 1} (α := ULift.{u, 0} ℤ)
    ((ghostComponent k : (a : 𝕎 (ULift.{u, 0} ℤ)) → ULift.{u, 0} ℤ)
        (f (mk p fun (i : ℕ) ↦ { down := x (0, i) }) (mk p fun (i : ℕ) ↦ { down := x (1, i) })) :
      ULift.{u, 0} ℤ)
    ((ghostComponent k : (a : 𝕎 (ULift.{u, 0} ℤ)) → ULift.{u, 0} ℤ)
        (g (mk p fun (i : ℕ) ↦ { down := x (0, i) }) (mk p fun (i : ℕ) ↦ { down := x (1, i) })) :
      ULift.{u, 0} ℤ)

Tactic:
specialize h (ULift ℤ) (mk p fun i => ⟨x (0, i)⟩) (mk p fun i => ⟨x (1, i)⟩) k

Premises used: ULift, WittVector.mk, Prod.mk, Int, OfNat.ofNat, ULift.up
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 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]
ψ : ℕ → 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_1 y : 𝕎 R
n k : ℕ
x : Fin 2 × ℕ → ℤ
h :
  Eq.{u + 1} (α := ULift.{u, 0} ℤ)
    ((eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ))
            (coeff
              (f (mk p fun (i : ℕ) ↦ { down := x (0, i) : ULift.{u, 0} ℤ })
                (mk p fun (i : ℕ) ↦ { down := x (1, i) : ULift.{u, 0} ℤ }))) :
          (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
        (wittPolynomial p ℤ k) :
      ULift.{u, 0} ℤ)
    ((eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ))
            (coeff
              (g (mk p fun (i : ℕ) ↦ { down := x (0, i) : ULift.{u, 0} ℤ })
                (mk p fun (i : ℕ) ↦ { down := x (1, i) : ULift.{u, 0} ℤ }))) :
          (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
        (wittPolynomial p ℤ k) :
      ULift.{u, 0} ℤ)
h₁ :
  Eq.{u + 1} (α := ULift.{u, 0} ℤ)
    ((RingEquiv.symm ULift.ringEquiv : (a : ℤ) → ULift.{u, 0} ℤ)
        ((eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun (i : ℕ) ↦
                (MvPolynomial.eval x : (a : MvPolynomial (Fin 2 × ℕ) ℤ) → ℤ) (φ i) :
              (a : MvPolynomial ℕ ℤ) → ℤ)
            (wittPolynomial p ℤ k) :
          ℤ) :
      ULift.{u, 0} ℤ)
    ((RingEquiv.symm ULift.ringEquiv : (a : ℤ) → ULift.{u, 0} ℤ)
        ((eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun (i : ℕ) ↦
                (MvPolynomial.eval x : (a : MvPolynomial (Fin 2 × ℕ) ℤ) → ℤ) (ψ i) :
              (a : MvPolynomial ℕ ℤ) → ℤ)
            (wittPolynomial p ℤ k) :
          ℤ) :
      ULift.{u, 0} ℤ)
⊢ Eq (α := ℤ)
    ((eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun (i : ℕ) ↦
            (MvPolynomial.eval x : (a : MvPolynomial (Fin 2 × ℕ) ℤ) → ℤ) (φ i) :
          (a : MvPolynomial ℕ ℤ) → ℤ)
        (wittPolynomial p ℤ k) :
      ℤ)
    ((eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun (i : ℕ) ↦
            (MvPolynomial.eval x : (a : MvPolynomial (Fin 2 × ℕ) ℤ) → ℤ) (ψ i) :
          (a : MvPolynomial ℕ ℤ) → ℤ)
        (wittPolynomial p ℤ k) :
      ℤ)

Tactic:
apply (ULift.ringEquiv.symm : ℤ ≃+* _).injective

Premises used: RingEquiv.injective, ULift.ringEquiv, RingEquiv.symm
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 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]
ψ : ℕ → 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_1 y : 𝕎 R
n k : ℕ
x : Fin 2 × ℕ → ℤ
h :
  Eq.{u + 1} (α := ULift.{u, 0} ℤ)
    ((eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ))
            (coeff
              (f (mk p fun (i : ℕ) ↦ { down := x (0, i) : ULift.{u, 0} ℤ })
                (mk p fun (i : ℕ) ↦ { down := x (1, i) : ULift.{u, 0} ℤ }))) :
          (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
        (wittPolynomial p ℤ k) :
      ULift.{u, 0} ℤ)
    ((eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ))
            (coeff
              (g (mk p fun (i : ℕ) ↦ { down := x (0, i) : ULift.{u, 0} ℤ })
                (mk p fun (i : ℕ) ↦ { down := x (1, i) : ULift.{u, 0} ℤ }))) :
          (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
        (wittPolynomial p ℤ k) :
      ULift.{u, 0} ℤ)
h₁ :
  Eq (α := ULift.{u, 0} ℤ)
    ((eval₂Hom
            (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ)
              (RingHom.comp (MvPolynomial.eval x) C))
            fun (i : ℕ) ↦
            ((↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) : (a : ℤ) → ULift.{u, 0} ℤ)
              ((MvPolynomial.eval x : (a : MvPolynomial (Fin 2 × ℕ) ℤ) → ℤ) (φ i) : ℤ) :
          (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
        (wittPolynomial p ℤ k) :
      ULift.{u, 0} ℤ)
    ((eval₂Hom
            (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ)
              (RingHom.comp (MvPolynomial.eval x) C))
            fun (i : ℕ) ↦
            ((↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) : (a : ℤ) → ULift.{u, 0} ℤ)
              ((MvPolynomial.eval x : (a : MvPolynomial (Fin 2 × ℕ) ℤ) → ℤ) (ψ i) : ℤ) :
          (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
        (wittPolynomial p ℤ k) :
      ULift.{u, 0} ℤ)
⊢ Eq.{u + 1} (α := ULift.{u, 0} ℤ)
    ((RingEquiv.symm ULift.ringEquiv : (a : ℤ) → ULift.{u, 0} ℤ)
        ((eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun (i : ℕ) ↦
                (MvPolynomial.eval x : (a : MvPolynomial (Fin 2 × ℕ) ℤ) → ℤ) (φ i) :
              (a : MvPolynomial ℕ ℤ) → ℤ)
            (wittPolynomial p ℤ k) :
          ℤ) :
      ULift.{u, 0} ℤ)
    ((RingEquiv.symm ULift.ringEquiv : (a : ℤ) → ULift.{u, 0} ℤ)
        ((eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun (i : ℕ) ↦
                (MvPolynomial.eval x : (a : MvPolynomial (Fin 2 × ℕ) ℤ) → ℤ) (ψ i) :
              (a : MvPolynomial ℕ ℤ) → ℤ)
            (wittPolynomial p ℤ k) :
          ℤ) :
      ULift.{u, 0} ℤ)

Tactic:
simp only [← RingEquiv.coe_toRingHom, map_eval₂Hom]

Premises used: MvPolynomial.map_eval₂Hom, RingEquiv.coe_toRingHom
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 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]
ψ : ℕ → 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_1 y : 𝕎 R
n k : ℕ
x : Fin 2 × ℕ → ℤ
h :
  Eq.{u + 1} (α := ULift.{u, 0} ℤ)
    ((eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ))
            (coeff
              (f (mk p fun (i : ℕ) ↦ { down := x (0, i) : ULift.{u, 0} ℤ })
                (mk p fun (i : ℕ) ↦ { down := x (1, i) : ULift.{u, 0} ℤ }))) :
          (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
        (wittPolynomial p ℤ k) :
      ULift.{u, 0} ℤ)
    ((eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ))
            (coeff
              (g (mk p fun (i : ℕ) ↦ { down := x (0, i) : ULift.{u, 0} ℤ })
                (mk p fun (i : ℕ) ↦ { down := x (1, i) : ULift.{u, 0} ℤ }))) :
          (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
        (wittPolynomial p ℤ k) :
      ULift.{u, 0} ℤ)
⊢ Eq.{u + 1} (α := ULift.{u, 0} ℤ)
    ((eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ))
            (coeff
              (f (mk p fun (i : ℕ) ↦ { down := x (0, i) : ULift.{u, 0} ℤ })
                (mk p fun (i : ℕ) ↦ { down := x (1, i) : ULift.{u, 0} ℤ }))) :
          (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
        (wittPolynomial p ℤ k) :
      ULift.{u, 0} ℤ)
    ((eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ))
            (coeff
              (g (mk p fun (i : ℕ) ↦ { down := x (0, i) : ULift.{u, 0} ℤ })
                (mk p fun (i : ℕ) ↦ { down := x (1, i) : ULift.{u, 0} ℤ }))) :
          (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
        (wittPolynomial p ℤ k) :
      ULift.{u, 0} ℤ)

Tactic:
h
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 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]
ψ : ℕ → 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_1 y : 𝕎 R
n k : ℕ
x : Fin 2 × ℕ → ℤ
h :
  Eq.{u + 1} (α := ULift.{u, 0} ℤ)
    ((eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ))
            (coeff
              (f (mk p fun (i : ℕ) ↦ { down := x (0, i) : ULift.{u, 0} ℤ })
                (mk p fun (i : ℕ) ↦ { down := x (1, i) : ULift.{u, 0} ℤ }))) :
          (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
        (wittPolynomial p ℤ k) :
      ULift.{u, 0} ℤ)
    ((eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ))
            (coeff
              (g (mk p fun (i : ℕ) ↦ { down := x (0, i) : ULift.{u, 0} ℤ })
                (mk p fun (i : ℕ) ↦ { down := x (1, i) : ULift.{u, 0} ℤ }))) :
          (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
        (wittPolynomial p ℤ k) :
      ULift.{u, 0} ℤ)
h₁ :
  Eq (α := ULift.{u, 0} ℤ)
    ((eval₂Hom
            (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ)
              ((eval₂Hom (RingHom.id ℤ) x).comp C))
            fun (i : ℕ) ↦
            (eval₂Hom (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) (RingHom.id ℤ))
                  fun (i : Fin 2 × ℕ) ↦
                  ((↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) : (a : ℤ) → ULift.{u, 0} ℤ) (x i) :
                (a : MvPolynomial (Fin 2 × ℕ) ℤ) → ULift.{u, 0} ℤ)
              (φ i) :
          (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
        (wittPolynomial p ℤ k) :
      ULift.{u, 0} ℤ)
    ((eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) fun (n : ℕ) ↦
            peval (φ n)
              ![coeff (mk p fun (i : ℕ) ↦ { down := x (0, i) : ULift.{u, 0} ℤ }),
                coeff (mk p fun (i : ℕ) ↦ { down := x (1, i) : ULift.{u, 0} ℤ })] :
          (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
        (wittPolynomial p ℤ k) :
      ULift.{u, 0} ℤ)
⊢ Eq (α := ULift.{u, 0} ℤ)
    ((eval₂Hom
            (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ)
              (RingHom.comp (MvPolynomial.eval x) C))
            fun (i : ℕ) ↦
            ((↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) : (a : ℤ) → ULift.{u, 0} ℤ)
              ((MvPolynomial.eval x : (a : MvPolynomial (Fin 2 × ℕ) ℤ) → ℤ) (φ i) : ℤ) :
          (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
        (wittPolynomial p ℤ k) :
      ULift.{u, 0} ℤ)
    ((eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ))
            (coeff
              (f (mk p fun (i : ℕ) ↦ { down := x (0, i) : ULift.{u, 0} ℤ })
                (mk p fun (i : ℕ) ↦ { down := x (1, i) : ULift.{u, 0} ℤ }))) :
          (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
        (wittPolynomial p ℤ k) :
      ULift.{u, 0} ℤ)

Tactic:
simp only [hf, hg, MvPolynomial.eval, map_eval₂Hom]

Premises used: MvPolynomial.map_eval₂Hom, MvPolynomial.eval
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 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]
ψ : ℕ → 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_1 y : 𝕎 R
n k : ℕ
x : Fin 2 × ℕ → ℤ
h :
  Eq.{u + 1} (α := ULift.{u, 0} ℤ)
    ((eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ))
            (coeff
              (f (mk p fun (i : ℕ) ↦ { down := x (0, i) : ULift.{u, 0} ℤ })
                (mk p fun (i : ℕ) ↦ { down := x (1, i) : ULift.{u, 0} ℤ }))) :
          (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
        (wittPolynomial p ℤ k) :
      ULift.{u, 0} ℤ)
    ((eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ))
            (coeff
              (g (mk p fun (i : ℕ) ↦ { down := x (0, i) : ULift.{u, 0} ℤ })
                (mk p fun (i : ℕ) ↦ { down := x (1, i) : ULift.{u, 0} ℤ }))) :
          (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
        (wittPolynomial p ℤ k) :
      ULift.{u, 0} ℤ)
apply :
  Eq.{max 1 (u + 1)} (α := ℕ → ULift.{u, 0} ℤ)
    (fun (i : ℕ) ↦
      (eval₂Hom (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) (RingHom.id ℤ))
            fun (i : Fin 2 × ℕ) ↦
            ((↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) : (a : ℤ) → ULift.{u, 0} ℤ) (x i) :
          (a : MvPolynomial (Fin 2 × ℕ) ℤ) → ULift.{u, 0} ℤ)
        (φ i))
    fun (n : ℕ) ↦
    peval (φ n)
      ![coeff (mk p fun (i : ℕ) ↦ { down := x (0, i) : ULift.{u, 0} ℤ }),
        coeff (mk p fun (i : ℕ) ↦ { down := x (1, i) : ULift.{u, 0} ℤ })]
⊢ Eq (α := ULift.{u, 0} ℤ)
    ((eval₂Hom
            (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ)
              ((eval₂Hom (RingHom.id ℤ) x).comp C))
            fun (i : ℕ) ↦
            (eval₂Hom (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) (RingHom.id ℤ))
                  fun (i : Fin 2 × ℕ) ↦
                  ((↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) : (a : ℤ) → ULift.{u, 0} ℤ) (x i) :
                (a : MvPolynomial (Fin 2 × ℕ) ℤ) → ULift.{u, 0} ℤ)
              (φ i) :
          (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
        (wittPolynomial p ℤ k) :
      ULift.{u, 0} ℤ)
    ((eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) fun (n : ℕ) ↦
            peval (φ n)
              ![coeff (mk p fun (i : ℕ) ↦ { down := x (0, i) : ULift.{u, 0} ℤ }),
                coeff (mk p fun (i : ℕ) ↦ { down := x (1, i) : ULift.{u, 0} ℤ })] :
          (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
        (wittPolynomial p ℤ k) :
      ULift.{u, 0} ℤ)

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

Premises used: MvPolynomial.eval₂Hom_congr, RingHom.ext_int, rfl
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 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]
ψ : ℕ → 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_1 y : 𝕎 R
n k : ℕ
x : Fin 2 × ℕ → ℤ
h :
  Eq.{u + 1} (α := ULift.{u, 0} ℤ)
    ((eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ))
            (coeff
              (f (mk p fun (i : ℕ) ↦ { down := x (0, i) : ULift.{u, 0} ℤ })
                (mk p fun (i : ℕ) ↦ { down := x (1, i) : ULift.{u, 0} ℤ }))) :
          (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
        (wittPolynomial p ℤ k) :
      ULift.{u, 0} ℤ)
    ((eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ))
            (coeff
              (g (mk p fun (i : ℕ) ↦ { down := x (0, i) : ULift.{u, 0} ℤ })
                (mk p fun (i : ℕ) ↦ { down := x (1, i) : ULift.{u, 0} ℤ }))) :
          (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
        (wittPolynomial p ℤ k) :
      ULift.{u, 0} ℤ)
h₁ :
  ∀ (x_2 : ℕ),
    Eq (α := ULift.{u, 0} ℤ)
      ((eval₂Hom (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) (RingHom.id ℤ))
              fun (i : Fin 2 × ℕ) ↦
              ((↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) : (a : ℤ) → ULift.{u, 0} ℤ) (x i) :
            (a : MvPolynomial (Fin 2 × ℕ) ℤ) → ULift.{u, 0} ℤ)
          (φ x_2) :
        ULift.{u, 0} ℤ)
      (peval (φ x_2)
          ![coeff (mk p fun (i : ℕ) ↦ { down := x (0, i) : ULift.{u, 0} ℤ }),
            coeff (mk p fun (i : ℕ) ↦ { down := x (1, i) : ULift.{u, 0} ℤ })] :
        ULift.{u, 0} ℤ)
⊢ Eq.{max 1 (u + 1)} (α := ℕ → ULift.{u, 0} ℤ)
    (fun (i : ℕ) ↦
      (eval₂Hom (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) (RingHom.id ℤ))
            fun (i : Fin 2 × ℕ) ↦
            ((↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) : (a : ℤ) → ULift.{u, 0} ℤ) (x i) :
          (a : MvPolynomial (Fin 2 × ℕ) ℤ) → ULift.{u, 0} ℤ)
        (φ i))
    fun (n : ℕ) ↦
    peval (φ n)
      ![coeff (mk p fun (i : ℕ) ↦ { down := x (0, i) : ULift.{u, 0} ℤ }),
        coeff (mk p fun (i : ℕ) ↦ { down := x (1, i) : ULift.{u, 0} ℤ })]

Tactic:
ext1