awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → 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} ℤ)
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} ℤ)
have apply : Eq.{max 1 (u + 1)} (α := Fin 2 × ℕ → ULift.{u, 0} ℤ)
  (fun (i : Fin 2 × ℕ) ↦ ((↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) : (a : ℤ) → ULift.{u, 0} ℤ) (x i))
  (uncurry
    ![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: apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → 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} ℤ)
x_2 : ℕ
⊢ Eq.{max 1 (u + 1)} (α := Fin 2 × ℕ → ULift.{u, 0} ℤ)
    (fun (i : Fin 2 × ℕ) ↦
      ((↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) : (a : ℤ) → ULift.{u, 0} ℤ) (x i))
    (uncurry
      ![coeff (mk p fun (i : ℕ) ↦ { down := x (0, i) : ULift.{u, 0} ℤ }),
        coeff (mk p fun (i : ℕ) ↦ { down := x (1, i) : ULift.{u, 0} ℤ })])
have h₁ : ∀ (b : Fin 2) (snd : ℕ),
  Eq (α := ℤ)
    (ULift.down.{u, 0}
      (((↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) : (a : ℤ) → ULift.{u, 0} ℤ) (x (b, snd))))
    (ULift.down.{u, 0}
      (uncurry
        ![coeff (mk p fun (i : ℕ) ↦ { down := x (0, i) : ULift.{u, 0} ℤ }),
          coeff (mk p fun (i : ℕ) ↦ { down := x (1, i) : ULift.{u, 0} ℤ })]
        (b, snd)))
Tactic: ext ⟨b, _⟩
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → 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} ℤ)
x_2 : ℕ
b : Fin 2
snd : ℕ
⊢ Eq (α := ℤ)
    (ULift.down.{u, 0}
      (((↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) : (a : ℤ) → ULift.{u, 0} ℤ) (x (b, snd))))
    (ULift.down.{u, 0}
      (uncurry
        ![coeff (mk p fun (i : ℕ) ↦ { down := x (0, i) : ULift.{u, 0} ℤ }),
          coeff (mk p fun (i : ℕ) ↦ { down := x (1, i) : ULift.{u, 0} ℤ })]
        (b, snd)))
have h₁ : Eq (α := ℤ)
  (ULift.down.{u, 0}
    (((↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) : (a : ℤ) → ULift.{u, 0} ℤ)
      (x ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2), snd))))
  (ULift.down.{u, 0}
    (uncurry
      ![coeff (mk p fun (i : ℕ) ↦ { down := x (0, i) : ULift.{u, 0} ℤ }),
        coeff (mk p fun (i : ℕ) ↦ { down := x (1, i) : ULift.{u, 0} ℤ })]
      ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩, snd)))
Tactic: fin_cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → 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} ℤ)
x_2 : ℕ
b : Fin 2
snd : ℕ
h₁ :
  Eq (α := ℤ)
    (ULift.down.{u, 0}
      (((↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) : (a : ℤ) → ULift.{u, 0} ℤ)
        (x ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2), snd))))
    (ULift.down.{u, 0}
      (uncurry
        ![coeff (mk p fun (i : ℕ) ↦ { down := x (0, i) : ULift.{u, 0} ℤ }),
          coeff (mk p fun (i : ℕ) ↦ { down := x (1, i) : ULift.{u, 0} ℤ })]
        ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩, snd)))
⊢ Eq (α := ℤ)
    (ULift.down.{u, 0}
      (((↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) : (a : ℤ) → ULift.{u, 0} ℤ) (x (b, snd))))
    (ULift.down.{u, 0}
      (uncurry
        ![coeff (mk p fun (i : ℕ) ↦ { down := x (0, i) : ULift.{u, 0} ℤ }),
          coeff (mk p fun (i : ℕ) ↦ { down := x (1, i) : ULift.{u, 0} ℤ })]
        (b, snd)))
