awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
Goal:
p : ℕ
idx : Type u_1
inst : Fact (Nat.Prime p)
f g : ℕ → MvPolynomial (idx × ℕ) ℤ
h :
  ∀ (n : ℕ),
    Eq (α := MvPolynomial (idx × ℕ) ℤ)
      ((bind₁ f : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittPolynomial p ℤ n) : MvPolynomial (idx × ℕ) ℤ)
      ((bind₁ g : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittPolynomial p ℤ n) : MvPolynomial (idx × ℕ) ℤ)
n : ℕ
⊢ f n = g n
have h₁ : Eq (α := MvPolynomial (idx × ℕ) ℚ)
  ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (f n) :
    MvPolynomial (idx × ℕ) ℚ)
  ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (g n) :
    MvPolynomial (idx × ℕ) ℚ)
Tactic: apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
Goal:
p : ℕ
idx : Type u_1
inst : Fact (Nat.Prime p)
f g : ℕ → MvPolynomial (idx × ℕ) ℤ
h :
  ∀ (n : ℕ),
    Eq (α := MvPolynomial (idx × ℕ) ℤ)
      ((bind₁ f : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittPolynomial p ℤ n) : MvPolynomial (idx × ℕ) ℤ)
      ((bind₁ g : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittPolynomial p ℤ n) : MvPolynomial (idx × ℕ) ℤ)
n : ℕ
⊢ Eq (α := MvPolynomial (idx × ℕ) ℚ)
    ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (f n) :
      MvPolynomial (idx × ℕ) ℚ)
    ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (g n) :
      MvPolynomial (idx × ℕ) ℚ)
have h₁ : ∀
  (h :
    Eq.{max 1 (u_1 + 1)} (α := (x : ℕ) → MvPolynomial (idx × ℕ) ℤ)
      (fun (n : ℕ) ↦ (bind₁ f : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittPolynomial p ℤ n)) fun (n : ℕ) ↦
      (bind₁ g : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittPolynomial p ℤ n))
  (n : ℕ),
  Eq (α := MvPolynomial (idx × ℕ) ℚ)
    ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (f n) :
      MvPolynomial (idx × ℕ) ℚ)
    ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (g n) :
      MvPolynomial (idx × ℕ) ℚ)
Tactic: rw [← funext_iff] at h
Cleared hypotheses: h, n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (hypothesis)
Goal:
p : ℕ
idx : Type u_1
inst : Fact (Nat.Prime p)
f g : ℕ → MvPolynomial (idx × ℕ) ℤ
h :
  Eq.{max 1 (u_1 + 1)} (α := (x : ℕ) → MvPolynomial (idx × ℕ) ℤ)
    (fun (n : ℕ) ↦ (bind₁ f : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittPolynomial p ℤ n)) fun (n : ℕ) ↦
    (bind₁ g : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittPolynomial p ℤ n)
n : ℕ
⊢ Eq (α := MvPolynomial (idx × ℕ) ℚ)
    ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (f n) :
      MvPolynomial (idx × ℕ) ℚ)
    ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (g n) :
      MvPolynomial (idx × ℕ) ℚ)
