awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x y : 𝕎 R
h h₁ : ∀ (n : ℕ), (x - y).ghostFun n = (x.ghostFun - y.ghostFun) n
h₂ h₃ :
  ∀ (n : ℕ),
    peval
          ((bind₁ (wittStructureInt p (HSub.hSub (α := MvPolynomial (Fin (Nat.succ 0).succ) ℤ) (X 0) (X 1))) :
              (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ)
            (W_ ℤ n))
          ![x.coeff, y.coeff] =
        peval
          ((bind₁ fun (i : Fin (Nat.succ 0).succ) ↦
                (rename (Prod.mk i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ) (W_ ℤ n) :
              (a : MvPolynomial (Fin (Nat.succ 0).succ) ℤ) → MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ)
            (HSub.hSub (α := MvPolynomial (Fin (Nat.succ 0).succ) ℤ) (X 0) (X 1)))
          ![x.coeff, y.coeff] →
      (x - y).ghostFun n = (x.ghostFun - y.ghostFun) n
h₄ h₅ :
  ∀ (n : ℕ),
    peval
          ((bind₁ (wittStructureInt p (HSub.hSub (α := MvPolynomial (Fin (Nat.succ 0).succ) ℤ) (X 0) (X 1))) :
              (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ)
            (W_ ℤ n))
          ![x.coeff, y.coeff] =
        peval
          ((bind₁ fun (i : Fin (Nat.succ 0).succ) ↦
                (rename (Prod.mk i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ) (W_ ℤ n) :
              (a : MvPolynomial (Fin (Nat.succ 0).succ) ℤ) → MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ)
            (HSub.hSub (α := MvPolynomial (Fin (Nat.succ 0).succ) ℤ) (X 0) (X 1)))
          ![x.coeff, y.coeff] →
      (eval (wittSub p) ![x, y]).ghostFun n = Sub.sub (x.ghostFun n) (y.ghostFun n)
⊢ (x - y).ghostFun = x.ghostFun - y.ghostFun

Tactic:
ghost_fun_tac X 0 - X 1, ![x.coeff, y.coeff]

Premises used: MvPolynomial.X, WittVector.coeff, OfNat.ofNat
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x y : 𝕎 R
h h₁ : ∀ (n : ℕ), (x * y).ghostFun n = (x.ghostFun * y.ghostFun) n
h₂ h₃ :
  ∀ (n : ℕ),
    peval
          ((bind₁ (wittStructureInt p (HMul.hMul (α := MvPolynomial (Fin (Nat.succ 0).succ) ℤ) (X 0) (X 1))) :
              (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ)
            (W_ ℤ n))
          ![x.coeff, y.coeff] =
        peval
          ((bind₁ fun (i : Fin (Nat.succ 0).succ) ↦
                (rename (Prod.mk i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ) (W_ ℤ n) :
              (a : MvPolynomial (Fin (Nat.succ 0).succ) ℤ) → MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ)
            (HMul.hMul (α := MvPolynomial (Fin (Nat.succ 0).succ) ℤ) (X 0) (X 1)))
          ![x.coeff, y.coeff] →
      (x * y).ghostFun n = (x.ghostFun * y.ghostFun) n
h₄ h₅ :
  ∀ (n : ℕ),
    peval
          ((bind₁ (wittStructureInt p (HMul.hMul (α := MvPolynomial (Fin (Nat.succ 0).succ) ℤ) (X 0) (X 1))) :
              (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ)
            (W_ ℤ n))
          ![x.coeff, y.coeff] =
        peval
          ((bind₁ fun (i : Fin (Nat.succ 0).succ) ↦
                (rename (Prod.mk i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ) (W_ ℤ n) :
              (a : MvPolynomial (Fin (Nat.succ 0).succ) ℤ) → MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ)
            (HMul.hMul (α := MvPolynomial (Fin (Nat.succ 0).succ) ℤ) (X 0) (X 1)))
          ![x.coeff, y.coeff] →
      (eval (wittMul p) ![x, y]).ghostFun n = Mul.mul (x.ghostFun n) (y.ghostFun n)
⊢ (x * y).ghostFun = x.ghostFun * y.ghostFun

Tactic:
ghost_fun_tac X 0 * X 1, ![x.coeff, y.coeff]

Premises used: MvPolynomial.X, WittVector.coeff, OfNat.ofNat
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x : 𝕎 R
h h₁ : ∀ (n : ℕ), (-x).ghostFun n = (-x.ghostFun) n
h₂ h₃ :
  ∀ (n : ℕ),
    peval
          ((bind₁ (wittStructureInt p (-X 0)) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin (Nat.succ 0) × ℕ) ℤ)
            (W_ ℤ n))
          ![x.coeff] =
        peval
          ((bind₁ fun (i : Fin (Nat.succ 0)) ↦
                (rename (Prod.mk i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin (Nat.succ 0) × ℕ) ℤ) (W_ ℤ n) :
              (a : MvPolynomial (Fin (Nat.succ 0)) ℤ) → MvPolynomial (Fin (Nat.succ 0) × ℕ) ℤ)
            (-X 0))
          ![x.coeff] →
      (-x).ghostFun n = (-x.ghostFun) n
h₄ h₅ :
  ∀ (n : ℕ),
    peval
          ((bind₁ (wittStructureInt p (-X 0)) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin (Nat.succ 0) × ℕ) ℤ)
            (W_ ℤ n))
          ![x.coeff] =
        peval
          ((bind₁ fun (i : Fin (Nat.succ 0)) ↦
                (rename (Prod.mk i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin (Nat.succ 0) × ℕ) ℤ) (W_ ℤ n) :
              (a : MvPolynomial (Fin (Nat.succ 0)) ℤ) → MvPolynomial (Fin (Nat.succ 0) × ℕ) ℤ)
            (-X 0))
          ![x.coeff] →
      (eval (wittNeg p) ![x]).ghostFun n = -x.ghostFun n
⊢ (-x).ghostFun = -x.ghostFun

Tactic:
ghost_fun_tac -X 0, ![x.coeff]

Premises used: MvPolynomial.X, WittVector.coeff, OfNat.ofNat
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
i : ℤ
ofNat : ∀ (a : ℕ), Eq.{u_1 + 1} (α := ℕ → R) (ghostFun (p := p) (Int.ofNat a).castDef) (↑(Int.ofNat a) : ℕ → R)
negSucc : ∀ (a : ℕ), Eq.{u_1 + 1} (α := ℕ → R) (ghostFun (p := p) (Int.negSucc a).castDef) (↑(Int.negSucc a) : ℕ → R)
⊢ Eq.{u_1 + 1} (α := ℕ → R) (ghostFun (p := p) i.castDef) (↑i : ℕ → R)

Tactic:
cases i
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
a : ℕ
⊢ Eq.{u_1 + 1} (α := ℕ → R) (ghostFun (p := p) (Int.ofNat a).castDef) (↑(Int.ofNat a) : ℕ → R)

Tactic:
simp [*, Int.castDef, ghostFun_natCast, ghostFun_neg]

Premises used: _private.0.WittVector.ghostFun_natCast, Int.castDef, _private.0.WittVector.ghostFun_neg
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
a : ℕ
⊢ Eq.{u_1 + 1} (α := ℕ → R) (ghostFun (p := p) (Int.negSucc a).castDef) (↑(Int.negSucc a) : ℕ → R)

Tactic:
simp [*, Int.castDef, ghostFun_natCast, ghostFun_neg]

Premises used: _private.0.WittVector.ghostFun_natCast, Int.castDef, _private.0.WittVector.ghostFun_neg
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
m : ℕ
x : 𝕎 R
h h₁ : ∀ (n : ℕ), (m • x).ghostFun n = (m • x.ghostFun) n
h₂ h₃ :
  ∀ (n : ℕ),
    peval
          ((bind₁ (wittStructureInt p (HSMul.hSMul (β := MvPolynomial (Fin (Nat.succ 0)) ℤ) m (X 0))) :
              (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin (Nat.succ 0) × ℕ) ℤ)
            (W_ ℤ n))
          ![x.coeff] =
        peval
          ((bind₁ fun (i : Fin (Nat.succ 0)) ↦
                (rename (Prod.mk i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin (Nat.succ 0) × ℕ) ℤ) (W_ ℤ n) :
              (a : MvPolynomial (Fin (Nat.succ 0)) ℤ) → MvPolynomial (Fin (Nat.succ 0) × ℕ) ℤ)
            (HSMul.hSMul (β := MvPolynomial (Fin (Nat.succ 0)) ℤ) m (X 0)))
          ![x.coeff] →
      (m • x).ghostFun n = (m • x.ghostFun) n
h₄ h₅ :
  ∀ (n : ℕ),
    peval
          ((bind₁ (wittStructureInt p (HSMul.hSMul (β := MvPolynomial (Fin (Nat.succ 0)) ℤ) m (X 0))) :
              (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin (Nat.succ 0) × ℕ) ℤ)
            (W_ ℤ n))
          ![x.coeff] =
        peval
          ((bind₁ fun (i : Fin (Nat.succ 0)) ↦
                (rename (Prod.mk i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin (Nat.succ 0) × ℕ) ℤ) (W_ ℤ n) :
              (a : MvPolynomial (Fin (Nat.succ 0)) ℤ) → MvPolynomial (Fin (Nat.succ 0) × ℕ) ℤ)
            (HSMul.hSMul (β := MvPolynomial (Fin (Nat.succ 0)) ℤ) m (X 0)))
          ![x.coeff] →
      (eval (wittStructureInt p (AddMonoid.nsmul m (X (Fin.ofNat 1 0)))) ![x]).ghostFun n =
        AddMonoid.nsmul m x.ghostFun n
⊢ (m • x).ghostFun = m • x.ghostFun

Tactic:
ghost_fun_tac m • (X 0), ![x.coeff]

Premises used: MvPolynomial.X, WittVector.coeff, OfNat.ofNat
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
m : ℤ
x : 𝕎 R
h h₁ : ∀ (n : ℕ), (m • x).ghostFun n = (m • x.ghostFun) n
h₂ h₃ :
  ∀ (n : ℕ),
    peval
          ((bind₁ (wittStructureInt p (HSMul.hSMul (β := MvPolynomial (Fin (Nat.succ 0)) ℤ) m (X 0))) :
              (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin (Nat.succ 0) × ℕ) ℤ)
            (W_ ℤ n))
          ![x.coeff] =
        peval
          ((bind₁ fun (i : Fin (Nat.succ 0)) ↦
                (rename (Prod.mk i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin (Nat.succ 0) × ℕ) ℤ) (W_ ℤ n) :
              (a : MvPolynomial (Fin (Nat.succ 0)) ℤ) → MvPolynomial (Fin (Nat.succ 0) × ℕ) ℤ)
            (HSMul.hSMul (β := MvPolynomial (Fin (Nat.succ 0)) ℤ) m (X 0)))
          ![x.coeff] →
      (m • x).ghostFun n = (m • x.ghostFun) n
h₄ h₅ :
  ∀ (n : ℕ),
    peval
          ((bind₁ (wittStructureInt p (HSMul.hSMul (β := MvPolynomial (Fin (Nat.succ 0)) ℤ) m (X 0))) :
              (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin (Nat.succ 0) × ℕ) ℤ)
            (W_ ℤ n))
          ![x.coeff] =
        peval
          ((bind₁ fun (i : Fin (Nat.succ 0)) ↦
                (rename (Prod.mk i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin (Nat.succ 0) × ℕ) ℤ) (W_ ℤ n) :
              (a : MvPolynomial (Fin (Nat.succ 0)) ℤ) → MvPolynomial (Fin (Nat.succ 0) × ℕ) ℤ)
            (HSMul.hSMul (β := MvPolynomial (Fin (Nat.succ 0)) ℤ) m (X 0)))
          ![x.coeff] →
      (eval (wittStructureInt p (SubNegMonoid.zsmul m (X (Fin.ofNat 1 0)))) ![x]).ghostFun n =
        SubNegMonoid.zsmul m x.ghostFun n
⊢ (m • x).ghostFun = m • x.ghostFun

Tactic:
ghost_fun_tac m • (X 0), ![x.coeff]

Premises used: MvPolynomial.X, WittVector.coeff, OfNat.ofNat
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x : 𝕎 R
m : ℕ
h h₁ : ∀ (n : ℕ), (x ^ m).ghostFun n = (x.ghostFun ^ m) n
h₂ h₃ :
  ∀ (n : ℕ),
    peval
          ((bind₁ (wittStructureInt p (HPow.hPow (α := MvPolynomial (Fin (Nat.succ 0)) ℤ) (X 0) m)) :
              (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin (Nat.succ 0) × ℕ) ℤ)
            (W_ ℤ n))
          ![x.coeff] =
        peval
          ((bind₁ fun (i : Fin (Nat.succ 0)) ↦
                (rename (Prod.mk i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin (Nat.succ 0) × ℕ) ℤ) (W_ ℤ n) :
              (a : MvPolynomial (Fin (Nat.succ 0)) ℤ) → MvPolynomial (Fin (Nat.succ 0) × ℕ) ℤ)
            (HPow.hPow (α := MvPolynomial (Fin (Nat.succ 0)) ℤ) (X 0) m))
          ![x.coeff] →
      (x ^ m).ghostFun n = (x.ghostFun ^ m) n
h₄ h₅ :
  ∀ (n : ℕ),
    peval
          ((bind₁ (wittStructureInt p (HPow.hPow (α := MvPolynomial (Fin (Nat.succ 0)) ℤ) (X 0) m)) :
              (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin (Nat.succ 0) × ℕ) ℤ)
            (W_ ℤ n))
          ![x.coeff] =
        peval
          ((bind₁ fun (i : Fin (Nat.succ 0)) ↦
                (rename (Prod.mk i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin (Nat.succ 0) × ℕ) ℤ) (W_ ℤ n) :
              (a : MvPolynomial (Fin (Nat.succ 0)) ℤ) → MvPolynomial (Fin (Nat.succ 0) × ℕ) ℤ)
            (HPow.hPow (α := MvPolynomial (Fin (Nat.succ 0)) ℤ) (X 0) m))
          ![x.coeff] →
      (eval (wittPow p m) ![x]).ghostFun n = Monoid.npow m (x.ghostFun n)
⊢ (x ^ m).ghostFun = x.ghostFun ^ m

Tactic:
ghost_fun_tac X 0 ^ m, ![x.coeff]

Premises used: MvPolynomial.X, WittVector.coeff, OfNat.ofNat
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
α : Type u_3
β : Type u_4
inst_2 : Invertible (α := R) (↑p : R)
x : 𝕎 R
h :
  ∀ (n : ℕ),
    coeff (p := p)
        ((fun (x : ℕ → R) ↦ (mk p fun (n : ℕ) ↦ (aeval x : (a : MvPolynomial ℕ R) → R) (xInTermsOfW p R n) : 𝕎 R))
          x.ghostFun)
        n =
      x.coeff n
⊢ (fun (x : ℕ → R) ↦ (mk p fun (n : ℕ) ↦ (aeval x : (a : MvPolynomial ℕ R) → R) (xInTermsOfW p R n) : 𝕎 R)) x.ghostFun =
    x

Tactic:
ext n
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
α : Type u_3
β : Type u_4
inst_2 : Invertible (α := R) (↑p : R)
x : 𝕎 R
n : ℕ
⊢ Eq (α := MvPolynomial ℕ R)
    ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R n) : MvPolynomial ℕ R)
    (X n : MvPolynomial ℕ R)

Tactic:
have := bind₁_wittPolynomial_xInTermsOfW p R n
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
α : Type u_3
β : Type u_4
inst_2 : Invertible (α := R) (↑p : R)
x : 𝕎 R
n : ℕ
this :
  Eq (α := MvPolynomial ℕ R)
    ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R n) : MvPolynomial ℕ R)
    (X n : MvPolynomial ℕ R)
⊢ Eq (α := R)
    ((aeval x.coeff : (a : MvPolynomial ℕ R) → R)
        ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R n) : MvPolynomial ℕ R) :
      R)
    ((aeval x.coeff : (a : MvPolynomial ℕ R) → R) (X n) : R)