have h₂ : Eq (α := ℤ)
  (ULift.down.{u, 0}
    (((↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) : (a : ℤ) → ULift.{u, 0} ℤ)
      (x ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2), snd))))
  (ULift.down.{u, 0}
    (uncurry
      ![coeff (mk p fun (i : ℕ) ↦ { down := x (0, i) : ULift.{u, 0} ℤ }),
        coeff (mk p fun (i : ℕ) ↦ { down := x (1, i) : ULift.{u, 0} ℤ })]
      ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩, snd)))
Tactic: fin_cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → 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} ℤ)
x_2 snd : ℕ
⊢ Eq (α := ℤ)
    (ULift.down.{u, 0}
      (((↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) : (a : ℤ) → ULift.{u, 0} ℤ)
        (x ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2), snd))))
    (ULift.down.{u, 0}
      (uncurry
        ![coeff (mk p fun (i : ℕ) ↦ { down := x (0, i) : ULift.{u, 0} ℤ }),
          coeff (mk p fun (i : ℕ) ↦ { down := x (1, i) : ULift.{u, 0} ℤ })]
        ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩, snd)))
have h₁ : Eq (α := ℤ)
  (ULift.down.{u, 0}
    (((↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) : (a : ℤ) → ULift.{u, 0} ℤ)
      (x ((⟨0, sorry⟩ : Fin 2), snd))))
  (ULift.down.{u, 0}
    (![fun (i : ℕ) ↦ { down := x (0, i) }, fun (i : ℕ) ↦ { down := x (1, i) : ULift.{u, 0} ℤ }] ⟨0, sorry⟩ snd))
Tactic: simp only [coeff_mk, uncurry]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → 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} ℤ)
x_2 snd : ℕ
⊢ Eq (α := ℤ)
    (ULift.down.{u, 0}
      (((↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) : (a : ℤ) → ULift.{u, 0} ℤ)
        (x ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2), snd))))
    (ULift.down.{u, 0}
      (uncurry
        ![coeff (mk p fun (i : ℕ) ↦ { down := x (0, i) : ULift.{u, 0} ℤ }),
          coeff (mk p fun (i : ℕ) ↦ { down := x (1, i) : ULift.{u, 0} ℤ })]
        ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩, snd)))
have h₁ : Eq (α := ℤ)
  (ULift.down.{u, 0}
    (((↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) : (a : ℤ) → ULift.{u, 0} ℤ)
      (x ((⟨1, sorry⟩ : Fin 2), snd))))
  (ULift.down.{u, 0}
    (![fun (i : ℕ) ↦ { down := x (0, i) }, fun (i : ℕ) ↦ { down := x (1, i) : ULift.{u, 0} ℤ }] ⟨1, sorry⟩ snd))
Tactic: simp only [coeff_mk, uncurry]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → 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 (α := 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
              (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} ℤ)
have 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} ℤ)
Tactic: simp only [hf, hg, MvPolynomial.eval, map_eval₂Hom]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → 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 (α := 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} ℤ)
have 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} ℤ })]
Tactic: apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → 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.{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} ℤ })]
have 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} ℤ)
Tactic: ext1
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → 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} ℤ)
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} ℤ)
have apply : Eq.{max 1 (u + 1)} (α := Fin 2 × ℕ → ULift.{u, 0} ℤ)
  (fun (i : Fin 2 × ℕ) ↦ ((↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) : (a : ℤ) → ULift.{u, 0} ℤ) (x i))
  (uncurry
    ![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: apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
Goal:
p : ℕ
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
hf : IsPoly₂ p f
g : R →+* S
x y : 𝕎 R
⊢ Eq (α := 𝕎 S) ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) (f x y) : 𝕎 S)
    (f ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) x) ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) y) : 𝕎 S)
have obtain : ∀ (φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ)
  (hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun (n : ℕ) ↦ peval (φ n) ![x.coeff, y.coeff]),
  Eq (α := 𝕎 S) ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) (f x y) : 𝕎 S)
    (f ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) x) ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) y) : 𝕎 S)
Tactic: obtain ⟨φ, hf⟩ := hf
Cleared hypotheses: hf