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
h : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
f g : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R
hh : IsPoly₂ p h
φ : ℕ → 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)
obtain :
  ∀ (χ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ)
    (hh :
      ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R), (h x y).coeff = fun (n : ℕ) ↦ peval (χ n) ![x.coeff, y.coeff]),
    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 ⟨χ, hh⟩ := hh
-- 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
φ : ℕ → 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)
χ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hh : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R), (h x y).coeff = fun (n : ℕ) ↦ peval (χ n) ![x.coeff, y.coeff]
⊢ IsPoly₂.{u_2} p fun (x : Type u_2) (_Rcr : CommRing x) (x_1 y : 𝕎 x) ↦ h (f x_1) (g y)

Tactic:
⟨⟨fun n ↦ bind₁ (uncurry <|
    ![fun k ↦ rename (Prod.mk (0 : Fin 2)) (φ k),
      fun k ↦ rename (Prod.mk (1 : Fin 2)) (ψ k)]) (χ n), ?_⟩⟩

Premises used: WittVector.IsPoly₂.mk', Prod.mk, MvPolynomial.bind₁, MvPolynomial.rename, Exists.intro, Matrix.vecEmpty, Function.uncurry, OfNat.ofNat, DFunLike.coe, Matrix.vecCons
-- 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
φ : ℕ → 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)
χ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hh : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R), (h x y).coeff = fun (n : ℕ) ↦ peval (χ n) ![x.coeff, y.coeff]
refine :
  ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R),
    (h (f x) (g y)).coeff = fun (n : ℕ) ↦
      peval
        ((fun (n : ℕ) ↦
            ((bind₁
                    (uncurry
                      ![fun (k : ℕ) ↦ (rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (φ k),
                        fun (k : ℕ) ↦
                        (rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (ψ k)]) :
                  (a : MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ)
                (χ n) :
              MvPolynomial (Fin 2 × ℕ) ℤ))
          n)
        ![x.coeff, y.coeff]
⊢ IsPoly₂.{u_2} p fun (x : Type u_2) (_Rcr : CommRing x) (x_1 y : 𝕎 x) ↦ h (f x_1) (g y)

Tactic:
refine ⟨⟨fun n ↦ bind₁ (uncurry <|
    ![fun k ↦ rename (Prod.mk (0 : Fin 2)) (φ k),
      fun k ↦ rename (Prod.mk (1 : Fin 2)) (ψ k)]) (χ n), ?_⟩⟩
-- 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
φ : ℕ → 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)
χ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hh : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R), (h x y).coeff = fun (n : ℕ) ↦ peval (χ n) ![x.coeff, y.coeff]
R_1 : Type u_2
inst_2 : CommRing R_1
x y : 𝕎 R_1
h₁ :
  ∀ (n : ℕ),
    (h (f x) (g y)).coeff n =
      peval
        ((fun (n : ℕ) ↦
            ((bind₁
                    (uncurry
                      ![fun (k : ℕ) ↦ (rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (φ k),
                        fun (k : ℕ) ↦
                        (rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (ψ k)]) :
                  (a : MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ)
                (χ n) :
              MvPolynomial (Fin 2 × ℕ) ℤ))
          n)
        ![x.coeff, y.coeff]
⊢ (h (f x) (g y)).coeff = fun (n : ℕ) ↦
    peval
      ((fun (n : ℕ) ↦
          ((bind₁
                  (uncurry
                    ![fun (k : ℕ) ↦ (rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (φ k),
                      fun (k : ℕ) ↦ (rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (ψ k)]) :
                (a : MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ)
              (χ n) :
            MvPolynomial (Fin 2 × ℕ) ℤ))
        n)
      ![x.coeff, y.coeff]

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
h : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
f g : ⦃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)
χ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hh : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R), (h x y).coeff = fun (n : ℕ) ↦ peval (χ n) ![x.coeff, y.coeff]
R_1 : Type u_2
inst_2 : CommRing R_1
x y : 𝕎 R_1
n : ℕ
h₁ :
  Eq.{u_2 + 1} (α := R_1)
    (((aeval.{0, u_2, 0} (R := ℤ) (S₁ := R_1) fun (a : Fin 2 × ℕ) ↦
              ![fun (n : ℕ) ↦
                  ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1) (φ n),
                  fun (n : ℕ) ↦
                  ((aeval (R := ℤ) y.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1) (ψ n)]
                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.{0, u_2, 0} (R := ℤ) (S₁ := R_1) fun (a : Fin 2 × ℕ) ↦ ![x.coeff, y.coeff] a.1 a.2 :
                    MvPolynomial (Fin 2 × ℕ) ℤ →ₐ[ℤ] R_1) :
                  (a : MvPolynomial (Fin 2 × ℕ) ℤ) → R_1)
                (![fun (k : ℕ) ↦ (rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (φ k),
                    fun (k : ℕ) ↦ (rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (ψ k)]
                  i.1 i.2) :
            MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ →ₐ[ℤ] R_1) :
          (a : MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ) → R_1)
        (χ n) :
      R_1)
⊢ (h (f x) (g y)).coeff n =
    peval
      ((fun (n : ℕ) ↦
          ((bind₁
                  (uncurry
                    ![fun (k : ℕ) ↦ (rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (φ k),
                      fun (k : ℕ) ↦ (rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (ψ k)]) :
                (a : MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ)
              (χ n) :
            MvPolynomial (Fin 2 × ℕ) ℤ))
        n)
      ![x.coeff, y.coeff]

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

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
h : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
f g : ⦃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)
χ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hh : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R), (h x y).coeff = fun (n : ℕ) ↦ peval (χ n) ![x.coeff, y.coeff]
R_1 : Type u_2
inst_2 : CommRing R_1
x y : 𝕎 R_1
n : ℕ
apply :
  Eq.{max 1 (u_2 + 1)} (α := Fin 2 × ℕ → R_1)
    (fun (a : Fin 2 × ℕ) ↦
      ![fun (n : ℕ) ↦ ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1) (φ n),
          fun (n : ℕ) ↦ ((aeval (R := ℤ) y.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1) (ψ n)]
        a.1 a.2)
    fun (i : Fin (Nat.succ 0).succ × ℕ) ↦
    ((aeval.{0, u_2, 0} (R := ℤ) (S₁ := R_1) fun (a : Fin 2 × ℕ) ↦ ![x.coeff, y.coeff] a.1 a.2 :
          MvPolynomial (Fin 2 × ℕ) ℤ →ₐ[ℤ] R_1) :
        (a : MvPolynomial (Fin 2 × ℕ) ℤ) → R_1)
      (![fun (k : ℕ) ↦ (rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (φ k), fun (k : ℕ) ↦
          (rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (ψ k)]
        i.1 i.2)
⊢ Eq.{u_2 + 1} (α := R_1)
    (((aeval.{0, u_2, 0} (R := ℤ) (S₁ := R_1) fun (a : Fin 2 × ℕ) ↦
              ![fun (n : ℕ) ↦
                  ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1) (φ n),
                  fun (n : ℕ) ↦
                  ((aeval (R := ℤ) y.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1) (ψ n)]
                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.{0, u_2, 0} (R := ℤ) (S₁ := R_1) fun (a : Fin 2 × ℕ) ↦ ![x.coeff, y.coeff] a.1 a.2 :
                    MvPolynomial (Fin 2 × ℕ) ℤ →ₐ[ℤ] R_1) :
                  (a : MvPolynomial (Fin 2 × ℕ) ℤ) → R_1)
                (![fun (k : ℕ) ↦ (rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (φ k),
                    fun (k : ℕ) ↦ (rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (ψ k)]
                  i.1 i.2) :
            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
h : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
f g : ⦃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)
χ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hh : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R), (h x y).coeff = fun (n : ℕ) ↦ peval (χ n) ![x.coeff, y.coeff]
R_1 : Type u_2
inst_2 : CommRing R_1
x y : 𝕎 R_1
n : ℕ
h₁ :
  ∀ (i : Fin 2) (n : ℕ),
    Eq.{u_2 + 1} (α := R_1)
      (![fun (n : ℕ) ↦ ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1) (φ n),
            fun (n : ℕ) ↦ ((aeval (R := ℤ) y.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1) (ψ n)]
          (i, n).1 (i, n).2 :
        R_1)
      (((aeval.{0, u_2, 0} (R := ℤ) (S₁ := R_1) fun (a : Fin 2 × ℕ) ↦ ![x.coeff, y.coeff] a.1 a.2 :
              MvPolynomial (Fin 2 × ℕ) ℤ →ₐ[ℤ] R_1) :
            (a : MvPolynomial (Fin 2 × ℕ) ℤ) → R_1)
          (![fun (k : ℕ) ↦ (rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (φ k),
              fun (k : ℕ) ↦ (rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (ψ k)]
            (i, n).1 (i, n).2) :
        R_1)
⊢ Eq.{max 1 (u_2 + 1)} (α := Fin 2 × ℕ → R_1)
    (fun (a : Fin 2 × ℕ) ↦
      ![fun (n : ℕ) ↦ ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1) (φ n),
          fun (n : ℕ) ↦ ((aeval (R := ℤ) y.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1) (ψ n)]
        a.1 a.2)
    fun (i : Fin (Nat.succ 0).succ × ℕ) ↦
    ((aeval.{0, u_2, 0} (R := ℤ) (S₁ := R_1) fun (a : Fin 2 × ℕ) ↦ ![x.coeff, y.coeff] a.1 a.2 :
          MvPolynomial (Fin 2 × ℕ) ℤ →ₐ[ℤ] R_1) :
        (a : MvPolynomial (Fin 2 × ℕ) ℤ) → R_1)
      (![fun (k : ℕ) ↦ (rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (φ k), fun (k : ℕ) ↦
          (rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (ψ k)]
        i.1 i.2)

Tactic:
ext ⟨i, n⟩
-- 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
φ : ℕ → 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)
χ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hh : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R), (h x y).coeff = fun (n : ℕ) ↦ peval (χ n) ![x.coeff, y.coeff]
R_1 : Type u_2
inst_2 : CommRing R_1
x y : 𝕎 R_1
n_1 n : ℕ
⊢ Eq.{u_2 + 1} (α := R_1)
    (![fun (n : ℕ) ↦ ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1) (φ n),
          fun (n : ℕ) ↦ ((aeval (R := ℤ) y.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1) (ψ n)]
        ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2), n).1 ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩, n).2 :
      R_1)
    (((aeval.{0, u_2, 0} (R := ℤ) (S₁ := R_1) fun (a : Fin 2 × ℕ) ↦ ![x.coeff, y.coeff] a.1 a.2 :
            MvPolynomial (Fin 2 × ℕ) ℤ →ₐ[ℤ] R_1) :
          (a : MvPolynomial (Fin 2 × ℕ) ℤ) → R_1)
        (![fun (k : ℕ) ↦ (rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (φ k), fun (k : ℕ) ↦
            (rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (ψ k)]
          ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2), n).1 ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩, n).2) :
      R_1)

Tactic:
simp [aeval_eq_eval₂Hom, eval₂Hom_rename, Function.comp_def]

Premises used: MvPolynomial.eval₂Hom_rename, Function.comp_def, MvPolynomial.aeval_eq_eval₂Hom
-- 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
φ : ℕ → 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)
χ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hh : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R), (h x y).coeff = fun (n : ℕ) ↦ peval (χ n) ![x.coeff, y.coeff]
R_1 : Type u_2
inst_2 : CommRing R_1
x y : 𝕎 R_1
n_1 n : ℕ
⊢ Eq.{u_2 + 1} (α := R_1)
    (![fun (n : ℕ) ↦ ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1) (φ n),
          fun (n : ℕ) ↦ ((aeval (R := ℤ) y.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1) (ψ n)]
        ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2), n).1 ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩, n).2 :
      R_1)
    (((aeval.{0, u_2, 0} (R := ℤ) (S₁ := R_1) fun (a : Fin 2 × ℕ) ↦ ![x.coeff, y.coeff] a.1 a.2 :
            MvPolynomial (Fin 2 × ℕ) ℤ →ₐ[ℤ] R_1) :
          (a : MvPolynomial (Fin 2 × ℕ) ℤ) → R_1)
        (![fun (k : ℕ) ↦ (rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (φ k), fun (k : ℕ) ↦
            (rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (ψ k)]
          ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2), n).1 ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩, n).2) :
      R_1)

Tactic:
simp [aeval_eq_eval₂Hom, eval₂Hom_rename, Function.comp_def]

Premises used: MvPolynomial.eval₂Hom_rename, Function.comp_def, MvPolynomial.aeval_eq_eval₂Hom
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
idx : Type u_1
inst : CommRing R
inst_1 : CommRing S
g : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R
f : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
hg : IsPoly p g
hf : IsPoly₂ p f
obtain :
  ∀ (φ : ℕ → 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]),
    IsPoly₂.{u_2} p fun (x : Type u_2) (_Rcr : CommRing x) (x_1 y : 𝕎 x) ↦ g (f x_1 y)
