awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x y : 𝕎 R
⊢ (x + y).ghostFun = x.ghostFun + y.ghostFun
have h : ∀ (n : ℕ), (x + y).ghostFun n = (x.ghostFun + y.ghostFun) n
Tactic: ghost_fun_tac X 0 + X 1, ![x.coeff, y.coeff]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
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
⊢ (x + y).ghostFun = x.ghostFun + y.ghostFun
have h₂ : ∀ (n : ℕ),
  peval
        ((bind₁ (wittStructureInt p (HAdd.hAdd (α := 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 × ℕ) ℤ)
          (HAdd.hAdd (α := MvPolynomial (Fin (Nat.succ 0).succ) ℤ) (X 0) (X 1)))
        ![x.coeff, y.coeff] →
    (x + y).ghostFun n = (x.ghostFun + y.ghostFun) n
Tactic: ghost_fun_tac X 0 + X 1, ![x.coeff, y.coeff]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
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 (HAdd.hAdd (α := 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 × ℕ) ℤ)
            (HAdd.hAdd (α := MvPolynomial (Fin (Nat.succ 0).succ) ℤ) (X 0) (X 1)))
          ![x.coeff, y.coeff] →
      (x + y).ghostFun n = (x.ghostFun + y.ghostFun) n
⊢ (x + y).ghostFun = x.ghostFun + y.ghostFun
have h₄ : ∀ (n : ℕ),
  peval
        ((bind₁ (wittStructureInt p (HAdd.hAdd (α := 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 × ℕ) ℤ)
          (HAdd.hAdd (α := MvPolynomial (Fin (Nat.succ 0).succ) ℤ) (X 0) (X 1)))
        ![x.coeff, y.coeff] →
    (eval (wittAdd p) ![x, y]).ghostFun n = Add.add (x.ghostFun n) (y.ghostFun n)
Tactic: ghost_fun_tac X 0 + X 1, ![x.coeff, y.coeff]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
i : ℕ
⊢ Eq.{u_1 + 1} (α := ℕ → R) (ghostFun (p := p) i.unaryCast) (↑i : ℕ → R)
have zero : Eq.{u_1 + 1} (α := ℕ → R) (ghostFun (p := p) (Nat.unaryCast 0)) (↑0 : ℕ → R)
Tactic: induction i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
i : ℕ
zero : Eq.{u_1 + 1} (α := ℕ → R) (ghostFun (p := p) (Nat.unaryCast 0)) (↑0 : ℕ → R)
⊢ Eq.{u_1 + 1} (α := ℕ → R) (ghostFun (p := p) i.unaryCast) (↑i : ℕ → R)
have succ : ∀ (n : ℕ),
  Eq.{u_1 + 1} (α := ℕ → R) (ghostFun (p := p) n.unaryCast) (↑n : ℕ → R) →
    Eq.{u_1 + 1} (α := ℕ → R) (ghostFun (p := p) (n + 1).unaryCast) (↑(n + 1) : ℕ → R)
Tactic: induction i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x y : 𝕎 R
⊢ (x - y).ghostFun = x.ghostFun - y.ghostFun
have h : ∀ (n : ℕ), (x - y).ghostFun n = (x.ghostFun - y.ghostFun) n
Tactic: ghost_fun_tac X 0 - X 1, ![x.coeff, y.coeff]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
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
⊢ (x - y).ghostFun = x.ghostFun - y.ghostFun
have 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
Tactic: ghost_fun_tac X 0 - X 1, ![x.coeff, y.coeff]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
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
⊢ (x - y).ghostFun = x.ghostFun - y.ghostFun
have 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)
Tactic: ghost_fun_tac X 0 - X 1, ![x.coeff, y.coeff]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x y : 𝕎 R
⊢ (x * y).ghostFun = x.ghostFun * y.ghostFun
have h : ∀ (n : ℕ), (x * y).ghostFun n = (x.ghostFun * y.ghostFun) n
Tactic: ghost_fun_tac X 0 * X 1, ![x.coeff, y.coeff]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
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
⊢ (x * y).ghostFun = x.ghostFun * y.ghostFun
have 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
Tactic: ghost_fun_tac X 0 * X 1, ![x.coeff, y.coeff]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
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
⊢ (x * y).ghostFun = x.ghostFun * y.ghostFun
have 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)
Tactic: ghost_fun_tac X 0 * X 1, ![x.coeff, y.coeff]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x : 𝕎 R
⊢ (-x).ghostFun = -x.ghostFun
have h : ∀ (n : ℕ), (-x).ghostFun n = (-x.ghostFun) n
Tactic: ghost_fun_tac -X 0, ![x.coeff]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
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
⊢ (-x).ghostFun = -x.ghostFun
have 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
Tactic: ghost_fun_tac -X 0, ![x.coeff]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
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
⊢ (-x).ghostFun = -x.ghostFun
have 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
Tactic: ghost_fun_tac -X 0, ![x.coeff]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
i : ℤ
⊢ Eq.{u_1 + 1} (α := ℕ → R) (ghostFun (p := p) i.castDef) (↑i : ℕ → R)
have ofNat : ∀ (a : ℕ), Eq.{u_1 + 1} (α := ℕ → R) (ghostFun (p := p) (Int.ofNat a).castDef) (↑(Int.ofNat a) : ℕ → R)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
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)
⊢ Eq.{u_1 + 1} (α := ℕ → R) (ghostFun (p := p) i.castDef) (↑i : ℕ → R)
have negSucc : ∀ (a : ℕ), Eq.{u_1 + 1} (α := ℕ → R) (ghostFun (p := p) (Int.negSucc a).castDef) (↑(Int.negSucc a) : ℕ → R)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
m : ℕ
x : 𝕎 R
⊢ (m • x).ghostFun = m • x.ghostFun
have h : ∀ (n : ℕ), (m • x).ghostFun n = (m • x.ghostFun) n
Tactic: ghost_fun_tac m • (X 0), ![x.coeff]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
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
⊢ (m • x).ghostFun = m • x.ghostFun
have 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
Tactic: ghost_fun_tac m • (X 0), ![x.coeff]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
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
⊢ (m • x).ghostFun = m • x.ghostFun
have 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
Tactic: ghost_fun_tac m • (X 0), ![x.coeff]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
m : ℤ
x : 𝕎 R
⊢ (m • x).ghostFun = m • x.ghostFun
have h : ∀ (n : ℕ), (m • x).ghostFun n = (m • x.ghostFun) n
Tactic: ghost_fun_tac m • (X 0), ![x.coeff]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
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
⊢ (m • x).ghostFun = m • x.ghostFun
have 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
Tactic: ghost_fun_tac m • (X 0), ![x.coeff]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
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
⊢ (m • x).ghostFun = m • x.ghostFun
have 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
Tactic: ghost_fun_tac m • (X 0), ![x.coeff]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x : 𝕎 R
m : ℕ
⊢ (x ^ m).ghostFun = x.ghostFun ^ m
have h : ∀ (n : ℕ), (x ^ m).ghostFun n = (x.ghostFun ^ m) n
Tactic: ghost_fun_tac X 0 ^ m, ![x.coeff]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
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
⊢ (x ^ m).ghostFun = x.ghostFun ^ m
have 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
Tactic: ghost_fun_tac X 0 ^ m, ![x.coeff]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
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
⊢ (x ^ m).ghostFun = x.ghostFun ^ m
have 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)
Tactic: ghost_fun_tac X 0 ^ m, ![x.coeff]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
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
⊢ (fun (x : ℕ → R) ↦ (mk p fun (n : ℕ) ↦ (aeval x : (a : MvPolynomial ℕ R) → R) (xInTermsOfW p R n) : 𝕎 R)) x.ghostFun =
    x
have 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
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (hypothesis)
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 : ℕ
⊢ 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
have this : 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
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (hypothesis)
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)
⊢ 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
have 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)
Tactic: apply_fun aeval x.coeff at this
Cleared hypotheses: this