Tactic:
apply_fun aeval x.coeff at this

Premises used: MvPolynomial.aeval, WittVector.coeff
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
α : Type u_3
β : Type u_4
inst_2 : Invertible (α := R) (↑p : R)
x : 𝕎 R
n : ℕ
this :
  Eq (α := R)
    ((aeval x.coeff : (a : MvPolynomial ℕ R) → R)
        ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R n) : MvPolynomial ℕ R) :
      R)
    ((aeval x.coeff : (a : MvPolynomial ℕ R) → R) (X n) : R)
⊢ coeff (p := p)
      ((fun (x : ℕ → R) ↦ (mk p fun (n : ℕ) ↦ (aeval x : (a : MvPolynomial ℕ R) → R) (xInTermsOfW p R n) : 𝕎 R))
        x.ghostFun)
      n =
    x.coeff n

Tactic:
simpa +unfoldPartialApp only [aeval_bind₁, aeval_X, ghostFun,
      aeval_wittPolynomial]

Premises used: aeval_wittPolynomial, MvPolynomial.aeval_X, MvPolynomial.aeval_bind₁, _private.0.WittVector.ghostFun
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
α : Type u_3
β : Type u_4
inst_2 : Invertible (α := R) (↑p : R)
x : ℕ → R
h :
  ∀ (n : ℕ),
    ghostFun (p := p)
        ((fun (x : ℕ → R) ↦ (mk p fun (n : ℕ) ↦ (aeval x : (a : MvPolynomial ℕ R) → R) (xInTermsOfW p R n) : 𝕎 R)) x)
        n =
      x n
