awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Complete (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
x : 𝕎 k
h : x.coeff 0 = 0
rw :
  Eq (α := 𝕎 k) ((verschiebung : (a : 𝕎 k) → 𝕎 k) (x.shift 1) : 𝕎 k)
    ((verschiebung : (a : 𝕎 k) → 𝕎 k)
        ((frobenius : (a : 𝕎 k) → 𝕎 k) ((RingEquiv.symm (frobeniusEquiv p k) : (a : 𝕎 k) → 𝕎 k) (x.shift 1) : 𝕎 k) :
          𝕎 k) :
      𝕎 k)
⊢ (verschiebung : (a : 𝕎 k) → 𝕎 k) (x.shift 1) =
    HMul.hMul (α := 𝕎 k) (β := 𝕎 k) ((RingEquiv.symm (frobeniusEquiv p k) : (a : 𝕎 k) → 𝕎 k) (x.shift 1) : 𝕎 k)
      ((↑p : 𝕎 k) : 𝕎 k)
have rw₁ : Eq (α := 𝕎 k) ((verschiebung : (a : 𝕎 k) → 𝕎 k) (x.shift 1) : 𝕎 k)
  ((verschiebung : (a : 𝕎 k) → 𝕎 k)
      ((frobeniusEquiv p k : (a : 𝕎 k) → 𝕎 k)
          ((RingEquiv.symm (frobeniusEquiv p k) : (a : 𝕎 k) → 𝕎 k) (x.shift 1) : 𝕎 k) :
        𝕎 k) :
    𝕎 k)
Tactic: rw [← verschiebung_frobenius, ← frobeniusEquiv_apply,
          RingEquiv.apply_symm_apply (frobeniusEquiv p k) _]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Complete (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
x : 𝕎 k
h : x.coeff 0 = 0
rw :
  Eq (α := 𝕎 k) ((verschiebung : (a : 𝕎 k) → 𝕎 k) (x.shift 1) : 𝕎 k)
    ((verschiebung : (a : 𝕎 k) → 𝕎 k)
        ((frobenius : (a : 𝕎 k) → 𝕎 k) ((RingEquiv.symm (frobeniusEquiv p k) : (a : 𝕎 k) → 𝕎 k) (x.shift 1) : 𝕎 k) :
          𝕎 k) :
      𝕎 k)
rw₁ :
  Eq (α := 𝕎 k) ((verschiebung : (a : 𝕎 k) → 𝕎 k) (x.shift 1) : 𝕎 k)
    ((verschiebung : (a : 𝕎 k) → 𝕎 k)
        ((frobeniusEquiv p k : (a : 𝕎 k) → 𝕎 k)
            ((RingEquiv.symm (frobeniusEquiv p k) : (a : 𝕎 k) → 𝕎 k) (x.shift 1) : 𝕎 k) :
          𝕎 k) :
      𝕎 k)
⊢ (verschiebung : (a : 𝕎 k) → 𝕎 k) (x.shift 1) =
    HMul.hMul (α := 𝕎 k) (β := 𝕎 k) ((RingEquiv.symm (frobeniusEquiv p k) : (a : 𝕎 k) → 𝕎 k) (x.shift 1) : 𝕎 k)
      ((↑p : 𝕎 k) : 𝕎 k)
have rw₂ : Eq (α := 𝕎 k) ((verschiebung : (a : 𝕎 k) → 𝕎 k) (x.shift 1) : 𝕎 k) ((verschiebung : (a : 𝕎 k) → 𝕎 k) (x.shift 1) : 𝕎 k)
Tactic: rw [← verschiebung_frobenius, ← frobeniusEquiv_apply,
          RingEquiv.apply_symm_apply (frobeniusEquiv p k) _]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Complete (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
x : 𝕎 k
h : x.coeff 0 = 0
⊢ x =
    HMul.hMul (α := 𝕎 k) (β := 𝕎 k) ((RingEquiv.symm (frobeniusEquiv p k) : (a : 𝕎 k) → 𝕎 k) (x.shift 1) : 𝕎 k)
      ((↑p : 𝕎 k) : 𝕎 k)
have _ : x = (verschiebung : (a : 𝕎 k) → 𝕎 k) (x.shift 1)
Tactic: calc
    _ = verschiebung (x.shift 1) := by
      simpa using eq_iterate_verschiebung (n := 1) (by simp [h])
    _ = _ := by
      rw [← verschiebung_frobenius, ← frobeniusEquiv_apply,
          RingEquiv.apply_symm_apply (frobeniusEquiv p k) _]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Complete (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
x : 𝕎 k
h : x.coeff 0 = 0
_ : x = (verschiebung : (a : 𝕎 k) → 𝕎 k) (x.shift 1)
⊢ x =
    HMul.hMul (α := 𝕎 k) (β := 𝕎 k) ((RingEquiv.symm (frobeniusEquiv p k) : (a : 𝕎 k) → 𝕎 k) (x.shift 1) : 𝕎 k)
      ((↑p : 𝕎 k) : 𝕎 k)
have _₁ : (verschiebung : (a : 𝕎 k) → 𝕎 k) (x.shift 1) =
  HMul.hMul (α := 𝕎 k) (β := 𝕎 k) ((RingEquiv.symm (frobeniusEquiv p k) : (a : 𝕎 k) → 𝕎 k) (x.shift 1) : 𝕎 k)
    ((↑p : 𝕎 k) : 𝕎 k)
Tactic: calc
    _ = verschiebung (x.shift 1) := by
      simpa using eq_iterate_verschiebung (n := 1) (by simp [h])
    _ = _ := by
      rw [← verschiebung_frobenius, ← frobeniusEquiv_apply,
          RingEquiv.apply_symm_apply (frobeniusEquiv p k) _]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Complete (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
x : 𝕎 k
n : ℕ
⊢ Membership.mem (γ := Ideal (𝕎 k)) (Ideal.span {HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n}) x ↔ ∀ m < n, x.coeff m = 0
have simp_rw : (∃ (c : 𝕎 k), x = c * HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n) ↔ ∀ m < n, x.coeff m = 0
Tactic: simp_rw [Ideal.mem_span_singleton, dvd_def, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Complete (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
x : 𝕎 k
n : ℕ
⊢ (∃ (c : 𝕎 k), x = c * HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n) ↔ ∀ m < n, x.coeff m = 0
have refine_1 : (∃ (c : 𝕎 k), x = c * HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n) →
  ∀ (m : ℕ) (hm : m < n) (u : 𝕎 k) (hu : x = u * HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n), x.coeff m = 0
Tactic: refine ⟨fun ⟨u, hu⟩ m hm ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Complete (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
x : 𝕎 k
n : ℕ
refine_1 :
  (∃ (c : 𝕎 k), x = c * HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n) →
    ∀ (m : ℕ) (hm : m < n) (u : 𝕎 k) (hu : x = u * HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n), x.coeff m = 0
⊢ (∃ (c : 𝕎 k), x = c * HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n) ↔ ∀ m < n, x.coeff m = 0
have refine_2 : ∀ (h : ∀ m < n, x.coeff m = 0), ∃ (c : 𝕎 k), x = c * HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n
Tactic: refine ⟨fun ⟨u, hu⟩ m hm ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Complete (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
x : 𝕎 k
n : ℕ
h : ∃ (c : 𝕎 k), x = c * HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n
m : ℕ
hm : m < n
u : 𝕎 k
hu : x = u * HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n
⊢ x.coeff m = 0
have refine_1 : (u * HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n).coeff m = 0
Tactic: rw [hu, mul_pow_charP_coeff_zero _ hm]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Complete (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
x : 𝕎 k
n : ℕ
h : ∃ (c : 𝕎 k), x = c * HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n
m : ℕ
hm : m < n
u : 𝕎 k
hu : x = u * HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n
refine_1 : (u * HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n).coeff m = 0
⊢ x.coeff m = 0
have refine_1₁ : Eq.{u_1 + 1} (α := k) 0 0
Tactic: rw [hu, mul_pow_charP_coeff_zero _ hm]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Complete (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
x : 𝕎 k
n : ℕ
h : ∀ m < n, x.coeff m = 0
⊢ ∃ (c : 𝕎 k), x = c * HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n
have h₁ : x = (⇑(RingEquiv.symm (frobeniusEquiv p k)) : (a : 𝕎 k) → 𝕎 k)^[n] (x.shift n) * HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n
Tactic: use (frobeniusEquiv p k).symm^[n] (x.shift n)
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Complete (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
x : 𝕎 k
n : ℕ
h : ∀ m < n, x.coeff m = 0
⊢ x = (⇑(RingEquiv.symm (frobeniusEquiv p k)) : (a : 𝕎 k) → 𝕎 k)^[n] (x.shift n) * HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n
have h₁ : x =
  (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n]
    ((⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[n] ((⇑(RingEquiv.symm (frobeniusEquiv p k)) : (a : 𝕎 k) → 𝕎 k)^[n] (x.shift n)))
Tactic: rw [← iterate_verschiebung_iterate_frobenius]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Complete (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
x : 𝕎 k
n : ℕ
h : ∀ m < n, x.coeff m = 0
⊢ (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] (x.shift n) =
    (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n]
      ((⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[n] ((⇑(RingEquiv.symm (frobeniusEquiv p k)) : (a : 𝕎 k) → 𝕎 k)^[n] (x.shift n)))
have e_a : x.shift n =
  (⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[n] ((⇑(RingEquiv.symm (frobeniusEquiv p k)) : (a : 𝕎 k) → 𝕎 k)^[n] (x.shift n))
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Complete (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
x : 𝕎 k
n : ℕ
h : ∀ m < n, x.coeff m = 0
⊢ x.shift n =
    (⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[n] ((⇑(RingEquiv.symm (frobeniusEquiv p k)) : (a : 𝕎 k) → 𝕎 k)^[n] (x.shift n))
have e_a : x.shift n =
  (Function.comp (β := 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k)
        (⇑(RingEquiv.symm (frobeniusEquiv p k)) : (a : 𝕎 k) → 𝕎 k))^[n]
    (x.shift n)
Tactic: rw [← Function.comp_apply (f := frobenius^[n]), ← Function.Commute.comp_iterate]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Complete (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
x : 𝕎 k
n : ℕ
h : ∀ m < n, x.coeff m = 0
e_a :
  x.shift n =
    (Function.comp (β := 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k)
          (⇑(RingEquiv.symm (frobeniusEquiv p k)) : (a : 𝕎 k) → 𝕎 k))^[n]
      (x.shift n)
⊢ x.shift n =
    (⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[n] ((⇑(RingEquiv.symm (frobeniusEquiv p k)) : (a : 𝕎 k) → 𝕎 k)^[n] (x.shift n))
have e_a₁ : Function.Commute (α := 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k) (⇑(RingEquiv.symm (frobeniusEquiv p k)) : (a : 𝕎 k) → 𝕎 k)
Tactic: rw [← Function.comp_apply (f := frobenius^[n]), ← Function.Commute.comp_iterate]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Complete (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
x : 𝕎 k
n : ℕ
h : ∀ m < n, x.coeff m = 0
⊢ x.shift n =
    (Function.comp (β := 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k)
          (⇑(RingEquiv.symm (frobeniusEquiv p k)) : (a : 𝕎 k) → 𝕎 k))^[n]
      (x.shift n)
have e_a : x.shift n =
  (⇑(RingEquiv.trans (RingEquiv.symm (frobeniusEquiv p k)) (frobeniusEquiv p k)) : (a : 𝕎 k) → 𝕎 k)^[n] (x.shift n)
Tactic: rw [← WittVector.frobeniusEquiv_apply, ← RingEquiv.coe_trans]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Complete (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
x : 𝕎 k
n : ℕ
h : ∀ m < n, x.coeff m = 0
⊢ x =
    (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n]
      ((⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[n] ((⇑(RingEquiv.symm (frobeniusEquiv p k)) : (a : 𝕎 k) → 𝕎 k)^[n] (x.shift n)))
have _ : x = (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] (x.shift n)
Tactic: calc
    _ = verschiebung^[n] (x.shift n) := by
      simpa using eq_iterate_verschiebung (x := x) (n := n) h
    _ = _ := by
      congr
      rw [← Function.comp_apply (f := frobenius^[n]), ← Function.Commute.comp_iterate]
      · rw [← WittVector.frobeniusEquiv_apply, ← RingEquiv.coe_trans]
        simp
      · rw [Function.Commute, Function.Semiconj, ← WittVector.frobeniusEquiv_apply]
        simp only [RingEquiv.apply_symm_apply, RingEquiv.symm_apply_apply, implies_true]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Complete (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
x : 𝕎 k
n : ℕ
h : ∀ m < n, x.coeff m = 0
_ : x = (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] (x.shift n)
⊢ x =
    (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n]
      ((⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[n] ((⇑(RingEquiv.symm (frobeniusEquiv p k)) : (a : 𝕎 k) → 𝕎 k)^[n] (x.shift n)))
have _₁ : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] (x.shift n) =
  (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n]
    ((⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[n] ((⇑(RingEquiv.symm (frobeniusEquiv p k)) : (a : 𝕎 k) → 𝕎 k)^[n] (x.shift n)))
Tactic: calc
    _ = verschiebung^[n] (x.shift n) := by
      simpa using eq_iterate_verschiebung (x := x) (n := n) h
    _ = _ := by
      congr
      rw [← Function.comp_apply (f := frobenius^[n]), ← Function.Commute.comp_iterate]
      · rw [← WittVector.frobeniusEquiv_apply, ← RingEquiv.coe_trans]
        simp
      · rw [Function.Commute, Function.Semiconj, ← WittVector.frobeniusEquiv_apply]
        simp only [RingEquiv.apply_symm_apply, RingEquiv.symm_apply_apply, implies_true]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Complete (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
⊢ Eq (α := Ideal (𝕎 k)) (RingHom.ker (F := 𝕎 k →+* k) constantCoeff) (Ideal.span {(↑p : 𝕎 k)})
have h : ∀ (x : 𝕎 k),
  Membership.mem (γ := Ideal (𝕎 k)) (RingHom.ker (F := 𝕎 k →+* k) constantCoeff) x ↔
    Membership.mem (γ := Ideal (𝕎 k)) (Ideal.span {(↑p : 𝕎 k)}) x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Complete (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
x : 𝕎 k
h :
  ∀ (n : ℕ),
    SModEq (R := 𝕎 k)
      (HSMul.hSMul (β := Submodule (𝕎 k) (𝕎 k)) (HPow.hPow (α := Ideal (𝕎 k)) (Ideal.span {(↑p : 𝕎 k)}) n) ⊤) x 0
⊢ x = 0
have h₁ : ∀ (n : ℕ), x.coeff n = coeff (p := p) 0 n
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Complete (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
x : 𝕎 k
h :
  ∀ (n : ℕ),
    SModEq (R := 𝕎 k)
      (HSMul.hSMul (β := Submodule (𝕎 k) (𝕎 k)) (HPow.hPow (α := Ideal (𝕎 k)) (Ideal.span {(↑p : 𝕎 k)}) n) ⊤) x 0
n : ℕ
⊢ x.coeff n = coeff (p := p) 0 n
have h₁ : ∀ (n : ℕ), SModEq (R := 𝕎 k) (HPow.hPow (α := Ideal (𝕎 k)) (Ideal.span {(↑p : 𝕎 k)}) n) x 0
Tactic: simp only [smul_eq_mul, Ideal.mul_top] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Complete (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
x : 𝕎 k
n : ℕ
h : ∀ (n : ℕ), SModEq (R := 𝕎 k) (HPow.hPow (α := Ideal (𝕎 k)) (Ideal.span {(↑p : 𝕎 k)}) n) x 0
⊢ x.coeff n = coeff (p := p) 0 n
have this : SModEq (R := 𝕎 k) (HPow.hPow (α := Ideal (𝕎 k)) (Ideal.span {(↑p : 𝕎 k)}) (n + 1)) x 0
Tactic: have := h (n + 1)
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Complete (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
x : 𝕎 k
n : ℕ
h : ∀ (n : ℕ), SModEq (R := 𝕎 k) (HPow.hPow (α := Ideal (𝕎 k)) (Ideal.span {(↑p : 𝕎 k)}) n) x 0
this : SModEq (R := 𝕎 k) (HPow.hPow (α := Ideal (𝕎 k)) (Ideal.span {(↑p : 𝕎 k)}) (n + 1)) x 0
⊢ x.coeff n = coeff (p := p) 0 n
have this₁ : ∀ m < n + 1, x.coeff m = 0
Tactic: simp only [Ideal.span_singleton_pow, SModEq.zero,
        mem_span_p_pow_iff_le_coeff_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Complete (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
x : ℕ → 𝕎 k
h :
  ∀ {m n : ℕ},
    m ≤ n →
      SModEq (R := 𝕎 k)
        (HSMul.hSMul (β := Submodule (𝕎 k) (𝕎 k)) (HPow.hPow (α := Ideal (𝕎 k)) (Ideal.span {(↑p : 𝕎 k)}) m) ⊤) (x m)
        (x n)
⊢ ∃ (L : 𝕎 k),
    ∀ (n : ℕ),
      SModEq (R := 𝕎 k)
        (HSMul.hSMul (β := Submodule (𝕎 k) (𝕎 k)) (HPow.hPow (α := Ideal (𝕎 k)) (Ideal.span {(↑p : 𝕎 k)}) n) ⊤) (x n) L
have h₁ : ∀ (n : ℕ),
  SModEq (R := 𝕎 k)
    (HSMul.hSMul (β := Submodule (𝕎 k) (𝕎 k)) (HPow.hPow (α := Ideal (𝕎 k)) (Ideal.span {(↑p : 𝕎 k)}) n) ⊤) (x n)
    (mk p fun (n : ℕ) ↦ (x (n + 1)).coeff n)
Tactic: use .mk p (fun n ↦ (x (n + 1)).coeff n)
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Complete (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
x : ℕ → 𝕎 k
h :
  ∀ {m n : ℕ},
    m ≤ n →
      SModEq (R := 𝕎 k)
        (HSMul.hSMul (β := Submodule (𝕎 k) (𝕎 k)) (HPow.hPow (α := Ideal (𝕎 k)) (Ideal.span {(↑p : 𝕎 k)}) m) ⊤) (x m)
        (x n)
n : ℕ
⊢ SModEq (R := 𝕎 k)
    (HSMul.hSMul (β := Submodule (𝕎 k) (𝕎 k)) (HPow.hPow (α := Ideal (𝕎 k)) (Ideal.span {(↑p : 𝕎 k)}) n) ⊤) (x n)
    (mk p fun (n : ℕ) ↦ (x (n + 1)).coeff n)
have h₁ : ∀ (h : ∀ {m n : ℕ}, m ≤ n → ∀ i < m, (x m).coeff i = (x n).coeff i),
  ∀ i < n, (x n).coeff i = coeff (mk p fun (n : ℕ) ↦ (x (n + 1)).coeff n) i
Tactic: simp only [Ideal.span_singleton_pow, smul_eq_mul, Ideal.mul_top, SModEq.sub_mem,
      mem_span_p_pow_iff_le_coeff_eq_zero, ← le_coeff_eq_iff_le_sub_coeff_eq_zero] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Defs (goal)
Goal:
p : ℕ
R : Type u_1
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = y.coeff n
⊢ x = y
have mk' : ∀ (coeff : ℕ → R) (h : ∀ (n : ℕ), WittVector.coeff (p := p) { coeff := coeff : 𝕎 R } n = y.coeff n),
  { coeff := coeff } = y
Tactic: cases x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Defs (goal)
Goal:
p : ℕ
R : Type u_1
y : 𝕎 R
coeff : ℕ → R
h : ∀ (n : ℕ), WittVector.coeff (p := p) { coeff := coeff : 𝕎 R } n = y.coeff n
⊢ { coeff := coeff } = y
have mk' : ∀ (coeff_1 : ℕ → R)
  (h :
    ∀ (n : ℕ), WittVector.coeff (p := p) { coeff := coeff : 𝕎 R } n = WittVector.coeff (p := p) { coeff := coeff_1 } n),
  Eq (α := 𝕎 R) { coeff := coeff } { coeff := coeff_1 }
Tactic: cases y
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Defs (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ wittZero p n = 0
have a : Eq (α := MvPolynomial (Fin 0 × ℕ) ℚ)
  ((map (Int.castRingHom ℚ) : (a : MvPolynomial (Fin 0 × ℕ) ℤ) → MvPolynomial (Fin 0 × ℕ) ℚ) (wittZero p n) :
    MvPolynomial (Fin 0 × ℕ) ℚ)
  ((map (Int.castRingHom ℚ) : (a : MvPolynomial (Fin 0 × ℕ) ℤ) → MvPolynomial (Fin 0 × ℕ) ℚ) 0 :
    MvPolynomial (Fin 0 × ℕ) ℚ)
Tactic: apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Defs (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ wittOne p 0 = 1
have a : Eq (α := MvPolynomial (Fin 0 × ℕ) ℚ)
  ((map (Int.castRingHom ℚ) : (a : MvPolynomial (Fin 0 × ℕ) ℤ) → MvPolynomial (Fin 0 × ℕ) ℚ) (wittOne p 0) :
    MvPolynomial (Fin 0 × ℕ) ℚ)
  ((map (Int.castRingHom ℚ) : (a : MvPolynomial (Fin 0 × ℕ) ℤ) → MvPolynomial (Fin 0 × ℕ) ℚ) 1 :
    MvPolynomial (Fin 0 × ℕ) ℚ)
Tactic: apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Defs (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : 0 < n
⊢ wittOne p n = 0
have a : Eq (α := MvPolynomial (Fin 0 × ℕ) ℚ)
  ((map (Int.castRingHom ℚ) : (a : MvPolynomial (Fin 0 × ℕ) ℤ) → MvPolynomial (Fin 0 × ℕ) ℚ) (wittOne p n) :
    MvPolynomial (Fin 0 × ℕ) ℚ)
  ((map (Int.castRingHom ℚ) : (a : MvPolynomial (Fin 0 × ℕ) ℤ) → MvPolynomial (Fin 0 × ℕ) ℚ) 0 :
    MvPolynomial (Fin 0 × ℕ) ℚ)
Tactic: apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Defs (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : 0 < n
⊢ Eq (α := MvPolynomial (Fin 0 × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (Fin 0 × ℕ) ℤ) → MvPolynomial (Fin 0 × ℕ) ℚ) (wittOne p n) :
      MvPolynomial (Fin 0 × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (Fin 0 × ℕ) ℤ) → MvPolynomial (Fin 0 × ℕ) ℚ) 0 :
      MvPolynomial (Fin 0 × ℕ) ℚ)
have a : Eq (α := MvPolynomial (Fin 0 × ℕ) ℚ)
  ((bind₁ fun (k : ℕ) ↦ 1 : (a : MvPolynomial ℕ ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (xInTermsOfW p ℚ n) :
    MvPolynomial (Fin 0 × ℕ) ℚ)
  (0 : MvPolynomial (Fin 0 × ℕ) ℚ)
Tactic: simp only [wittOne, wittStructureRat, map_zero, map_one, map_wittStructureInt]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Defs (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : 0 < n
⊢ Eq (α := MvPolynomial (Fin 0 × ℕ) ℚ)
    ((bind₁ fun (k : ℕ) ↦ 1 : (a : MvPolynomial ℕ ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (xInTermsOfW p ℚ n) :
      MvPolynomial (Fin 0 × ℕ) ℚ)
    (0 : MvPolynomial (Fin 0 × ℕ) ℚ)
have a : ∀ (n : ℕ)
  (IH :
    ∀ m < n,
      ∀ (hn : 0 < m),
        Eq (α := MvPolynomial (Fin 0 × ℕ) ℚ)
          ((bind₁ fun (k : ℕ) ↦ 1 : (a : MvPolynomial ℕ ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (xInTermsOfW p ℚ m) :
            MvPolynomial (Fin 0 × ℕ) ℚ)
          (0 : MvPolynomial (Fin 0 × ℕ) ℚ))
  (hn : 0 < n),
  Eq (α := MvPolynomial (Fin 0 × ℕ) ℚ)
    ((bind₁ fun (k : ℕ) ↦ 1 : (a : MvPolynomial ℕ ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (xInTermsOfW p ℚ n) :
      MvPolynomial (Fin 0 × ℕ) ℚ)
    (0 : MvPolynomial (Fin 0 × ℕ) ℚ)
Tactic: induction n using Nat.strong_induction_on with | h n IH => ?_
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Defs (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    ∀ (hn : 0 < m),
      Eq (α := MvPolynomial (Fin 0 × ℕ) ℚ)
        ((bind₁ fun (k : ℕ) ↦ 1 : (a : MvPolynomial ℕ ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (xInTermsOfW p ℚ m) :
          MvPolynomial (Fin 0 × ℕ) ℚ)
        (0 : MvPolynomial (Fin 0 × ℕ) ℚ)
hn : 0 < n
⊢ Eq (α := MvPolynomial (Fin 0 × ℕ) ℚ)
    ((bind₁ fun (k : ℕ) ↦ 1 : (a : MvPolynomial ℕ ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (xInTermsOfW p ℚ n) :
      MvPolynomial (Fin 0 × ℕ) ℚ)
    (0 : MvPolynomial (Fin 0 × ℕ) ℚ)
have a : Eq (α := MvPolynomial (Fin 0 × ℕ) ℚ)
  ((bind₁ fun (k : ℕ) ↦ 1 : (a : MvPolynomial ℕ ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ)
      (HMul.hMul (β := MvPolynomial ℕ ℚ)
        (HSub.hSub (α := MvPolynomial ℕ ℚ) (X n)
          (∑ i ∈ Finset.range n,
            HMul.hMul (α := MvPolynomial ℕ ℚ)
              ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
              (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ i) (p ^ (n - i)))))
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ)
            (HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n) :
          MvPolynomial ℕ ℚ)) :
    MvPolynomial (Fin 0 × ℕ) ℚ)
  (0 : MvPolynomial (Fin 0 × ℕ) ℚ)
Tactic: rw [xInTermsOfW_eq]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Defs (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    ∀ (hn : 0 < m),
      Eq (α := MvPolynomial (Fin 0 × ℕ) ℚ)
        ((bind₁ fun (k : ℕ) ↦ 1 : (a : MvPolynomial ℕ ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (xInTermsOfW p ℚ m) :
          MvPolynomial (Fin 0 × ℕ) ℚ)
        (0 : MvPolynomial (Fin 0 × ℕ) ℚ)
hn : 0 < n
⊢ Eq (α := MvPolynomial (Fin 0 × ℕ) ℚ)
    ((bind₁ fun (k : ℕ) ↦ 1 : (a : MvPolynomial ℕ ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ)
        (HMul.hMul (β := MvPolynomial ℕ ℚ)
          (HSub.hSub (α := MvPolynomial ℕ ℚ) (X n)
            (∑ i ∈ Finset.range n,
              HMul.hMul (α := MvPolynomial ℕ ℚ)
                ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
                (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ i) (p ^ (n - i)))))
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ)
              (HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n) :
            MvPolynomial ℕ ℚ)) :
      MvPolynomial (Fin 0 × ℕ) ℚ)
    (0 : MvPolynomial (Fin 0 × ℕ) ℚ)
have a : HSub.hSub (α := MvPolynomial (Fin 0 × ℕ) ℚ) 1
      (∑ x ∈ Finset.range n,
        HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ) ((C : (a : ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (↑p : ℚ)) x *
          HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ)
            ((bind₁ fun (k : ℕ) ↦ 1 : (a : MvPolynomial ℕ ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (xInTermsOfW p ℚ x) :
              MvPolynomial (Fin 0 × ℕ) ℚ)
            (p ^ (n - x))) *
    HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ)
      ((C : (a : ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _))
      n =
  0
Tactic: simp only [map_mul, map_sub, map_sum, map_pow, bind₁_X_right,
    bind₁_C_right]