awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.WittVector.IsPoly
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 : ℕ
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 × ℕ) ℚ)
⊢ 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

Premises used: funext_iff
-- Module: Mathlib.RingTheory.WittVector.IsPoly
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.{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
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
idx : Type u_1
inst : Fact (Nat.Prime p)
f g : ℕ → MvPolynomial (idx × ℕ) ℤ
n : ℕ
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))
⊢ 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:
simpa only [Function.comp_def, map_bind₁, map_wittPolynomial, ← bind₁_bind₁,
    bind₁_wittPolynomial_xInTermsOfW, bind₁_X_right] using h

Premises used: MvPolynomial.map_bind₁, Function.comp_def, MvPolynomial.bind₁_bind₁, map_wittPolynomial, bind₁_wittPolynomial_xInTermsOfW, MvPolynomial.bind₁_X_right
-- Module: Mathlib.RingTheory.WittVector.IsPoly
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 ℕ ℤ)
h₁ : ∀ (n : ℕ), f n = g n
⊢ f = g

Tactic:
ext1 n
-- Module: Mathlib.RingTheory.WittVector.IsPoly
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 : ℕ
h₁ :
  Eq (α := MvPolynomial ℕ ℚ)
    ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (f n) : MvPolynomial ℕ ℚ)
    ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (g n) : MvPolynomial ℕ ℚ)
⊢ f n = g n

Tactic:
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective

Premises used: Rat, MvPolynomial.map_injective, Int.castRingHom, Int.cast_injective
-- Module: Mathlib.RingTheory.WittVector.IsPoly
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 : ℕ
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 ℕ ℚ)
⊢ 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

Premises used: funext_iff
-- Module: Mathlib.RingTheory.WittVector.IsPoly
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 ℕ ℚ)
    ((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
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f g : ℕ → MvPolynomial ℕ ℤ
n : ℕ
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))
⊢ Eq (α := MvPolynomial ℕ ℚ)
    ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (f n) : MvPolynomial ℕ ℚ)
    ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (g n) : MvPolynomial ℕ ℚ)

Tactic:
simpa only [Function.comp_def, map_bind₁, map_wittPolynomial, ← bind₁_bind₁,
    bind₁_wittPolynomial_xInTermsOfW, bind₁_X_right] using h

Premises used: MvPolynomial.map_bind₁, Function.comp_def, MvPolynomial.bind₁_bind₁, map_wittPolynomial, bind₁_wittPolynomial_xInTermsOfW, MvPolynomial.bind₁_X_right
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
idx : Type u_1
inst : CommRing R
inst_1 : CommRing S
R_1 : Type u_2
inst_2 : CommRing R_1
x : 𝕎 R_1
⊢ (id x).coeff = fun (n : ℕ) ↦
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1) (X n)

Tactic:
simp only [aeval_X, id]

Premises used: MvPolynomial.aeval_X, id
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
idx : Type u_1
inst : CommRing R
inst_1 : CommRing S
⊢ IsPoly.{u_2} p fun (x : Type u_2) (x_1 : CommRing x) (a : 𝕎 x) ↦ a

Tactic:
WittVector.idIsPoly _

Premises used: WittVector.idIsPoly
-- Module: Mathlib.RingTheory.WittVector.IsPoly
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)
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
⊢ ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R), f x = g x

Tactic:
obtain ⟨φ, hf⟩ := hf
-- Module: Mathlib.RingTheory.WittVector.IsPoly
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)
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
⊢ ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R), f x = g x

Tactic:
obtain ⟨ψ, hg⟩ := hg
-- Module: Mathlib.RingTheory.WittVector.IsPoly
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
h₁ : ∀ (n : ℕ), (f x).coeff n = (g x).coeff n
⊢ f x = g x

Tactic:
ext n
-- Module: Mathlib.RingTheory.WittVector.IsPoly
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 : ℕ
h₁ :
  ∀ (n : ℕ),
    Eq (α := MvPolynomial ℕ ℤ)
      ((bind₁ φ : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n) : MvPolynomial ℕ ℤ)
      ((bind₁ ψ : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n) : MvPolynomial ℕ ℤ)
⊢ (f x).coeff n = (g x).coeff n

Tactic:
rw [hf, hg, poly_eq_of_wittPolynomial_bind_eq p φ ψ]

Premises used: WittVector.poly_eq_of_wittPolynomial_bind_eq
-- Module: Mathlib.RingTheory.WittVector.IsPoly
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 : ℕ
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 ℕ ℤ) :
        ℤ)
⊢ Eq (α := MvPolynomial ℕ ℤ)
    ((bind₁ φ : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k) : MvPolynomial ℕ ℤ)
    ((bind₁ ψ : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k) : MvPolynomial ℕ ℤ)

Tactic:
apply MvPolynomial.funext

Premises used: MvPolynomial.funext
-- Module: Mathlib.RingTheory.WittVector.IsPoly
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 : ℕ → ℤ
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) :
      ℤ)
⊢ 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:
simp only [hom_bind₁]

Premises used: MvPolynomial.hom_bind₁
-- Module: Mathlib.RingTheory.WittVector.IsPoly
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.{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

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

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

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

Tactic:
h