awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.WittVector.Truncated
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_1 : (k : ℕ) → RingHom.{u_2, u_1} S (TruncatedWittVector p k R)
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f_1 k₂) = f_1 k₁
f : (k : ℕ) → RingHom.{u_2, u_1} S (TruncatedWittVector p k R)
hf : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
⊢ Eq (α :=
    { f : (k : ℕ) → RingHom.{u_2, u_1} S (TruncatedWittVector p k R) //
      ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁ })
    ((fun (g : RingHom.{u_2, u_1} S (𝕎 R)) ↦
        (Subtype.mk (p := fun (f : (k : ℕ) → RingHom.{u_2, u_1} S (TruncatedWittVector p k R)) ↦
            ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁)
            (fun (k : ℕ) ↦ RingHom.comp (truncate k) g) ⋯ :
          { f : (k : ℕ) → RingHom.{u_2, u_1} S (TruncatedWittVector p k R) //
            ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁ }))
      ((fun
            (f :
              { f : (k : ℕ) → RingHom.{u_2, u_1} S (TruncatedWittVector p k R) //
                ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁ }) ↦
          lift (↑f : (k : ℕ) → S →+* TruncatedWittVector p k R) ⋯)
        (Subtype.mk (p := fun (f : (k : ℕ) → RingHom.{u_2, u_1} S (TruncatedWittVector p k R)) ↦
          ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁) f hf)))
    (Subtype.mk (p := fun (f : (k : ℕ) → RingHom.{u_2, u_1} S (TruncatedWittVector p k R)) ↦
      ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁) f hf)

Tactic:
simp only [truncate_comp_lift]

Premises used: WittVector.truncate_comp_lift
-- Module: Mathlib.RingTheory.WittVector.Truncated
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
S : Type u_2
inst_2 : Semiring S
g₁ g₂ : RingHom.{u_2, u_1} S (𝕎 R)
h : ∀ (k : ℕ), RingHom.comp (truncate k) g₁ = RingHom.comp (truncate k) g₂
⊢ g₁ = g₂

Tactic:
liftEquiv.symm.injective <| Subtype.ext <| funext h

Premises used: funext, WittVector.liftEquiv, Equiv.injective, Equiv.symm, Subtype.ext
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
x : 𝕎 R
n : ℕ
⊢ x.verschiebungFun.coeff n = if n = 0 then 0 else x.coeff (n - 1)

Tactic:
simp only [verschiebungFun]

Premises used: WittVector.verschiebungFun
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
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
rw₁ rw₂ : Eq.{u_1 + 1} (α := R) 0 0
⊢ x.verschiebungFun.coeff 0 = 0

Tactic:
rw [verschiebungFun_coeff, if_pos rfl]

Premises used: WittVector.verschiebungFun_coeff, if_pos, rfl
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
x : 𝕎 R
n : ℕ
⊢ x.verschiebungFun.coeff n.succ = x.coeff n

Tactic:
rfl

Premises used: Nat.pred, rfl, ite
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
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
rw₈ rw₉ : Eq.{u_1 + 1} (α := R) 0 0
⊢ Eq (α := R) ((ghostComponent 0 : (a : 𝕎 R) → R) x.verschiebungFun : 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]

Premises used: WittVector.ghostComponent_apply, aeval_wittPolynomial, pow_zero, Finset.sum_singleton, pow_one, WittVector.verschiebungFun_coeff_zero, Finset.range_one, one_mul
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
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))
⊢ (ghostComponent (n + 1) : (a : 𝕎 R) → R) x.verschiebungFun =
    HMul.hMul (α := R) (β := R) ((↑p : R) : R) ((ghostComponent n : (a : 𝕎 R) → R) x : R)

Tactic:
simp only [ghostComponent_apply, aeval_wittPolynomial]

Premises used: WittVector.ghostComponent_apply, aeval_wittPolynomial
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
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))
⊢ ∑ 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:
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]

Premises used: Finset.mul_sum, pow_ne_zero, WittVector.verschiebungFun_coeff, if_pos, MulZeroClass.mul_zero, Nat.Prime.ne_zero, add_zero, Finset.sum_range_succ', Finset.sum_congr, zero_pow, rfl, Fact.out
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
n i : ℕ
⊢ HPow.hPow (α := R) (↑p : R) (i + 1) * x.verschiebungFun.coeff (i + 1) ^ p ^ (n + 1 - (i + 1)) =
    (↑p : R) * (HPow.hPow (α := R) (↑p : R) i * x.coeff i ^ p ^ (n - i))

