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
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)
have 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]
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), ?_⟩⟩
-- 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
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 (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]
have 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]
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
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 (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]
have 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)
Tactic: simp +unfoldPartialApp only [peval, aeval_bind₁, hh, hf, hg,
    uncurry]
-- 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
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 : ℕ
⊢ 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)
have 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)
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
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 : ℕ
⊢ 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)
have 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)
Tactic: ext ⟨i, 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
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 : ℕ
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)
have h₁ : 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, sorry⟩ : Fin 2), n).1 ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩, 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, sorry⟩ : Fin 2), n).1 ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩, n).2) :
    R_1)
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
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
⊢ IsPoly₂.{u_2} p fun (x : Type u_2) (_Rcr : CommRing x) (x_1 y : 𝕎 x) ↦ g (f x_1 y)
have 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)
Tactic: obtain ⟨φ, hf⟩ := hf
Cleared hypotheses: hf
-- 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
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]
⊢ IsPoly₂.{u_2} p fun (x : Type u_2) (_Rcr : CommRing x) (x_1 y : 𝕎 x) ↦ g (f x_1 y)
have 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)
Tactic: obtain ⟨ψ, hg⟩ := hg
Cleared hypotheses: hg
-- 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
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)
⊢ IsPoly₂.{u_2} p fun (x : Type u_2) (_Rcr : CommRing x) (x_1 y : 𝕎 x) ↦ g (f x_1 y)
have 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]
Tactic: use fun n => bind₁ φ (ψ 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
f : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
hf : IsPoly₂ p f
⊢ IsPoly.{u_2} p fun (x : Type u_2) (_Rcr : CommRing x) (x_1 : 𝕎 x) ↦ f x_1 x_1
have 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
Tactic: obtain ⟨φ, hf⟩ := hf
Cleared hypotheses: hf
-- 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]
⊢ IsPoly.{u_2} p fun (x : Type u_2) (_Rcr : CommRing x) (x_1 : 𝕎 x) ↦ f x_1 x_1
have 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)
Tactic: refine ⟨⟨fun n => bind₁ (uncurry ![X, X]) (φ 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
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
⊢ (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)
have 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)
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
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 : ℕ
⊢ (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)
have h : Eq.{u_2 + 1} (α := R_1)
  (((aeval.{0, u_2, 0} (R := ℤ) (S₁ := R_1) fun (a : Fin 2 × ℕ) ↦ ![x.coeff, x.coeff] a.1 a.2 :
          MvPolynomial (Fin 2 × ℕ) ℤ →ₐ[ℤ] R_1) :
        (a : MvPolynomial (Fin 2 × ℕ) ℤ) → R_1)
      (φ n) :
    R_1)
  (((aeval.{0, u_2, 0} (R := ℤ) (S₁ := R_1) fun (i : Fin (Nat.succ 0).succ × ℕ) ↦
            ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1)
              (![X, X] i.1 i.2 : MvPolynomial ℕ ℤ) :
          MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ →ₐ[ℤ] R_1) :
        (a : MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ) → R_1)
      (φ n) :
    R_1)
Tactic: simp +unfoldPartialApp only [hf, peval, uncurry, aeval_bind₁]
-- 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 : ℕ
⊢ Eq.{u_2 + 1} (α := R_1)
    (((aeval.{0, u_2, 0} (R := ℤ) (S₁ := R_1) fun (a : Fin 2 × ℕ) ↦ ![x.coeff, x.coeff] a.1 a.2 :
            MvPolynomial (Fin 2 × ℕ) ℤ →ₐ[ℤ] R_1) :
          (a : MvPolynomial (Fin 2 × ℕ) ℤ) → R_1)
        (φ n) :
      R_1)
    (((aeval.{0, u_2, 0} (R := ℤ) (S₁ := R_1) fun (i : Fin (Nat.succ 0).succ × ℕ) ↦
              ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1)
                (![X, X] i.1 i.2 : MvPolynomial ℕ ℤ) :
            MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ →ₐ[ℤ] R_1) :
          (a : MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ) → R_1)
        (φ n) :
      R_1)
have apply : Eq.{max 1 (u_2 + 1)} (α := Fin 2 × ℕ → R_1) (fun (a : Fin 2 × ℕ) ↦ ![x.coeff, x.coeff] a.1 a.2)
  fun (i : Fin (Nat.succ 0).succ × ℕ) ↦
  ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1)
    (![X, X] i.1 i.2 : MvPolynomial ℕ ℤ)
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
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 : ℕ
⊢ Eq.{max 1 (u_2 + 1)} (α := Fin 2 × ℕ → R_1) (fun (a : Fin 2 × ℕ) ↦ ![x.coeff, x.coeff] a.1 a.2)
    fun (i : Fin (Nat.succ 0).succ × ℕ) ↦
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1)
      (![X, X] i.1 i.2 : MvPolynomial ℕ ℤ)
have h : ∀ (i : Fin 2) (k : ℕ),
  ![x.coeff, x.coeff] (i, k).1 (i, k).2 =
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1)
      (![X, X] (i, k).1 (i, k).2 : MvPolynomial ℕ ℤ)
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
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 : ℕ
⊢ ![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) (⟨0, sorry⟩ : Fin 2), k).1 ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2), k).2 =
  ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1)
    (![X, X] ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2), k).1 ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩, k).2 : MvPolynomial ℕ ℤ)
Tactic: fin_cases i
Cleared hypotheses: i