⊢ IsPoly₂.{u_2} p fun (x : Type u_2) (_Rcr : CommRing x) (x_1 y : 𝕎 x) ↦ g (f x_1 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
g : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R
f : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
hg : IsPoly p g
φ : ℕ → 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]
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) ↦ g (f x_1 y)
⊢ IsPoly₂.{u_2} p fun (x : Type u_2) (_Rcr : CommRing x) (x_1 y : 𝕎 x) ↦ g (f x_1 y)

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 : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R
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]
ψ : ℕ → 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 y : 𝕎 R),
    (g (f x y)).coeff = fun (n : ℕ) ↦
      peval
        ((fun (n : ℕ) ↦
            ((bind₁ φ : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (ψ n) : MvPolynomial (Fin 2 × ℕ) ℤ))
          n)
        ![x.coeff, y.coeff]
⊢ IsPoly₂.{u_2} p fun (x : Type u_2) (_Rcr : CommRing x) (x_1 y : 𝕎 x) ↦ g (f x_1 y)

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 : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R
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]
ψ : ℕ → 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 y : 𝕎 R_1
⊢ (g (f x y)).coeff = fun (n : ℕ) ↦
    peval
      ((fun (n : ℕ) ↦
          ((bind₁ φ : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (ψ n) : MvPolynomial (Fin 2 × ℕ) ℤ))
        n)
      ![x.coeff, y.coeff]

Tactic:
simp only [peval, aeval_bind₁, hg, hf]

Premises used: WittVector.peval, 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
f : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
hf : IsPoly₂ p f
obtain :
  ∀ (φ : ℕ → 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]),
    IsPoly.{u_2} p fun (x : Type u_2) (_Rcr : CommRing x) (x_1 : 𝕎 x) ↦ f x_1 x_1