Tactic:
simp only [pow_succ', verschiebungFun_coeff_succ, Nat.succ_sub_succ_eq_sub, mul_assoc]

Premises used: mul_assoc, WittVector.verschiebungFun_coeff_succ, Nat.succ_sub_succ_eq_sub, pow_succ'
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
Goal:
⊢ verschiebungPoly 0 = 0

Tactic:
rfl

Premises used: WittVector.verschiebungPoly, rfl, ite
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
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
succ :
  ∀ (n : ℕ),
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (verschiebungPoly (n + 1)) =
      x.verschiebungFun.coeff (n + 1)
⊢ ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (verschiebungPoly n) =
    x.verschiebungFun.coeff n

Tactic:
rcases n with - | n
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
x : 𝕎 R
⊢ ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (verschiebungPoly 0) =
    x.verschiebungFun.coeff 0

Tactic:
simp only [verschiebungPoly, ite_true, map_zero, verschiebungFun_coeff_zero]

Premises used: map_zero, WittVector.verschiebungPoly, ite_true, WittVector.verschiebungFun_coeff_zero
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
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
succ₄ succ₅ : x.coeff n = x.coeff n
⊢ ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (verschiebungPoly (n + 1)) =
    x.verschiebungFun.coeff (n + 1)

Tactic:
rw [verschiebungPoly, verschiebungFun_coeff_succ, if_neg n.succ_ne_zero, aeval_X,
      add_tsub_cancel_right]

Premises used: MvPolynomial.aeval_X, WittVector.verschiebungPoly, Nat.succ_ne_zero, WittVector.verschiebungFun_coeff_succ, add_tsub_cancel_right, if_neg
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
h :
  ∀ ⦃R : Type u_3⦄ [inst : CommRing R] (x : 𝕎 R),
    x.verschiebungFun.coeff = fun (n : ℕ) ↦ (aeval x.coeff : (a : MvPolynomial ℕ ℤ) → R) (verschiebungPoly n)
⊢ IsPoly.{u_3} p fun (R : Type u_3) (_Rcr : CommRing R) ↦ verschiebungFun

Tactic:
use verschiebungPoly

Premises used: WittVector.verschiebungPoly
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
⊢ ∀ ⦃R : Type u_3⦄ [inst : CommRing R] (x : 𝕎 R),
    x.verschiebungFun.coeff = fun (n : ℕ) ↦ (aeval x.coeff : (a : MvPolynomial ℕ ℤ) → R) (verschiebungPoly n)

Tactic:
simp only [aeval_verschiebung_poly', forall₃_true_iff]

Premises used: WittVector.aeval_verschiebung_poly', forall₃_true_iff
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
Goal:
p_1 : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
p : ℕ
f : ⦃R : Type u_3⦄ → [CommRing R] → 𝕎 R → 𝕎 R
inst_2 : IsPoly p f
⊢ IsPoly.{u_3} p fun (R : Type u_3) (I : CommRing R) ↦ verschiebungFun ∘ f

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
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)
h₁ : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (coeff (p := p) (verschiebungFun 0) (n + 1)) (coeff (p := p) 0 (n + 1))
⊢ Eq.{u_1 + 1} (α := 𝕎 R) (verschiebungFun 0) 0

Tactic:
ext ⟨⟩
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
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) (if Eq (α := ℕ) 0 0 then 0 else coeff (p := p) 0 (HSub.hSub (α := ℕ) 0 1)) (coeff (p := p) 0 0)
⊢ Eq.{u_1 + 1} (α := R) (coeff (p := p) (verschiebungFun 0) 0) (coeff (p := p) 0 0)

Tactic:
rw [verschiebungFun_coeff]

Premises used: WittVector.verschiebungFun_coeff
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
hp : Fact (Nat.Prime p)
n : ℕ
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))
⊢ Eq.{u_1 + 1} (α := R) (coeff (p := p) (verschiebungFun 0) (n + 1)) (coeff (p := p) 0 (n + 1))