have h₁ : Eq.{u_1 + 1} (α := MvPolynomial (idx × ℕ) ℚ)
  ((fun (fam : ℕ → MvPolynomial (idx × ℕ) ℤ) ↦
      ((bind₁
              ((⇑(MvPolynomial.map (Int.castRingHom ℚ)) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) ∘
                fam) :
            (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
          (xInTermsOfW p ℚ n) :
        MvPolynomial (idx × ℕ) ℚ))
    fun (n : ℕ) ↦ (bind₁ f : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittPolynomial p ℤ n))
  ((fun (fam : ℕ → MvPolynomial (idx × ℕ) ℤ) ↦
      ((bind₁
              ((⇑(MvPolynomial.map (Int.castRingHom ℚ)) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) ∘
                fam) :
            (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
          (xInTermsOfW p ℚ n) :
        MvPolynomial (idx × ℕ) ℚ))
    fun (n : ℕ) ↦ (bind₁ g : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittPolynomial p ℤ n))
Tactic: replace h :=
    congr_arg (fun fam => bind₁ (MvPolynomial.map (Int.castRingHom ℚ) ∘ fam) (xInTermsOfW p ℚ n)) h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f g : ℕ → MvPolynomial ℕ ℤ
h :
  ∀ (n : ℕ),
    Eq (α := MvPolynomial ℕ ℤ)
      ((bind₁ f : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n) : MvPolynomial ℕ ℤ)
      ((bind₁ g : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n) : MvPolynomial ℕ ℤ)
⊢ f = g
have h₁ : ∀ (n : ℕ), f n = g n
Tactic: ext1 n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f g : ℕ → MvPolynomial ℕ ℤ
h :
  ∀ (n : ℕ),
    Eq (α := MvPolynomial ℕ ℤ)
      ((bind₁ f : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n) : MvPolynomial ℕ ℤ)
      ((bind₁ g : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n) : MvPolynomial ℕ ℤ)
n : ℕ
⊢ f n = g n
have h₁ : Eq (α := MvPolynomial ℕ ℚ)
  ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (f n) : MvPolynomial ℕ ℚ)
  ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (g n) : MvPolynomial ℕ ℚ)
Tactic: apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f g : ℕ → MvPolynomial ℕ ℤ
h :
  ∀ (n : ℕ),
    Eq (α := MvPolynomial ℕ ℤ)
      ((bind₁ f : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n) : MvPolynomial ℕ ℤ)
      ((bind₁ g : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n) : MvPolynomial ℕ ℤ)
n : ℕ
⊢ Eq (α := MvPolynomial ℕ ℚ)
    ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (f n) : MvPolynomial ℕ ℚ)
    ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (g n) : MvPolynomial ℕ ℚ)
have h₁ : ∀
  (h :
    Eq (α := (x : ℕ) → MvPolynomial ℕ ℤ)
      (fun (n : ℕ) ↦ (bind₁ f : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n)) fun (n : ℕ) ↦
      (bind₁ g : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n))
  (n : ℕ),
  Eq (α := MvPolynomial ℕ ℚ)
    ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (f n) : MvPolynomial ℕ ℚ)
    ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (g n) : MvPolynomial ℕ ℚ)
Tactic: rw [← funext_iff] at h
Cleared hypotheses: h, n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f g : ℕ → MvPolynomial ℕ ℤ
h :
  Eq (α := (x : ℕ) → MvPolynomial ℕ ℤ)
    (fun (n : ℕ) ↦ (bind₁ f : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n)) fun (n : ℕ) ↦
    (bind₁ g : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n)
n : ℕ
⊢ Eq (α := MvPolynomial ℕ ℚ)
    ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (f n) : MvPolynomial ℕ ℚ)
    ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (g n) : MvPolynomial ℕ ℚ)
have h₁ : Eq (α := MvPolynomial ℕ ℚ)
  ((fun (fam : ℕ → MvPolynomial ℕ ℤ) ↦
      ((bind₁ ((⇑(MvPolynomial.map (Int.castRingHom ℚ)) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) ∘ fam) :
            (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ)
          (xInTermsOfW p ℚ n) :
        MvPolynomial ℕ ℚ))
    fun (n : ℕ) ↦ (bind₁ f : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n))
  ((fun (fam : ℕ → MvPolynomial ℕ ℤ) ↦
      ((bind₁ ((⇑(MvPolynomial.map (Int.castRingHom ℚ)) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) ∘ fam) :
            (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ)
          (xInTermsOfW p ℚ n) :
        MvPolynomial ℕ ℚ))
    fun (n : ℕ) ↦ (bind₁ g : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n))
Tactic: replace h :=
    congr_arg (fun fam => bind₁ (MvPolynomial.map (Int.castRingHom ℚ) ∘ fam) (xInTermsOfW p ℚ n)) h
Cleared hypotheses: h
-- 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
hf : IsPoly p f
hg : IsPoly p g
h :
  ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ),
    Eq (α := R) ((ghostComponent n : (a : 𝕎 R) → R) (f x) : R) ((ghostComponent n : (a : 𝕎 R) → R) (g x) : R)
⊢ ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R), f x = g x
have obtain : ∀ (φ : ℕ → MvPolynomial ℕ ℤ)
  (hf :
    ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R),
      (f x).coeff = fun (n : ℕ) ↦ (aeval x.coeff : (a : MvPolynomial ℕ ℤ) → R) (φ n))
  (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R), f x = g x
