awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
S : Type u_2
inst_2 : Semiring S
f : (k : ℕ) → RingHom.{u_2, u_1} S (TruncatedWittVector p k R)
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
x : S
⊢ Eq.{u_1 + 1} (α := TruncatedWittVector p n R)
    ((RingHom.comp (truncate n) (lift f f_compat) : (a : S) → TruncatedWittVector p n R) x : TruncatedWittVector p n R)
    ((f n : (a : S) → TruncatedWittVector p n R) x : TruncatedWittVector p n R)
have a : Eq.{u_1 + 1} (α := TruncatedWittVector p n R)
  ((truncate n : (a : 𝕎 R) → TruncatedWittVector p n R) ((lift f f_compat : (a : S) → 𝕎 R) x : 𝕎 R) :
    TruncatedWittVector p n R)
  ((f n : (a : S) → TruncatedWittVector p n R) x : TruncatedWittVector p n R)
Tactic: rw [RingHom.comp_apply, truncate_lift]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
S : Type u_2
inst_2 : Semiring S
f : (k : ℕ) → RingHom.{u_2, u_1} S (TruncatedWittVector p k R)
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
x : S
a :
  Eq.{u_1 + 1} (α := TruncatedWittVector p n R)
    ((truncate n : (a : 𝕎 R) → TruncatedWittVector p n R) ((lift f f_compat : (a : S) → 𝕎 R) x : 𝕎 R) :
      TruncatedWittVector p n R)
    ((f n : (a : S) → TruncatedWittVector p n R) x : TruncatedWittVector p n R)
⊢ Eq.{u_1 + 1} (α := TruncatedWittVector p n R)
    ((RingHom.comp (truncate n) (lift f f_compat) : (a : S) → TruncatedWittVector p n R) x : TruncatedWittVector p n R)
    ((f n : (a : S) → TruncatedWittVector p n R) x : TruncatedWittVector p n R)
have a₁ : Eq.{u_1 + 1} (α := TruncatedWittVector p n R)
  ((f n : (a : S) → TruncatedWittVector p n R) x : TruncatedWittVector p n R)
  ((f n : (a : S) → TruncatedWittVector p n R) x : TruncatedWittVector p n R)
Tactic: rw [RingHom.comp_apply, truncate_lift]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
S : Type u_2
inst_2 : Semiring S
f : (k : ℕ) → RingHom.{u_2, u_1} S (TruncatedWittVector p k R)
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
g : RingHom.{u_2, u_1} S (𝕎 R)
g_compat : ∀ (k : ℕ), RingHom.comp (truncate k) g = f k
⊢ lift f f_compat = g
have a : ∀ (x : S), Eq.{u_1 + 1} (α := 𝕎 R) ((lift f f_compat : (a : S) → 𝕎 R) x : 𝕎 R) ((g : (a : S) → 𝕎 R) x : 𝕎 R)
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
S : Type u_2
inst_2 : Semiring S
f : (k : ℕ) → RingHom.{u_2, u_1} S (TruncatedWittVector p k R)
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
g : RingHom.{u_2, u_1} S (𝕎 R)
g_compat : ∀ (k : ℕ), RingHom.comp (truncate k) g = f k
x : S
⊢ Eq.{u_1 + 1} (α := 𝕎 R) ((lift f f_compat : (a : S) → 𝕎 R) x : 𝕎 R) ((g : (a : S) → 𝕎 R) x : 𝕎 R)
have a : ∀ (i : ℕ),
  Membership.mem (γ := Ideal (𝕎 R)) (RingHom.ker (F := 𝕎 R →+* TruncatedWittVector p i R) (truncate i))
    (HSub.hSub (α := 𝕎 R) (β := 𝕎 R) ((lift f f_compat : (a : S) → 𝕎 R) x : 𝕎 R) ((g : (a : S) → 𝕎 R) x : 𝕎 R))