Tactic:
rw [verschiebungFun_coeff]

Premises used: WittVector.verschiebungFun_coeff
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
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) (if Eq (α := ℕ) 0 0 then 0 else coeff (p := p) 0 (HSub.hSub (α := ℕ) 0 1)) (coeff (p := p) 0 0)

Tactic:
simp only [zero_coeff, ite_self]

Premises used: ite_self, WittVector.zero_coeff
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
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) (if n + 1 = 0 then 0 else coeff (p := p) 0 (n + 1 - 1)) (coeff (p := p) 0 (n + 1))

Tactic:
simp only [zero_coeff, ite_self]

Premises used: ite_self, WittVector.zero_coeff
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
Goal:
p : ℕ
S : Type u_2
inst : CommRing S
hp : Fact (Nat.Prime p)
R : Type u_1
R._inst : CommRing R
refine_3 :
  ∀ (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)
⊢ ∀ (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:
_
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
Goal:
p : ℕ
S : Type u_2
inst : CommRing S
hp : Fact (Nat.Prime p)
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
refine_3 :
  ∀ (y : 𝕎 R) (n : ℕ),
    Eq (α := R) ((ghostComponent n : (a : 𝕎 R) → R) (x + y).verschiebungFun : R)
      ((ghostComponent n : (a : 𝕎 R) → R) (x.verschiebungFun + y.verschiebungFun) : R)
⊢ ∀ (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:
_
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
hp : Fact (Nat.Prime p)
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)
⊢ ∀ (x y : 𝕎 R), (x + y).verschiebungFun = x.verschiebungFun + y.verschiebungFun

Tactic:
ghost_calc _ _
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
Goal:
p : ℕ
S : Type u_2
inst : CommRing S
hp : Fact (Nat.Prime p)
R : Type u_1
R._inst : CommRing R
x y : 𝕎 R
⊢ Eq (α := R) ((ghostComponent 0 : (a : 𝕎 R) → R) (x + y).verschiebungFun : R)
    ((ghostComponent 0 : (a : 𝕎 R) → R) (x.verschiebungFun + y.verschiebungFun) : R)

Tactic:
ghost_simp
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
Goal:
p : ℕ
S : Type u_2
inst : CommRing S
hp : Fact (Nat.Prime p)
R : Type u_1
R._inst : CommRing R
x y : 𝕎 R
n : ℕ
⊢ Eq (α := R) ((ghostComponent (n + 1) : (a : 𝕎 R) → R) (x + y).verschiebungFun : R)
    ((ghostComponent (n + 1) : (a : 𝕎 R) → R) (x.verschiebungFun + y.verschiebungFun) : R)

Tactic:
ghost_simp
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ IsPoly.{u_3} p fun (x : Type u_3) (x_1 : CommRing x) ↦ (⇑verschiebung : (a : 𝕎 x) → 𝕎 x)

Tactic:
verschiebungFun_isPoly p

Premises used: WittVector.verschiebungFun, WittVector.verschiebungFun_isPoly
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
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)
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))
⊢ 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)

Tactic:
ext ⟨-, -⟩
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
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.{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:
f.map_zero

Premises used: RingHom.map_zero, ite
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
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.{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:
exact f.map_zero

Premises used: RingHom.map_zero
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
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
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:
rfl
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
⊢ Eq (α := R) ((ghostComponent 0 : (a : 𝕎 R) → R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R) : R) (0 : R)

Tactic:
ghostComponent_zero_verschiebungFun _

Premises used: WittVector.verschiebungFun, WittVector.ghostComponent_zero_verschiebungFun
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
⊢ (ghostComponent (n + 1) : (a : 𝕎 R) → R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R) =
    HMul.hMul (α := R) (β := R) ((↑p : R) : R) ((ghostComponent n : (a : 𝕎 R) → R) x : R)

Tactic:
ghostComponent_verschiebungFun _ _

Premises used: WittVector.ghostComponent_verschiebungFun, WittVector.verschiebungFun
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
⊢ Eq.{u_1 + 1} (α := R) (coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x) 0) 0

Tactic:
rfl

Premises used: rfl, ite
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
⊢ coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x) (n + 1) = x.coeff n

Tactic:
rfl

Premises used: Nat.pred, rfl, ite
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
⊢ coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x) n.succ = x.coeff n