Tactic: obtain ⟨φ, hf⟩ := hf
Cleared hypotheses: hf
-- 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
hg : IsPoly p g
h :
  ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ),
    Eq (α := R) ((ghostComponent n : (a : 𝕎 R) → R) (f x) : R) ((ghostComponent n : (a : 𝕎 R) → R) (g x) : R)
φ : ℕ → MvPolynomial ℕ ℤ
hf :
  ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R),
    (f x).coeff = fun (n : ℕ) ↦ (aeval x.coeff : (a : MvPolynomial ℕ ℤ) → R) (φ n)
⊢ ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R), f x = g x
have obtain : ∀ (ψ : ℕ → 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 : 𝕎 R), f x = g x
Tactic: obtain ⟨ψ, hg⟩ := hg
Cleared hypotheses: hg
-- 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
h :
  ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ),
    Eq (α := R) ((ghostComponent n : (a : 𝕎 R) → R) (f x) : R) ((ghostComponent n : (a : 𝕎 R) → R) (g x) : 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 : 𝕎 R
⊢ f x = g x
have h₁ : ∀ (n : ℕ), (f x).coeff n = (g x).coeff n
Tactic: ext n
-- 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
h :
  ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ),
    Eq (α := R) ((ghostComponent n : (a : 𝕎 R) → R) (f x) : R) ((ghostComponent n : (a : 𝕎 R) → R) (g x) : 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 : 𝕎 R
n : ℕ
⊢ (f x).coeff n = (g x).coeff n
have h₁ : ∀ (n : ℕ),
  Eq (α := MvPolynomial ℕ ℤ)
    ((bind₁ φ : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n) : MvPolynomial ℕ ℤ)
    ((bind₁ ψ : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n) : MvPolynomial ℕ ℤ)
Tactic: rw [hf, hg, poly_eq_of_wittPolynomial_bind_eq p φ ψ]
-- 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
h :
  ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ),
    Eq (α := R) ((ghostComponent n : (a : 𝕎 R) → R) (f x) : R) ((ghostComponent n : (a : 𝕎 R) → R) (g x) : 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 : 𝕎 R
n k : ℕ
⊢ Eq (α := MvPolynomial ℕ ℤ)
    ((bind₁ φ : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k) : MvPolynomial ℕ ℤ)
    ((bind₁ ψ : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k) : MvPolynomial ℕ ℤ)
have h₁ : ∀ (x : ℕ → ℤ),
  Eq (α := ℤ)
    ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ)
        ((bind₁ φ : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k) : MvPolynomial ℕ ℤ) :
      ℤ)
    ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ)
        ((bind₁ ψ : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k) : MvPolynomial ℕ ℤ) :
      ℤ)
Tactic: apply MvPolynomial.funext
-- 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
h :
  ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ),
    Eq (α := R) ((ghostComponent n : (a : 𝕎 R) → R) (f x) : R) ((ghostComponent n : (a : 𝕎 R) → R) (g x) : 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 : ℕ → ℤ
⊢ Eq (α := ℤ)
    ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ)
        ((bind₁ φ : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k) : MvPolynomial ℕ ℤ) :
      ℤ)
    ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ)
        ((bind₁ ψ : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k) : MvPolynomial ℕ ℤ) :
      ℤ)