Tactic: rw [← sub_eq_zero, ← Ideal.mem_bot, ← iInf_ker_truncate, Ideal.mem_iInf]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
x : 𝕎 R
⊢ x.verschiebungFun.coeff 0 = 0
have rw : (if Eq (α := ℕ) 0 0 then 0 else x.coeff (HSub.hSub (α := ℕ) 0 1)) = 0
Tactic: rw [verschiebungFun_coeff, if_pos rfl]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
x : 𝕎 R
rw : (if Eq (α := ℕ) 0 0 then 0 else x.coeff (HSub.hSub (α := ℕ) 0 1)) = 0
⊢ x.verschiebungFun.coeff 0 = 0
have rw₁ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [verschiebungFun_coeff, if_pos rfl]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
⊢ Eq (α := R) ((ghostComponent 0 : (a : 𝕎 R) → R) x.verschiebungFun : R) (0 : R)
have rw : Eq (α := R)
  (((aeval (R := ℤ) x.verschiebungFun.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
      (wittPolynomial p ℤ 0) :
    R)
  (0 : R)
Tactic: rw [ghostComponent_apply, aeval_wittPolynomial, Finset.range_one, Finset.sum_singleton,
    verschiebungFun_coeff_zero, pow_zero, pow_zero, pow_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
rw :
  Eq (α := R)
    (((aeval (R := ℤ) x.verschiebungFun.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
        (wittPolynomial p ℤ 0) :
      R)
    (0 : R)
⊢ Eq (α := R) ((ghostComponent 0 : (a : 𝕎 R) → R) x.verschiebungFun : R) (0 : R)
have rw₁ : Eq.{u_1 + 1} (α := R)
  (∑ i ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1), HPow.hPow (α := R) (↑p : R) i * x.verschiebungFun.coeff i ^ p ^ (0 - i))
  0
Tactic: rw [ghostComponent_apply, aeval_wittPolynomial, Finset.range_one, Finset.sum_singleton,
    verschiebungFun_coeff_zero, pow_zero, pow_zero, pow_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
rw :
  Eq (α := R)
    (((aeval (R := ℤ) x.verschiebungFun.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
        (wittPolynomial p ℤ 0) :
      R)
    (0 : R)
rw₁ :
  Eq.{u_1 + 1} (α := R)
    (∑ i ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1),
      HPow.hPow (α := R) (↑p : R) i * x.verschiebungFun.coeff i ^ p ^ (0 - i))
    0
⊢ Eq (α := R) ((ghostComponent 0 : (a : 𝕎 R) → R) x.verschiebungFun : R) (0 : R)
have rw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ {0}, HPow.hPow (α := R) (↑p : R) i * x.verschiebungFun.coeff i ^ p ^ (0 - i)) 0
Tactic: rw [ghostComponent_apply, aeval_wittPolynomial, Finset.range_one, Finset.sum_singleton,
    verschiebungFun_coeff_zero, pow_zero, pow_zero, pow_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
rw :
  Eq (α := R)
    (((aeval (R := ℤ) x.verschiebungFun.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
        (wittPolynomial p ℤ 0) :
      R)
    (0 : R)
rw₁ :
  Eq.{u_1 + 1} (α := R)
    (∑ i ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1),
      HPow.hPow (α := R) (↑p : R) i * x.verschiebungFun.coeff i ^ p ^ (0 - i))
    0
rw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ {0}, HPow.hPow (α := R) (↑p : R) i * x.verschiebungFun.coeff i ^ p ^ (0 - i)) 0
⊢ Eq (α := R) ((ghostComponent 0 : (a : 𝕎 R) → R) x.verschiebungFun : R) (0 : R)
have rw₃ : HPow.hPow (α := R) (β := ℕ) (↑p : R) 0 * x.verschiebungFun.coeff 0 ^ p ^ HSub.hSub (α := ℕ) 0 0 = 0
Tactic: rw [ghostComponent_apply, aeval_wittPolynomial, Finset.range_one, Finset.sum_singleton,
    verschiebungFun_coeff_zero, pow_zero, pow_zero, pow_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
rw :
  Eq (α := R)
    (((aeval (R := ℤ) x.verschiebungFun.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
        (wittPolynomial p ℤ 0) :
      R)
    (0 : R)
rw₁ :
  Eq.{u_1 + 1} (α := R)
    (∑ i ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1),
      HPow.hPow (α := R) (↑p : R) i * x.verschiebungFun.coeff i ^ p ^ (0 - i))
    0
rw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ {0}, HPow.hPow (α := R) (↑p : R) i * x.verschiebungFun.coeff i ^ p ^ (0 - i)) 0
rw₃ : HPow.hPow (α := R) (β := ℕ) (↑p : R) 0 * x.verschiebungFun.coeff 0 ^ p ^ HSub.hSub (α := ℕ) 0 0 = 0
⊢ Eq (α := R) ((ghostComponent 0 : (a : 𝕎 R) → R) x.verschiebungFun : R) (0 : R)
have rw₄ : HPow.hPow (α := R) (β := ℕ) (↑p : R) 0 * HPow.hPow (α := R) 0 (p ^ HSub.hSub (α := ℕ) 0 0) = 0
Tactic: rw [ghostComponent_apply, aeval_wittPolynomial, Finset.range_one, Finset.sum_singleton,
    verschiebungFun_coeff_zero, pow_zero, pow_zero, pow_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
rw :
  Eq (α := R)
    (((aeval (R := ℤ) x.verschiebungFun.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
        (wittPolynomial p ℤ 0) :
      R)
    (0 : R)
rw₁ :
  Eq.{u_1 + 1} (α := R)
    (∑ i ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1),
      HPow.hPow (α := R) (↑p : R) i * x.verschiebungFun.coeff i ^ p ^ (0 - i))
    0
rw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ {0}, HPow.hPow (α := R) (↑p : R) i * x.verschiebungFun.coeff i ^ p ^ (0 - i)) 0
rw₃ : HPow.hPow (α := R) (β := ℕ) (↑p : R) 0 * x.verschiebungFun.coeff 0 ^ p ^ HSub.hSub (α := ℕ) 0 0 = 0
rw₄ : HPow.hPow (α := R) (β := ℕ) (↑p : R) 0 * HPow.hPow (α := R) 0 (p ^ HSub.hSub (α := ℕ) 0 0) = 0
⊢ Eq (α := R) ((ghostComponent 0 : (a : 𝕎 R) → R) x.verschiebungFun : R) (0 : R)
have rw₅ : 1 * HPow.hPow (α := R) 0 (p ^ HSub.hSub (α := ℕ) 0 0) = 0
Tactic: rw [ghostComponent_apply, aeval_wittPolynomial, Finset.range_one, Finset.sum_singleton,
    verschiebungFun_coeff_zero, pow_zero, pow_zero, pow_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
rw :
  Eq (α := R)
    (((aeval (R := ℤ) x.verschiebungFun.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
        (wittPolynomial p ℤ 0) :
      R)
    (0 : R)
rw₁ :
  Eq.{u_1 + 1} (α := R)
    (∑ i ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1),
      HPow.hPow (α := R) (↑p : R) i * x.verschiebungFun.coeff i ^ p ^ (0 - i))
    0
rw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ {0}, HPow.hPow (α := R) (↑p : R) i * x.verschiebungFun.coeff i ^ p ^ (0 - i)) 0
rw₃ : HPow.hPow (α := R) (β := ℕ) (↑p : R) 0 * x.verschiebungFun.coeff 0 ^ p ^ HSub.hSub (α := ℕ) 0 0 = 0
rw₄ : HPow.hPow (α := R) (β := ℕ) (↑p : R) 0 * HPow.hPow (α := R) 0 (p ^ HSub.hSub (α := ℕ) 0 0) = 0
rw₅ : 1 * HPow.hPow (α := R) 0 (p ^ HSub.hSub (α := ℕ) 0 0) = 0
⊢ Eq (α := R) ((ghostComponent 0 : (a : 𝕎 R) → R) x.verschiebungFun : R) (0 : R)
have rw₆ : 1 * HPow.hPow (α := R) (β := ℕ) 0 1 = 0
Tactic: rw [ghostComponent_apply, aeval_wittPolynomial, Finset.range_one, Finset.sum_singleton,
    verschiebungFun_coeff_zero, pow_zero, pow_zero, pow_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
rw :
  Eq (α := R)
    (((aeval (R := ℤ) x.verschiebungFun.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
        (wittPolynomial p ℤ 0) :
      R)
    (0 : R)
rw₁ :
  Eq.{u_1 + 1} (α := R)
    (∑ i ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1),
      HPow.hPow (α := R) (↑p : R) i * x.verschiebungFun.coeff i ^ p ^ (0 - i))
    0
rw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ {0}, HPow.hPow (α := R) (↑p : R) i * x.verschiebungFun.coeff i ^ p ^ (0 - i)) 0
rw₃ : HPow.hPow (α := R) (β := ℕ) (↑p : R) 0 * x.verschiebungFun.coeff 0 ^ p ^ HSub.hSub (α := ℕ) 0 0 = 0
rw₄ : HPow.hPow (α := R) (β := ℕ) (↑p : R) 0 * HPow.hPow (α := R) 0 (p ^ HSub.hSub (α := ℕ) 0 0) = 0
rw₅ : 1 * HPow.hPow (α := R) 0 (p ^ HSub.hSub (α := ℕ) 0 0) = 0
rw₆ : 1 * HPow.hPow (α := R) (β := ℕ) 0 1 = 0
⊢ Eq (α := R) ((ghostComponent 0 : (a : 𝕎 R) → R) x.verschiebungFun : R) (0 : R)
have rw₇ : HMul.hMul (α := R) 1 0 = 0
Tactic: rw [ghostComponent_apply, aeval_wittPolynomial, Finset.range_one, Finset.sum_singleton,
    verschiebungFun_coeff_zero, pow_zero, pow_zero, pow_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
rw :
  Eq (α := R)
    (((aeval (R := ℤ) x.verschiebungFun.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
        (wittPolynomial p ℤ 0) :
      R)
    (0 : R)
rw₁ :
  Eq.{u_1 + 1} (α := R)
    (∑ i ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1),
      HPow.hPow (α := R) (↑p : R) i * x.verschiebungFun.coeff i ^ p ^ (0 - i))
    0
rw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ {0}, HPow.hPow (α := R) (↑p : R) i * x.verschiebungFun.coeff i ^ p ^ (0 - i)) 0
rw₃ : HPow.hPow (α := R) (β := ℕ) (↑p : R) 0 * x.verschiebungFun.coeff 0 ^ p ^ HSub.hSub (α := ℕ) 0 0 = 0
rw₄ : HPow.hPow (α := R) (β := ℕ) (↑p : R) 0 * HPow.hPow (α := R) 0 (p ^ HSub.hSub (α := ℕ) 0 0) = 0
rw₅ : 1 * HPow.hPow (α := R) 0 (p ^ HSub.hSub (α := ℕ) 0 0) = 0
rw₆ : 1 * HPow.hPow (α := R) (β := ℕ) 0 1 = 0
rw₇ : HMul.hMul (α := R) 1 0 = 0
⊢ Eq (α := R) ((ghostComponent 0 : (a : 𝕎 R) → R) x.verschiebungFun : R) (0 : R)
have rw₈ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [ghostComponent_apply, aeval_wittPolynomial, Finset.range_one, Finset.sum_singleton,
    verschiebungFun_coeff_zero, pow_zero, pow_zero, pow_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
⊢ (ghostComponent (n + 1) : (a : 𝕎 R) → R) x.verschiebungFun =
    HMul.hMul (α := R) (β := R) ((↑p : R) : R) ((ghostComponent n : (a : 𝕎 R) → R) x : R)
have simp : ∑ i ∈ Finset.range (n + 1 + 1), HPow.hPow (α := R) (↑p : R) i * x.verschiebungFun.coeff i ^ p ^ (n + 1 - i) =
  HMul.hMul (α := R) (↑p : R) (∑ i ∈ Finset.range (n + 1), HPow.hPow (α := R) (↑p : R) i * x.coeff i ^ p ^ (n - i))
Tactic: simp only [ghostComponent_apply, aeval_wittPolynomial]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
⊢ ∑ i ∈ Finset.range (n + 1 + 1), HPow.hPow (α := R) (↑p : R) i * x.verschiebungFun.coeff i ^ p ^ (n + 1 - i) =
    HMul.hMul (α := R) (↑p : R) (∑ i ∈ Finset.range (n + 1), HPow.hPow (α := R) (↑p : R) i * x.coeff i ^ p ^ (n - i))
have rw : ∀ x_1 ∈ Finset.range (n + 1),
  HPow.hPow (α := R) (↑p : R) (x_1 + 1) * x.verschiebungFun.coeff (x_1 + 1) ^ p ^ (n + 1 - (x_1 + 1)) =
    (↑p : R) * (HPow.hPow (α := R) (↑p : R) x_1 * x.coeff x_1 ^ p ^ (n - x_1))
Tactic: rw [Finset.sum_range_succ', verschiebungFun_coeff, if_pos rfl,
    zero_pow (pow_ne_zero _ hp.1.ne_zero), mul_zero, add_zero, Finset.mul_sum, Finset.sum_congr rfl]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
x : 𝕎 R
n : ℕ
⊢ ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (verschiebungPoly n) =
    x.verschiebungFun.coeff n
have zero : ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (verschiebungPoly 0) =
  x.verschiebungFun.coeff 0
Tactic: rcases n with - | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
x : 𝕎 R
n : ℕ
zero :
  ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (verschiebungPoly 0) =
    x.verschiebungFun.coeff 0
⊢ ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (verschiebungPoly n) =
    x.verschiebungFun.coeff n
have succ : ∀ (n : ℕ),
  ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (verschiebungPoly (n + 1)) =
    x.verschiebungFun.coeff (n + 1)
Tactic: rcases n with - | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
x : 𝕎 R
n : ℕ
⊢ ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (verschiebungPoly (n + 1)) =
    x.verschiebungFun.coeff (n + 1)
have succ : ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
    (if n + 1 = 0 then 0 else X (n + 1 - 1)) =
  x.verschiebungFun.coeff (n + 1)
Tactic: rw [verschiebungPoly, verschiebungFun_coeff_succ, if_neg n.succ_ne_zero, aeval_X,
      add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
x : 𝕎 R
n : ℕ
succ :
  ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
      (if n + 1 = 0 then 0 else X (n + 1 - 1)) =
    x.verschiebungFun.coeff (n + 1)
⊢ ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (verschiebungPoly (n + 1)) =
    x.verschiebungFun.coeff (n + 1)
have succ₁ : ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
    (if n + 1 = 0 then 0 else X (n + 1 - 1)) =
  x.coeff n
Tactic: rw [verschiebungPoly, verschiebungFun_coeff_succ, if_neg n.succ_ne_zero, aeval_X,
      add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
x : 𝕎 R
n : ℕ
succ :
  ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
      (if n + 1 = 0 then 0 else X (n + 1 - 1)) =
    x.verschiebungFun.coeff (n + 1)
succ₁ :
  ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
      (if n + 1 = 0 then 0 else X (n + 1 - 1)) =
    x.coeff n
⊢ ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (verschiebungPoly (n + 1)) =
    x.verschiebungFun.coeff (n + 1)
have succ₂ : ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (X (n + 1 - 1)) = x.coeff n
Tactic: rw [verschiebungPoly, verschiebungFun_coeff_succ, if_neg n.succ_ne_zero, aeval_X,
      add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
x : 𝕎 R
n : ℕ
succ :
  ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
      (if n + 1 = 0 then 0 else X (n + 1 - 1)) =
    x.verschiebungFun.coeff (n + 1)
succ₁ :
  ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
      (if n + 1 = 0 then 0 else X (n + 1 - 1)) =
    x.coeff n
succ₂ : ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (X (n + 1 - 1)) = x.coeff n
⊢ ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (verschiebungPoly (n + 1)) =
    x.verschiebungFun.coeff (n + 1)
have succ₃ : x.coeff (n + 1 - 1) = x.coeff n
Tactic: rw [verschiebungPoly, verschiebungFun_coeff_succ, if_neg n.succ_ne_zero, aeval_X,
      add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
x : 𝕎 R
n : ℕ
succ :
  ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
      (if n + 1 = 0 then 0 else X (n + 1 - 1)) =
    x.verschiebungFun.coeff (n + 1)
succ₁ :
  ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
      (if n + 1 = 0 then 0 else X (n + 1 - 1)) =
    x.coeff n
succ₂ : ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (X (n + 1 - 1)) = x.coeff n
succ₃ : x.coeff (n + 1 - 1) = x.coeff n
⊢ ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (verschiebungPoly (n + 1)) =
    x.verschiebungFun.coeff (n + 1)
have succ₄ : x.coeff n = x.coeff n
Tactic: rw [verschiebungPoly, verschiebungFun_coeff_succ, if_neg n.succ_ne_zero, aeval_X,
      add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
⊢ IsPoly.{u_3} p fun (R : Type u_3) (_Rcr : CommRing R) ↦ verschiebungFun
have h : ∀ ⦃R : Type u_3⦄ [inst : CommRing R] (x : 𝕎 R),
  x.verschiebungFun.coeff = fun (n : ℕ) ↦ (aeval x.coeff : (a : MvPolynomial ℕ ℤ) → R) (verschiebungPoly n)
Tactic: use verschiebungPoly
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
hp : Fact (Nat.Prime p)
⊢ Eq.{u_1 + 1} (α := 𝕎 R) (verschiebungFun 0) 0
have h : Eq.{u_1 + 1} (α := R) (coeff (p := p) (verschiebungFun 0) 0) (coeff (p := p) 0 0)
Tactic: ext ⟨⟩
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
hp : Fact (Nat.Prime p)
h : Eq.{u_1 + 1} (α := R) (coeff (p := p) (verschiebungFun 0) 0) (coeff (p := p) 0 0)
⊢ Eq.{u_1 + 1} (α := 𝕎 R) (verschiebungFun 0) 0
have h₁ : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (coeff (p := p) (verschiebungFun 0) (n + 1)) (coeff (p := p) 0 (n + 1))
Tactic: ext ⟨⟩
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
hp : Fact (Nat.Prime p)
⊢ Eq.{u_1 + 1} (α := R) (coeff (p := p) (verschiebungFun 0) 0) (coeff (p := p) 0 0)
have h : Eq.{u_1 + 1} (α := R) (if Eq (α := ℕ) 0 0 then 0 else coeff (p := p) 0 (HSub.hSub (α := ℕ) 0 1)) (coeff (p := p) 0 0)
Tactic: rw [verschiebungFun_coeff]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
hp : Fact (Nat.Prime p)
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (coeff (p := p) (verschiebungFun 0) (n + 1)) (coeff (p := p) 0 (n + 1))
have h : Eq.{u_1 + 1} (α := R) (if n + 1 = 0 then 0 else coeff (p := p) 0 (n + 1 - 1)) (coeff (p := p) 0 (n + 1))
Tactic: rw [verschiebungFun_coeff]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
hp : Fact (Nat.Prime p)
⊢ ∀ (x y : 𝕎 R), (x + y).verschiebungFun = x.verschiebungFun + y.verschiebungFun
have refine_3 : ∀ (R : Type u_1) [R._inst : CommRing R] (x y : 𝕎 R) (n : ℕ),
  Eq (α := R) ((ghostComponent n : (a : 𝕎 R) → R) (x + y).verschiebungFun : R)
    ((ghostComponent n : (a : 𝕎 R) → R) (x.verschiebungFun + y.verschiebungFun) : R)
Tactic: ghost_calc _ _
Cleared hypotheses: R, inst
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
hp : Fact (Nat.Prime p)
f : R →+* S
x : 𝕎 R
⊢ Eq (α := 𝕎 S)
    (((map f : RingHom.{u_1, u_2} (𝕎 R) (𝕎 S)) : (a : 𝕎 R) → 𝕎 S) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x) : 𝕎 S)
    ((verschiebung : (a : 𝕎 S) → 𝕎 S) (((map f : RingHom.{u_1, u_2} (𝕎 R) (𝕎 S)) : (a : 𝕎 R) → 𝕎 S) x : 𝕎 S) : 𝕎 S)
have h : Eq.{u_2 + 1} (α := S)
  (coeff (p := p) (((map f : RingHom.{u_1, u_2} (𝕎 R) (𝕎 S)) : (a : 𝕎 R) → 𝕎 S) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x)) 0)
  (coeff (p := p)
    ((verschiebung : (a : 𝕎 S) → 𝕎 S) (((map f : RingHom.{u_1, u_2} (𝕎 R) (𝕎 S)) : (a : 𝕎 R) → 𝕎 S) x : 𝕎 S)) 0)
Tactic: ext ⟨-, -⟩
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
hp : Fact (Nat.Prime p)
f : R →+* S
x : 𝕎 R
h :
  Eq.{u_2 + 1} (α := S)
    (coeff (p := p) (((map f : RingHom.{u_1, u_2} (𝕎 R) (𝕎 S)) : (a : 𝕎 R) → 𝕎 S) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x))
      0)
    (coeff (p := p)
      ((verschiebung : (a : 𝕎 S) → 𝕎 S) (((map f : RingHom.{u_1, u_2} (𝕎 R) (𝕎 S)) : (a : 𝕎 R) → 𝕎 S) x : 𝕎 S)) 0)
⊢ Eq (α := 𝕎 S)
    (((map f : RingHom.{u_1, u_2} (𝕎 R) (𝕎 S)) : (a : 𝕎 R) → 𝕎 S) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x) : 𝕎 S)
    ((verschiebung : (a : 𝕎 S) → 𝕎 S) (((map f : RingHom.{u_1, u_2} (𝕎 R) (𝕎 S)) : (a : 𝕎 R) → 𝕎 S) x : 𝕎 S) : 𝕎 S)
have h₁ : ∀ (n : ℕ),
  Eq.{u_2 + 1} (α := S)
    (coeff (p := p) (((map f : RingHom.{u_1, u_2} (𝕎 R) (𝕎 S)) : (a : 𝕎 R) → 𝕎 S) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x))
      (n + 1))
    (coeff (p := p)
      ((verschiebung : (a : 𝕎 S) → 𝕎 S) (((map f : RingHom.{u_1, u_2} (𝕎 R) (𝕎 S)) : (a : 𝕎 R) → 𝕎 S) x : 𝕎 S)) (n + 1))
Tactic: ext ⟨-, -⟩
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Verschiebung (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := 𝕎 R) (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)
have rw : ∀ (a : 𝕎 R), Eq (α := 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) a : 𝕎 R) (0 : 𝕎 R) → a = 0
Tactic: rw [injective_iff_map_eq_zero]