Tactic:
rfl

Premises used: Nat.pred, rfl, ite
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
rw : ∀ (a : 𝕎 R), Eq (α := 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) a : 𝕎 R) (0 : 𝕎 R) → a = 0
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := 𝕎 R) (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)

Tactic:
rw [injective_iff_map_eq_zero]

Premises used: injective_iff_map_eq_zero
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
w : 𝕎 R
h : Eq (α := 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) w : 𝕎 R) (0 : 𝕎 R)
h₁ : ∀ (n : ℕ), w.coeff n = coeff (p := p) 0 n
⊢ w = 0

Tactic:
ext n
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
w : 𝕎 R
h : Eq (α := 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) w : 𝕎 R) (0 : 𝕎 R)
n : ℕ
h₁ : Eq.{u_1 + 1} (α := R) (coeff (p := p) 0 n.succ) (coeff (p := p) 0 n)
⊢ w.coeff n = coeff (p := p) 0 n

Tactic:
rw [← verschiebung_coeff_succ, h]

Premises used: WittVector.verschiebung_coeff_succ
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
w : 𝕎 R
h : Eq (α := 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) w : 𝕎 R) (0 : 𝕎 R)
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (coeff (p := p) 0 n.succ) (coeff (p := p) 0 n)

Tactic:
simp only [zero_coeff]

Premises used: WittVector.zero_coeff
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
⊢ Eq (α := R)
    (((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (verschiebungPoly n) : R)
    (coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x) n : R)

Tactic:
aeval_verschiebung_poly' x n

Premises used: WittVector.aeval_verschiebung_poly'
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h :
  ∀ (x : ℕ → ℤ),
    Eq (α := ℤ)
      ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ)
          ((bind₁ verschiebungPoly : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n) :
            MvPolynomial ℕ ℤ) :
        ℤ)
      ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ)
          (if n = 0 then 0
          else HMul.hMul (α := MvPolynomial ℕ ℤ) (↑p : MvPolynomial ℕ ℤ) (wittPolynomial p ℤ (n - 1))) :
        ℤ)
⊢ (bind₁ verschiebungPoly : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n) =
    if n = 0 then 0 else HMul.hMul (α := MvPolynomial ℕ ℤ) (↑p : MvPolynomial ℕ ℤ) (wittPolynomial p ℤ (n - 1))

Tactic:
apply MvPolynomial.funext

Premises used: MvPolynomial.funext
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℕ → ℤ
pos :
  ∀ (hn : n = 0),
    Eq (α := ℤ)
      ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ)
          ((bind₁ verschiebungPoly : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n) :
            MvPolynomial ℕ ℤ) :
        ℤ)
      ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) 0 : ℤ)
neg :
  ∀ (hn : ¬n = 0),
    Eq (α := ℤ)
      ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ)
          ((bind₁ verschiebungPoly : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n) :
            MvPolynomial ℕ ℤ) :
        ℤ)
      ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ)
          (HMul.hMul (α := MvPolynomial ℕ ℤ) (↑p : MvPolynomial ℕ ℤ) (wittPolynomial p ℤ (n - 1))) :
        ℤ)
⊢ Eq (α := ℤ)
    ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ)
        ((bind₁ verschiebungPoly : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n) :
          MvPolynomial ℕ ℤ) :
      ℤ)
    ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ)
        (if n = 0 then 0 else HMul.hMul (α := MvPolynomial ℕ ℤ) (↑p : MvPolynomial ℕ ℤ) (wittPolynomial p ℤ (n - 1))) :
      ℤ)

Tactic:
split_ifs with hn
-- Module: Mathlib.RingTheory.WittVector.Verschiebung
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℕ → ℤ
hn : n = 0
⊢ Eq (α := ℤ)
    ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ)
        ((bind₁ verschiebungPoly : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n) :
          MvPolynomial ℕ ℤ) :
      ℤ)
    ((MvPolynomial.eval x : (a : MvPolynomial ℕ ℤ) → ℤ) 0 : ℤ)

Tactic:
simp only [hn, wittPolynomial_zero, bind₁_X_right, verschiebungPoly_zero, map_zero]

Premises used: map_zero, wittPolynomial_zero, MvPolynomial.bind₁_X_right, WittVector.verschiebungPoly_zero