have h₁ : Eq (α := ℤ)
  ((eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun (i : ℕ) ↦
          (MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (φ i) :
        (a : MvPolynomial ℕ ℤ) → ℤ)
      (wittPolynomial p ℤ k) :
    ℤ)
  ((eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun (i : ℕ) ↦
          (MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (ψ i) :
        (a : MvPolynomial ℕ ℤ) → ℤ)
      (wittPolynomial p ℤ k) :
    ℤ)
Tactic: simp only [hom_bind₁]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R
h :
  ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ),
    Eq (α := R) ((ghostComponent n : (a : 𝕎 R) → R) (f x) : R) ((ghostComponent n : (a : 𝕎 R) → R) (g x) : 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 : ℕ → ℤ
⊢ Eq (α := ℤ)
    ((eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun (i : ℕ) ↦
            (MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (φ i) :
          (a : MvPolynomial ℕ ℤ) → ℤ)
        (wittPolynomial p ℤ k) :
      ℤ)
    ((eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun (i : ℕ) ↦
            (MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (ψ i) :
          (a : MvPolynomial ℕ ℤ) → ℤ)
        (wittPolynomial p ℤ k) :
      ℤ)
have h₁ : Eq.{u + 1} (α := ULift.{u, 0} ℤ)
  ((ghostComponent k : (a : 𝕎 (ULift.{u, 0} ℤ)) → ULift.{u, 0} ℤ) (f (mk p fun (i : ℕ) ↦ { down := x i })) :
    ULift.{u, 0} ℤ)
  ((ghostComponent k : (a : 𝕎 (ULift.{u, 0} ℤ)) → ULift.{u, 0} ℤ) (g (mk p fun (i : ℕ) ↦ { down := x i })) :
    ULift.{u, 0} ℤ)
Tactic: specialize h (ULift ℤ) (mk p fun i => ⟨x i⟩) k
Cleared hypotheses: h
-- 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
φ : ℕ → 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} ℤ)
⊢ Eq (α := ℤ)
    ((eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun (i : ℕ) ↦
            (MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (φ i) :
          (a : MvPolynomial ℕ ℤ) → ℤ)
        (wittPolynomial p ℤ k) :
      ℤ)
    ((eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun (i : ℕ) ↦
            (MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (ψ i) :
          (a : MvPolynomial ℕ ℤ) → ℤ)
        (wittPolynomial p ℤ k) :
      ℤ)
have h₁ : Eq.{u + 1} (α := ULift.{u, 0} ℤ)
  ((RingEquiv.symm ULift.ringEquiv : (a : ℤ) → ULift.{u, 0} ℤ)
      ((eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun (i : ℕ) ↦
              (MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (φ i) :
            (a : MvPolynomial ℕ ℤ) → ℤ)
          (wittPolynomial p ℤ k) :
        ℤ) :
    ULift.{u, 0} ℤ)
  ((RingEquiv.symm ULift.ringEquiv : (a : ℤ) → ULift.{u, 0} ℤ)
      ((eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun (i : ℕ) ↦
              (MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (ψ i) :
            (a : MvPolynomial ℕ ℤ) → ℤ)
          (wittPolynomial p ℤ k) :
        ℤ) :
    ULift.{u, 0} ℤ)
Tactic: apply (ULift.ringEquiv.symm : ℤ ≃+* _).injective
-- 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
φ : ℕ → 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} ℤ)
⊢ Eq.{u + 1} (α := ULift.{u, 0} ℤ)
    ((RingEquiv.symm ULift.ringEquiv : (a : ℤ) → ULift.{u, 0} ℤ)
        ((eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun (i : ℕ) ↦
                (MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (φ i) :
              (a : MvPolynomial ℕ ℤ) → ℤ)
            (wittPolynomial p ℤ k) :
          ℤ) :
      ULift.{u, 0} ℤ)
    ((RingEquiv.symm ULift.ringEquiv : (a : ℤ) → ULift.{u, 0} ℤ)
        ((eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun (i : ℕ) ↦
                (MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (ψ i) :
              (a : MvPolynomial ℕ ℤ) → ℤ)
            (wittPolynomial p ℤ k) :
          ℤ) :
      ULift.{u, 0} ℤ)
have h₁ : Eq (α := ULift.{u, 0} ℤ)
  ((eval₂Hom
          (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ)
            (RingHom.comp (MvPolynomial.eval x) C))
          fun (i : ℕ) ↦
          ((↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) : (a : ℤ) → ULift.{u, 0} ℤ)
            ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (φ i) : ℤ) :
        (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
      (wittPolynomial p ℤ k) :
    ULift.{u, 0} ℤ)
  ((eval₂Hom
          (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ)
            (RingHom.comp (MvPolynomial.eval x) C))
          fun (i : ℕ) ↦
          ((↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) : (a : ℤ) → ULift.{u, 0} ℤ)
            ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (ψ i) : ℤ) :
        (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
      (wittPolynomial p ℤ k) :
    ULift.{u, 0} ℤ)
Tactic: simp only [← RingEquiv.coe_toRingHom, 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
φ : ℕ → 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} ℤ)
⊢ 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
            (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} ℤ)
have h₁ : Eq (α := ULift.{u, 0} ℤ)
  ((eval₂Hom
          (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ)
            (RingHom.comp (MvPolynomial.eval x) C))
          fun (i : ℕ) ↦
          ((↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) : (a : ℤ) → ULift.{u, 0} ℤ)
            ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) (φ 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: convert! h using 1