⊢ ghostFun (p := p)
      ((fun (x : ℕ → R) ↦ (mk p fun (n : ℕ) ↦ (aeval x : (a : MvPolynomial ℕ R) → R) (xInTermsOfW p R n) : 𝕎 R)) x) =
    x

Tactic:
ext n
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
α : Type u_3
β : Type u_4
inst_2 : Invertible (α := R) (↑p : R)
x : ℕ → R
n : ℕ
⊢ Eq (α := MvPolynomial ℕ R)
    ((bind₁ (xInTermsOfW p R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (W_ R n) : MvPolynomial ℕ R)
    (X n : MvPolynomial ℕ R)

Tactic:
have := bind₁_xInTermsOfW_wittPolynomial p R n
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
α : Type u_3
β : Type u_4
inst_2 : Invertible (α := R) (↑p : R)
x : ℕ → R
n : ℕ
this :
  Eq (α := MvPolynomial ℕ R)
    ((bind₁ (xInTermsOfW p R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (W_ R n) : MvPolynomial ℕ R)
    (X n : MvPolynomial ℕ R)
⊢ Eq (α := R)
    ((aeval x : (a : MvPolynomial ℕ R) → R)
        ((bind₁ (xInTermsOfW p R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (W_ R n) : MvPolynomial ℕ R) :
      R)
    ((aeval x : (a : MvPolynomial ℕ R) → R) (X n) : R)

Tactic:
apply_fun aeval x at this

Premises used: MvPolynomial.aeval
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
α : Type u_3
β : Type u_4
inst_2 : Invertible (α := R) (↑p : R)
x : ℕ → R
n : ℕ
this :
  Eq (α := R)
    ((aeval x : (a : MvPolynomial ℕ R) → R)
        ((bind₁ (xInTermsOfW p R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (W_ R n) : MvPolynomial ℕ R) :
      R)
    ((aeval x : (a : MvPolynomial ℕ R) → R) (X n) : R)
⊢ ghostFun (p := p)
      ((fun (x : ℕ → R) ↦ (mk p fun (n : ℕ) ↦ (aeval x : (a : MvPolynomial ℕ R) → R) (xInTermsOfW p R n) : 𝕎 R)) x) n =
    x n

Tactic:
simpa only [aeval_bind₁, aeval_X, ghostFun, aeval_wittPolynomial]

Premises used: aeval_wittPolynomial, MvPolynomial.aeval_X, MvPolynomial.aeval_bind₁, _private.0.WittVector.ghostFun
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : R →+* S
hf : Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ Injective.{u_1 + 1, u_2 + 1} (α := 𝕎 R) (β := 𝕎 S) (⇑(map f) : (a : 𝕎 R) → 𝕎 S)

Tactic:
mapFun.injective f hf

Premises used: WittVector.mk, DFunLike.coe, WittVector.mapFun.injective, WittVector.mapFun
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : R →+* S
hf : Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ Surjective.{u_1 + 1, u_2 + 1} (α := 𝕎 R) (β := 𝕎 S) (⇑(map f) : (a : 𝕎 R) → 𝕎 S)

Tactic:
mapFun.surjective f hf

Premises used: WittVector.mapFun.surjective, WittVector.mk, DFunLike.coe, WittVector.mapFun
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : R →+* S
x : 𝕎 R
n : ℕ
⊢ Eq.{u_2 + 1} (α := S) (coeff (p := p) (((map f : RingHom.{u_1, u_2} (𝕎 R) (𝕎 S)) : (a : 𝕎 R) → 𝕎 S) x) n : S)
    ((f : (a : R) → S) (x.coeff n) : S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
a :
  ∀ (x : 𝕎 R) (n : ℕ),
    Eq.{u_1 + 1} (α := R) (coeff (p := p) ((map (RingHom.id R) : (a : 𝕎 R) → 𝕎 R) x) n)
      (coeff (p := p) ((RingHom.id (𝕎 R) : (a : 𝕎 R) → 𝕎 R) x) n)
⊢ Eq (α := 𝕎 R →+* 𝕎 R) (map (RingHom.id R)) (RingHom.id (𝕎 R))

Tactic:
ext
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (coeff (p := p) ((map (RingHom.id R) : (a : 𝕎 R) → 𝕎 R) x) n)
    (coeff (p := p) ((RingHom.id (𝕎 R) : (a : 𝕎 R) → 𝕎 R) x) n)

Tactic:
simp
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : R →+* S
x : 𝕎 R
⊢ Eq.{u_2 + 1} (α := 𝕎 S) (((map f : RingHom.{u_1, u_2} (𝕎 R) (𝕎 S)) : (a : 𝕎 R) → 𝕎 S) x : 𝕎 S) (0 : 𝕎 S) ↔
    ∀ (n : ℕ), Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (x.coeff n) : S) (0 : S)

Tactic:
⟨fun h n ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : R →+* S
x : 𝕎 R
refine_1 :
  ∀ (h : Eq.{u_2 + 1} (α := 𝕎 S) (((map f : RingHom.{u_1, u_2} (𝕎 R) (𝕎 S)) : (a : 𝕎 R) → 𝕎 S) x : 𝕎 S) (0 : 𝕎 S))
    (n : ℕ), Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (x.coeff n) : S) (0 : S)
refine_2 :
  ∀ (h : ∀ (n : ℕ), Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (x.coeff n) : S) (0 : S)),
    Eq.{u_2 + 1} (α := 𝕎 S) (((map f : RingHom.{u_1, u_2} (𝕎 R) (𝕎 S)) : (a : 𝕎 R) → 𝕎 S) x : 𝕎 S) (0 : 𝕎 S)
⊢ Eq.{u_2 + 1} (α := 𝕎 S) (((map f : RingHom.{u_1, u_2} (𝕎 R) (𝕎 S)) : (a : 𝕎 R) → 𝕎 S) x : 𝕎 S) (0 : 𝕎 S) ↔
    ∀ (n : ℕ), Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (x.coeff n) : S) (0 : S)

Tactic:
refine ⟨fun h n ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : R →+* S
x : 𝕎 R
h : Eq.{u_2 + 1} (α := 𝕎 S) (((map f : RingHom.{u_1, u_2} (𝕎 R) (𝕎 S)) : (a : 𝕎 R) → 𝕎 S) x : 𝕎 S) (0 : 𝕎 S)
n : ℕ
⊢ Eq.{u_2 + 1} (α := S) (coeff (p := p) (((map f : RingHom.{u_1, u_2} (𝕎 R) (𝕎 S)) : (a : 𝕎 R) → 𝕎 S) x) n)
    (coeff (p := p) 0 n)

Tactic:
apply_fun (·.coeff n) at h
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : R →+* S
x : 𝕎 R
n : ℕ
h :
  Eq.{u_2 + 1} (α := S) (coeff (p := p) (((map f : RingHom.{u_1, u_2} (𝕎 R) (𝕎 S)) : (a : 𝕎 R) → 𝕎 S) x) n)
    (coeff (p := p) 0 n)
⊢ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (x.coeff n) : S) (0 : S)

Tactic:
simpa using h
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : R →+* S
x : 𝕎 R
h : ∀ (n : ℕ), Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (x.coeff n) : S) (0 : S)
refine_2 :
  ∀ (n : ℕ),
    Eq.{u_2 + 1} (α := S) (coeff (p := p) (((map f : RingHom.{u_1, u_2} (𝕎 R) (𝕎 S)) : (a : 𝕎 R) → 𝕎 S) x) n)
      (coeff (p := p) 0 n)
⊢ Eq.{u_2 + 1} (α := 𝕎 S) (((map f : RingHom.{u_1, u_2} (𝕎 R) (𝕎 S)) : (a : 𝕎 R) → 𝕎 S) x : 𝕎 S) (0 : 𝕎 S)

Tactic:
ext n
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : R →+* S
x : 𝕎 R
h : ∀ (n : ℕ), Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (x.coeff n) : S) (0 : S)
n : ℕ
⊢ Eq.{u_2 + 1} (α := S) (coeff (p := p) (((map f : RingHom.{u_1, u_2} (𝕎 R) (𝕎 S)) : (a : 𝕎 R) → 𝕎 S) x) n)
    (coeff (p := p) 0 n)

Tactic:
simpa using h n
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
n : ℕ
x : 𝕎 R
⊢ Eq (α := R) ((ghostComponent n : (a : 𝕎 R) → R) x : R)
    (((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (W_ ℤ n) : R)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂, _private.0.WittVector.ghostFun, Finset.sum, rfl
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
hx : ∀ i ≤ n, (↑p : R) ∣ x.coeff i
rw :
  HPow.hPow (α := R) (↑p : R) (n + 1) ∣
    ∑ i ∈ Finset.range (n + 1),
      ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
        ((monomial (Finsupp.single i (p ^ (n - i))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) i) :
          MvPolynomial ℕ ℤ)
⊢ HPow.hPow (α := R) (↑p : R) (n + 1) ∣ (ghostComponent n : (a : 𝕎 R) → R) x

Tactic:
rw [WittVector.ghostComponent_apply, wittPolynomial, MvPolynomial.aeval_sum]

Premises used: MvPolynomial.aeval_sum, wittPolynomial, WittVector.ghostComponent_apply
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
hx : ∀ i ≤ n, (↑p : R) ∣ x.coeff i
h :
  ∀ i ∈ Finset.range (n + 1),
    HPow.hPow (α := R) (↑p : R) (n + 1) ∣
      ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
        ((monomial (Finsupp.single i (p ^ (n - i))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) i) :
          MvPolynomial ℕ ℤ)
⊢ HPow.hPow (α := R) (↑p : R) (n + 1) ∣
    ∑ i ∈ Finset.range (n + 1),
      ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
        ((monomial (Finsupp.single i (p ^ (n - i))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) i) :
          MvPolynomial ℕ ℤ)

Tactic:
apply Finset.dvd_sum

Premises used: Finset.dvd_sum
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
hx : ∀ i ≤ n, (↑p : R) ∣ x.coeff i
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ i < n + 1

Tactic:
simp only [Finset.mem_range] at hi

Premises used: Finset.mem_range
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
hx : ∀ i ≤ n, (↑p : R) ∣ x.coeff i
i : ℕ
hi : i < n + 1
⊢ ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
      ((monomial (Finsupp.single i (p ^ (n - i))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) i) :
        MvPolynomial ℕ ℤ) =
    HPow.hPow (α := R) (↑p : R) i * x.coeff i ^ p ^ (n - i)

Tactic:
simp [MvPolynomial.aeval_monomial, map_pow]

Premises used: map_pow, MvPolynomial.aeval_monomial