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
φ : ℕ → MvPolynomial ℕ ℤ
hf :
  ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R),
    (f x).coeff = fun (n : ℕ) ↦ (aeval x.coeff : (a : MvPolynomial ℕ ℤ) → R) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg :
  ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R),
    (g x).coeff = fun (n : ℕ) ↦ (aeval x.coeff : (a : MvPolynomial ℕ ℤ) → R) (ψ n)
R : Type u
_Rcr : CommRing R
x_1 : 𝕎 R
n k : ℕ
x : ℕ → ℤ
h :
  Eq.{u + 1} (α := ULift.{u, 0} ℤ)
    ((eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (coeff (f (mk p fun (i : ℕ) ↦ { down := x 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 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 : ℕ) ↦
                  ((↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) : (a : ℤ) → ULift.{u, 0} ℤ) (x i) :
                (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
              (φ i) :
          (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
        (wittPolynomial p ℤ k) :
      ULift.{u, 0} ℤ)
    ((eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) fun (n : ℕ) ↦
            (aeval (coeff (mk p fun (i : ℕ) ↦ { down := x i : ULift.{u, 0} ℤ })) :
                (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
              (φ n) :
          (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 ℕ ℤ) → ℤ) (φ 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 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
φ : ℕ → MvPolynomial ℕ ℤ
hf :
  ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R),
    (f x).coeff = fun (n : ℕ) ↦ (aeval x.coeff : (a : MvPolynomial ℕ ℤ) → R) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg :
  ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R),
    (g x).coeff = fun (n : ℕ) ↦ (aeval x.coeff : (a : MvPolynomial ℕ ℤ) → R) (ψ n)
R : Type u
_Rcr : CommRing R
x_1 : 𝕎 R
n k : ℕ
x : ℕ → ℤ
h :
  Eq.{u + 1} (α := ULift.{u, 0} ℤ)
    ((eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (coeff (f (mk p fun (i : ℕ) ↦ { down := x 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 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 : ℕ) ↦
            ((↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) : (a : ℤ) → ULift.{u, 0} ℤ) (x i) :
          (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
        (φ i))
    fun (n : ℕ) ↦
    (aeval (coeff (mk p fun (i : ℕ) ↦ { down := x i : ULift.{u, 0} ℤ })) : (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
      (φ n)
⊢ 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 : ℕ) ↦
                  ((↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) : (a : ℤ) → ULift.{u, 0} ℤ) (x i) :
                (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
              (φ i) :
          (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
        (wittPolynomial p ℤ k) :
      ULift.{u, 0} ℤ)
    ((eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) fun (n : ℕ) ↦
            (aeval (coeff (mk p fun (i : ℕ) ↦ { down := x i : ULift.{u, 0} ℤ })) :
                (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
              (φ n) :
          (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
φ : ℕ → MvPolynomial ℕ ℤ
hf :
  ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R),
    (f x).coeff = fun (n : ℕ) ↦ (aeval x.coeff : (a : MvPolynomial ℕ ℤ) → R) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg :
  ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R),
    (g x).coeff = fun (n : ℕ) ↦ (aeval x.coeff : (a : MvPolynomial ℕ ℤ) → R) (ψ n)
R : Type u
_Rcr : CommRing R
x_1 : 𝕎 R
n k : ℕ
x : ℕ → ℤ
h :
  Eq.{u + 1} (α := ULift.{u, 0} ℤ)
    ((eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (coeff (f (mk p fun (i : ℕ) ↦ { down := x 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 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 : ℕ) ↦
              ((↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) : (a : ℤ) → ULift.{u, 0} ℤ) (x i) :
            (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
          (φ x_2) :
        ULift.{u, 0} ℤ)
      ((aeval (coeff (mk p fun (i : ℕ) ↦ { down := x i : ULift.{u, 0} ℤ })) : (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
          (φ x_2) :
        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 : ℕ) ↦
            ((↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) : (a : ℤ) → ULift.{u, 0} ℤ) (x i) :
          (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
        (φ i))
    fun (n : ℕ) ↦
    (aeval (coeff (mk p fun (i : ℕ) ↦ { down := x i : ULift.{u, 0} ℤ })) : (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
      (φ n)

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

Tactic:
rfl
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf :
  ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R),
    (f x).coeff = fun (n : ℕ) ↦ (aeval x.coeff : (a : MvPolynomial ℕ ℤ) → R) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg :
  ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R),
    (g x).coeff = fun (n : ℕ) ↦ (aeval x.coeff : (a : MvPolynomial ℕ ℤ) → R) (ψ n)
R : Type u
_Rcr : CommRing R
x_1 : 𝕎 R
n k : ℕ
x : ℕ → ℤ
h :
  Eq.{u + 1} (α := ULift.{u, 0} ℤ)
    ((eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (coeff (f (mk p fun (i : ℕ) ↦ { down := x 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 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 : ℕ) ↦
                  ((↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) : (a : ℤ) → ULift.{u, 0} ℤ) (x i) :
                (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
              (ψ i) :
          (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
        (wittPolynomial p ℤ k) :
      ULift.{u, 0} ℤ)
    ((eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) fun (n : ℕ) ↦
            (aeval (coeff (mk p fun (i : ℕ) ↦ { down := x i : ULift.{u, 0} ℤ })) :
                (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
              (ψ n) :
          (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 ℕ ℤ) → ℤ) (ψ i) : ℤ) :
          (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 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
φ : ℕ → MvPolynomial ℕ ℤ
hf :
  ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R),
    (f x).coeff = fun (n : ℕ) ↦ (aeval x.coeff : (a : MvPolynomial ℕ ℤ) → R) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg :
  ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R),
    (g x).coeff = fun (n : ℕ) ↦ (aeval x.coeff : (a : MvPolynomial ℕ ℤ) → R) (ψ n)
R : Type u
_Rcr : CommRing R
x_1 : 𝕎 R
n k : ℕ
x : ℕ → ℤ
h :
  Eq.{u + 1} (α := ULift.{u, 0} ℤ)
    ((eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (coeff (f (mk p fun (i : ℕ) ↦ { down := x 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 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 : ℕ) ↦
            ((↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) : (a : ℤ) → ULift.{u, 0} ℤ) (x i) :
          (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
        (ψ i))
    fun (n : ℕ) ↦
    (aeval (coeff (mk p fun (i : ℕ) ↦ { down := x i : ULift.{u, 0} ℤ })) : (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
      (ψ n)
⊢ 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 : ℕ) ↦
                  ((↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) : (a : ℤ) → ULift.{u, 0} ℤ) (x i) :
                (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
              (ψ i) :
          (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
        (wittPolynomial p ℤ k) :
      ULift.{u, 0} ℤ)
    ((eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) fun (n : ℕ) ↦
            (aeval (coeff (mk p fun (i : ℕ) ↦ { down := x i : ULift.{u, 0} ℤ })) :
                (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
              (ψ n) :
          (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
φ : ℕ → MvPolynomial ℕ ℤ
hf :
  ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R),
    (f x).coeff = fun (n : ℕ) ↦ (aeval x.coeff : (a : MvPolynomial ℕ ℤ) → R) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg :
  ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R),
    (g x).coeff = fun (n : ℕ) ↦ (aeval x.coeff : (a : MvPolynomial ℕ ℤ) → R) (ψ n)
R : Type u
_Rcr : CommRing R
x_1 : 𝕎 R
n k : ℕ
x : ℕ → ℤ
h :
  Eq.{u + 1} (α := ULift.{u, 0} ℤ)
    ((eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (coeff (f (mk p fun (i : ℕ) ↦ { down := x 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 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 : ℕ) ↦
              ((↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) : (a : ℤ) → ULift.{u, 0} ℤ) (x i) :
            (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
          (ψ x_2) :
        ULift.{u, 0} ℤ)
      ((aeval (coeff (mk p fun (i : ℕ) ↦ { down := x i : ULift.{u, 0} ℤ })) : (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
          (ψ x_2) :
        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 : ℕ) ↦
            ((↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) : (a : ℤ) → ULift.{u, 0} ℤ) (x i) :
          (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
        (ψ i))
    fun (n : ℕ) ↦
    (aeval (coeff (mk p fun (i : ℕ) ↦ { down := x i : ULift.{u, 0} ℤ })) : (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
      (ψ n)

Tactic:
ext1
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf :
  ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R),
    (f x).coeff = fun (n : ℕ) ↦ (aeval x.coeff : (a : MvPolynomial ℕ ℤ) → R) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg :
  ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R),
    (g x).coeff = fun (n : ℕ) ↦ (aeval x.coeff : (a : MvPolynomial ℕ ℤ) → R) (ψ n)
R : Type u
_Rcr : CommRing R
x_1 : 𝕎 R
n k : ℕ
x : ℕ → ℤ
h :
  Eq.{u + 1} (α := ULift.{u, 0} ℤ)
    ((eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (coeff (f (mk p fun (i : ℕ) ↦ { down := x 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 i : ULift.{u, 0} ℤ }))) :
          (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
        (wittPolynomial p ℤ k) :
      ULift.{u, 0} ℤ)
x_2 : ℕ
apply :
  Eq.{max 1 (u + 1)} (α := ℕ → ULift.{u, 0} ℤ)
    (fun (i : ℕ) ↦ ((↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) : (a : ℤ) → ULift.{u, 0} ℤ) (x i))
    (coeff (mk p fun (i : ℕ) ↦ { down := x i : ULift.{u, 0} ℤ }))
⊢ Eq (α := ULift.{u, 0} ℤ)
    ((eval₂Hom (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) (RingHom.id ℤ)) fun (i : ℕ) ↦
            ((↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) : (a : ℤ) → ULift.{u, 0} ℤ) (x i) :
          (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
        (ψ x_2) :
      ULift.{u, 0} ℤ)
    ((aeval (coeff (mk p fun (i : ℕ) ↦ { down := x i : ULift.{u, 0} ℤ })) : (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
        (ψ x_2) :
      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 : ℕ
R S : Type u
idx : Type u_1
inst : CommRing R
inst_1 : CommRing S
g f : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R
hg : IsPoly p g
hf : IsPoly p f
obtain :
  ∀ (φ : ℕ → MvPolynomial ℕ ℤ)
    (hf :
      ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R),
        (f x).coeff = fun (n : ℕ) ↦ (aeval x.coeff : (a : MvPolynomial ℕ ℤ) → R) (φ n)),
    IsPoly.{u_2} p fun (R : Type u_2) (_Rcr : CommRing R) ↦ g ∘ f
⊢ IsPoly.{u_2} p fun (R : Type u_2) (_Rcr : CommRing R) ↦ g ∘ f

Tactic:
obtain ⟨φ, hf⟩ := hf
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
idx : Type u_1
inst : CommRing R
inst_1 : CommRing S
g f : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R
hg : IsPoly p g
φ : ℕ → MvPolynomial ℕ ℤ
hf :
  ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R),
    (f x).coeff = fun (n : ℕ) ↦ (aeval x.coeff : (a : MvPolynomial ℕ ℤ) → R) (φ n)
obtain :
  ∀ (ψ : ℕ → MvPolynomial ℕ ℤ)
    (hg :
      ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R),
        (g x).coeff = fun (n : ℕ) ↦ (aeval x.coeff : (a : MvPolynomial ℕ ℤ) → R) (ψ n)),
    IsPoly.{u_2} p fun (R : Type u_2) (_Rcr : CommRing R) ↦ g ∘ f
⊢ IsPoly.{u_2} p fun (R : Type u_2) (_Rcr : CommRing R) ↦ g ∘ f

Tactic:
obtain ⟨ψ, hg⟩ := hg
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
idx : Type u_1
inst : CommRing R
inst_1 : CommRing S
g f : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf :
  ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R),
    (f x).coeff = fun (n : ℕ) ↦ (aeval x.coeff : (a : MvPolynomial ℕ ℤ) → R) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg :
  ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R),
    (g x).coeff = fun (n : ℕ) ↦ (aeval x.coeff : (a : MvPolynomial ℕ ℤ) → R) (ψ n)
h :
  ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R),
    ((g ∘ f) x).coeff = fun (n : ℕ) ↦
      (aeval x.coeff : (a : MvPolynomial ℕ ℤ) → R)
        ((fun (n : ℕ) ↦ ((bind₁ φ : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (ψ n) : MvPolynomial ℕ ℤ)) n)
⊢ IsPoly.{u_2} p fun (R : Type u_2) (_Rcr : CommRing R) ↦ g ∘ f

Tactic:
use fun n => bind₁ φ (ψ n)

Premises used: MvPolynomial.bind₁, DFunLike.coe
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
idx : Type u_1
inst : CommRing R
inst_1 : CommRing S
g f : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf :
  ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R),
    (f x).coeff = fun (n : ℕ) ↦ (aeval x.coeff : (a : MvPolynomial ℕ ℤ) → R) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg :
  ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R),
    (g x).coeff = fun (n : ℕ) ↦ (aeval x.coeff : (a : MvPolynomial ℕ ℤ) → R) (ψ n)
R_1 : Type u_2
inst_2 : CommRing R_1
x : 𝕎 R_1
⊢ ((g ∘ f) x).coeff = fun (n : ℕ) ↦
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1)
      ((fun (n : ℕ) ↦ ((bind₁ φ : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (ψ n) : MvPolynomial ℕ ℤ)) n)

Tactic:
simp only [aeval_bind₁, Function.comp, hg, hf]

Premises used: Function.comp, MvPolynomial.aeval_bind₁
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
idx : Type u_1
inst : CommRing R
inst_1 : CommRing S
h : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
f g : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R
hh : IsPoly₂ p h
hf : IsPoly p f
hg : IsPoly p g
obtain :
  ∀ (φ : ℕ → MvPolynomial ℕ ℤ)
    (hf :
      ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R),
        (f x).coeff = fun (n : ℕ) ↦ (aeval x.coeff : (a : MvPolynomial ℕ ℤ) → R) (φ n)),
    IsPoly₂.{u_2} p fun (x : Type u_2) (_Rcr : CommRing x) (x_1 y : 𝕎 x) ↦ h (f x_1) (g y)
⊢ IsPoly₂.{u_2} p fun (x : Type u_2) (_Rcr : CommRing x) (x_1 y : 𝕎 x) ↦ h (f x_1) (g y)

Tactic:
obtain ⟨φ, hf⟩ := hf
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
idx : Type u_1
inst : CommRing R
inst_1 : CommRing S
h : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
f g : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R
hh : IsPoly₂ p h
hg : IsPoly p g
φ : ℕ → MvPolynomial ℕ ℤ
hf :
  ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R),
    (f x).coeff = fun (n : ℕ) ↦ (aeval x.coeff : (a : MvPolynomial ℕ ℤ) → R) (φ n)
obtain :
  ∀ (ψ : ℕ → MvPolynomial ℕ ℤ)
    (hg :
      ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R),
        (g x).coeff = fun (n : ℕ) ↦ (aeval x.coeff : (a : MvPolynomial ℕ ℤ) → R) (ψ n)),
    IsPoly₂.{u_2} p fun (x : Type u_2) (_Rcr : CommRing x) (x_1 y : 𝕎 x) ↦ h (f x_1) (g y)
⊢ IsPoly₂.{u_2} p fun (x : Type u_2) (_Rcr : CommRing x) (x_1 y : 𝕎 x) ↦ h (f x_1) (g y)

Tactic:
obtain ⟨ψ, hg⟩ := hg