⊢ IsPoly.{u_2} p fun (x : Type u_2) (_Rcr : CommRing x) (x_1 : 𝕎 x) ↦ f x_1 x_1

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
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]
⊢ IsPoly.{u_2} p fun (x : Type u_2) (_Rcr : CommRing x) (x_1 : 𝕎 x) ↦ f x_1 x_1

Tactic:
⟨⟨fun n => bind₁ (uncurry ![X, X]) (φ n), ?_⟩⟩

Premises used: MvPolynomial.X, MvPolynomial.bind₁, Exists.intro, Matrix.vecEmpty, WittVector.IsPoly.mk', Function.uncurry, DFunLike.coe, Matrix.vecCons
-- 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]
refine :
  ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R),
    (f x x).coeff = fun (n : ℕ) ↦
      (aeval x.coeff : (a : MvPolynomial ℕ ℤ) → R)
        ((fun (n : ℕ) ↦
            ((bind₁ (uncurry ![X, X]) : (a : MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ) → MvPolynomial ℕ ℤ) (φ n) :
              MvPolynomial ℕ ℤ))
          n)
⊢ IsPoly.{u_2} p fun (x : Type u_2) (_Rcr : CommRing x) (x_1 : 𝕎 x) ↦ f x_1 x_1

Tactic:
refine ⟨⟨fun n => bind₁ (uncurry ![X, X]) (φ n), ?_⟩⟩
-- 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
h :
  ∀ (n : ℕ),
    (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)
⊢ (f x x).coeff = fun (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:
funext n