awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Compare (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
rw :
  Eq (α := 𝕎 (ZMod p) →+* ZMod (p ^ m))
    (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p m)))
      (RingHom.comp (TruncatedWittVector.truncate h) (truncate n)))
    (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p m))) (truncate m))
⊢ Eq (α := 𝕎 (ZMod p) →+* ZMod (p ^ m))
    (RingHom.comp
      (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p m))) (TruncatedWittVector.truncate h))
      (truncate n))
    (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p m))) (truncate m))
have rw₁ : Eq (α := 𝕎 (ZMod p) →+* ZMod (p ^ m))
  (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p m))) (truncate m))
  (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p m))) (truncate m))
Tactic: rw [RingHom.comp_assoc, truncate_comp_wittVector_truncate]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Compare (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k₁ k₂ : ℕ
hk : k₁ ≤ k₂
⊢ Eq (α := ℤ_[p] →+* TruncatedWittVector p k₁ (ZMod p))
    (RingHom.comp (TruncatedWittVector.truncate hk)
      (RingHom.comp (RingEquiv.toRingHom (zmodEquivTrunc p k₂)) (PadicInt.toZModPow k₂)))
    (RingHom.comp (RingEquiv.toRingHom (zmodEquivTrunc p k₁)) (PadicInt.toZModPow k₁))
have rw : Eq (α := ℤ_[p] →+* TruncatedWittVector p k₁ (ZMod p))
  (RingHom.comp (RingHom.comp (TruncatedWittVector.truncate hk) (RingEquiv.toRingHom (zmodEquivTrunc p k₂)))
    (PadicInt.toZModPow k₂))
  (RingHom.comp (RingEquiv.toRingHom (zmodEquivTrunc p k₁)) (PadicInt.toZModPow k₁))
Tactic: rw [← RingHom.comp_assoc, commutes, RingHom.comp_assoc,
    PadicInt.zmod_cast_comp_toZModPow _ _ hk]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Compare (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k₁ k₂ : ℕ
hk : k₁ ≤ k₂
rw :
  Eq (α := ℤ_[p] →+* TruncatedWittVector p k₁ (ZMod p))
    (RingHom.comp (RingHom.comp (TruncatedWittVector.truncate hk) (RingEquiv.toRingHom (zmodEquivTrunc p k₂)))
      (PadicInt.toZModPow k₂))
    (RingHom.comp (RingEquiv.toRingHom (zmodEquivTrunc p k₁)) (PadicInt.toZModPow k₁))
⊢ Eq (α := ℤ_[p] →+* TruncatedWittVector p k₁ (ZMod p))
    (RingHom.comp (TruncatedWittVector.truncate hk)
      (RingHom.comp (RingEquiv.toRingHom (zmodEquivTrunc p k₂)) (PadicInt.toZModPow k₂)))
    (RingHom.comp (RingEquiv.toRingHom (zmodEquivTrunc p k₁)) (PadicInt.toZModPow k₁))
have rw₁ : Eq (α := ℤ_[p] →+* TruncatedWittVector p k₁ (ZMod p))
  (RingHom.comp
    (@RingHom.comp _ (ZMod (p ^ k₁)) _ _ Semiring.toNonAssocSemiring _ (RingEquiv.toRingHom (zmodEquivTrunc p k₁))
      (ZMod.castHom sorry (ZMod (p ^ k₁))))
    (PadicInt.toZModPow k₂))
  (RingHom.comp (RingEquiv.toRingHom (zmodEquivTrunc p k₁)) (PadicInt.toZModPow k₁))
Tactic: rw [← RingHom.comp_assoc, commutes, RingHom.comp_assoc,
    PadicInt.zmod_cast_comp_toZModPow _ _ hk]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Compare (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k₁ k₂ : ℕ
hk : k₁ ≤ k₂
rw :
  Eq (α := ℤ_[p] →+* TruncatedWittVector p k₁ (ZMod p))
    (RingHom.comp (RingHom.comp (TruncatedWittVector.truncate hk) (RingEquiv.toRingHom (zmodEquivTrunc p k₂)))
      (PadicInt.toZModPow k₂))
    (RingHom.comp (RingEquiv.toRingHom (zmodEquivTrunc p k₁)) (PadicInt.toZModPow k₁))
rw₁ :
  Eq (α := ℤ_[p] →+* TruncatedWittVector p k₁ (ZMod p))
    (RingHom.comp
      (@RingHom.comp _ (ZMod (p ^ k₁)) _ _ Semiring.toNonAssocSemiring _ (RingEquiv.toRingHom (zmodEquivTrunc p k₁))
        (ZMod.castHom ⋯ (ZMod (p ^ k₁))))
      (PadicInt.toZModPow k₂))
    (RingHom.comp (RingEquiv.toRingHom (zmodEquivTrunc p k₁)) (PadicInt.toZModPow k₁))
⊢ Eq (α := ℤ_[p] →+* TruncatedWittVector p k₁ (ZMod p))
    (RingHom.comp (TruncatedWittVector.truncate hk)
      (RingHom.comp (RingEquiv.toRingHom (zmodEquivTrunc p k₂)) (PadicInt.toZModPow k₂)))
    (RingHom.comp (RingEquiv.toRingHom (zmodEquivTrunc p k₁)) (PadicInt.toZModPow k₁))
have rw₂ : Eq (α := ℤ_[p] →+* TruncatedWittVector p k₁ (ZMod p))
  (@RingHom.comp _ (ZMod (p ^ k₁)) _ _ Semiring.toNonAssocSemiring _ (RingEquiv.toRingHom (zmodEquivTrunc p k₁))
    (RingHom.comp (ZMod.castHom sorry (ZMod (p ^ k₁))) (PadicInt.toZModPow k₂)))
  (RingHom.comp (RingEquiv.toRingHom (zmodEquivTrunc p k₁)) (PadicInt.toZModPow k₁))
Tactic: rw [← RingHom.comp_assoc, commutes, RingHom.comp_assoc,
    PadicInt.zmod_cast_comp_toZModPow _ _ hk]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Compare (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k₁ k₂ : ℕ
hk : k₁ ≤ k₂
rw :
  Eq (α := ℤ_[p] →+* TruncatedWittVector p k₁ (ZMod p))
    (RingHom.comp (RingHom.comp (TruncatedWittVector.truncate hk) (RingEquiv.toRingHom (zmodEquivTrunc p k₂)))
      (PadicInt.toZModPow k₂))
    (RingHom.comp (RingEquiv.toRingHom (zmodEquivTrunc p k₁)) (PadicInt.toZModPow k₁))
rw₁ :
  Eq (α := ℤ_[p] →+* TruncatedWittVector p k₁ (ZMod p))
    (RingHom.comp
      (@RingHom.comp _ (ZMod (p ^ k₁)) _ _ Semiring.toNonAssocSemiring _ (RingEquiv.toRingHom (zmodEquivTrunc p k₁))
        (ZMod.castHom ⋯ (ZMod (p ^ k₁))))
      (PadicInt.toZModPow k₂))
    (RingHom.comp (RingEquiv.toRingHom (zmodEquivTrunc p k₁)) (PadicInt.toZModPow k₁))
rw₂ :
  Eq (α := ℤ_[p] →+* TruncatedWittVector p k₁ (ZMod p))
    (@RingHom.comp _ (ZMod (p ^ k₁)) _ _ Semiring.toNonAssocSemiring _ (RingEquiv.toRingHom (zmodEquivTrunc p k₁))
      (RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k₁))) (PadicInt.toZModPow k₂)))
    (RingHom.comp (RingEquiv.toRingHom (zmodEquivTrunc p k₁)) (PadicInt.toZModPow k₁))
⊢ Eq (α := ℤ_[p] →+* TruncatedWittVector p k₁ (ZMod p))
    (RingHom.comp (TruncatedWittVector.truncate hk)
      (RingHom.comp (RingEquiv.toRingHom (zmodEquivTrunc p k₂)) (PadicInt.toZModPow k₂)))
    (RingHom.comp (RingEquiv.toRingHom (zmodEquivTrunc p k₁)) (PadicInt.toZModPow k₁))
have rw₃ : Eq (α := ℤ_[p] →+* TruncatedWittVector p k₁ (ZMod p))
  (RingHom.comp (RingEquiv.toRingHom (zmodEquivTrunc p k₁)) (PadicInt.toZModPow k₁))
  (RingHom.comp (RingEquiv.toRingHom (zmodEquivTrunc p k₁)) (PadicInt.toZModPow k₁))
Tactic: rw [← RingHom.comp_assoc, commutes, RingHom.comp_assoc,
    PadicInt.zmod_cast_comp_toZModPow _ _ hk]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Compare (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Eq (α := ℤ_[p] →+* ℤ_[p]) (RingHom.comp (toPadicInt p) (fromPadicInt p)) (RingHom.id ℤ_[p])
have rw : ∀ (n : ℕ),
  Eq (α := ℤ_[p] →+* ZMod (p ^ n)) (RingHom.comp (PadicInt.toZModPow n) (RingHom.comp (toPadicInt p) (fromPadicInt p)))
    (RingHom.comp (PadicInt.toZModPow n) (RingHom.id ℤ_[p]))
Tactic: rw [← PadicInt.toZModPow_eq_iff_ext]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Compare (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ Eq (α := ℤ_[p] →+* ZMod (p ^ n)) (RingHom.comp (PadicInt.toZModPow n) (RingHom.comp (toPadicInt p) (fromPadicInt p)))
    (RingHom.comp (PadicInt.toZModPow n) (RingHom.id ℤ_[p]))
have rw : Eq (α := ℤ_[p] →+* ZMod (p ^ n)) (RingHom.comp (toZModPow p n) (fromPadicInt p))
  (RingHom.comp (PadicInt.toZModPow n) (RingHom.id ℤ_[p]))
Tactic: rw [← RingHom.comp_assoc, toPadicInt, PadicInt.lift_spec]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Compare (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ Eq (α := ℤ_[p] →+* ZMod (p ^ n)) (RingHom.comp (toZModPow p n) (fromPadicInt p))
    (RingHom.comp (PadicInt.toZModPow n) (RingHom.id ℤ_[p]))
have simp : Eq (α := ℤ_[p] →+* ZMod (p ^ n))
  (RingHom.comp (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p n))) (truncate n))
    (lift (fun (k : ℕ) ↦ RingHom.comp (RingEquiv.toRingHom (zmodEquivTrunc p k)) (PadicInt.toZModPow k)) sorry))
  (PadicInt.toZModPow n)
Tactic: simp only [fromPadicInt, toZModPow, RingHom.comp_id]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Compare (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ Eq (α := ℤ_[p] →+* ZMod (p ^ n))
    (RingHom.comp (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p n))) (truncate n))
      (lift (fun (k : ℕ) ↦ RingHom.comp (RingEquiv.toRingHom (zmodEquivTrunc p k)) (PadicInt.toZModPow k)) ⋯))
    (PadicInt.toZModPow n)
have rw : Eq (α := ℤ_[p] →+* ZMod (p ^ n))
  (RingHom.comp
    (@RingHom.comp _ (TruncatedWittVector p n (ZMod p)) _ _ Semiring.toNonAssocSemiring _
      (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p n))) (RingEquiv.toRingHom (zmodEquivTrunc p n)))
    (PadicInt.toZModPow n))
  (PadicInt.toZModPow n)
Tactic: rw [RingHom.comp_assoc, truncate_comp_lift, ← RingHom.comp_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Compare (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ Eq (α := ℤ_[p]) ((RingHom.comp (toPadicInt p) (fromPadicInt p) : (a : ℤ_[p]) → ℤ_[p]) x : ℤ_[p])
    ((RingHom.id ℤ_[p] : (a : ℤ_[p]) → ℤ_[p]) x : ℤ_[p])
have rw : Eq (α := ℤ_[p]) ((RingHom.id ℤ_[p] : (a : ℤ_[p]) → ℤ_[p]) x : ℤ_[p])
  ((RingHom.id ℤ_[p] : (a : ℤ_[p]) → ℤ_[p]) x : ℤ_[p])
Tactic: rw [toPadicInt_comp_fromPadicInt]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Compare (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Eq (α := 𝕎 (ZMod p) →+* 𝕎 (ZMod p)) (RingHom.comp (fromPadicInt p) (toPadicInt p)) (RingHom.id (𝕎 (ZMod p)))
have h : ∀ (k : ℕ),
  Eq (α := 𝕎 (ZMod p) →+* TruncatedWittVector p k (ZMod p))
    (RingHom.comp (truncate k) (RingHom.comp (fromPadicInt p) (toPadicInt p)))
    (RingHom.comp (truncate k) (RingHom.id (𝕎 (ZMod p))))
Tactic: apply WittVector.hom_ext
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Compare (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ Eq (α := 𝕎 (ZMod p) →+* TruncatedWittVector p n (ZMod p))
    (RingHom.comp (truncate n) (RingHom.comp (fromPadicInt p) (toPadicInt p)))
    (RingHom.comp (truncate n) (RingHom.id (𝕎 (ZMod p))))
have h : Eq (α := 𝕎 (ZMod p) →+* TruncatedWittVector p n (ZMod p))
  (RingHom.comp (RingEquiv.toRingHom (zmodEquivTrunc p n)) (RingHom.comp (PadicInt.toZModPow n) (toPadicInt p)))
  (RingHom.comp (truncate n) (RingHom.id (𝕎 (ZMod p))))
Tactic: rw [fromPadicInt, ← RingHom.comp_assoc, truncate_comp_lift, RingHom.comp_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Compare (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : 𝕎 (ZMod p)
⊢ Eq (α := 𝕎 (ZMod p)) ((RingHom.comp (fromPadicInt p) (toPadicInt p) : (a : 𝕎 (ZMod p)) → 𝕎 (ZMod p)) x : 𝕎 (ZMod p))
    ((RingHom.id (𝕎 (ZMod p)) : (a : 𝕎 (ZMod p)) → 𝕎 (ZMod p)) x : 𝕎 (ZMod p))
have rw : Eq (α := 𝕎 (ZMod p)) ((RingHom.id (𝕎 (ZMod p)) : (a : 𝕎 (ZMod p)) → 𝕎 (ZMod p)) x : 𝕎 (ZMod p))
  ((RingHom.id (𝕎 (ZMod p)) : (a : 𝕎 (ZMod p)) → 𝕎 (ZMod p)) x : 𝕎 (ZMod p))
Tactic: rw [fromPadicInt_comp_toPadicInt]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Complete (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
x y : 𝕎 k
n : ℕ
⊢ (∀ i < n, x.coeff i = y.coeff i) ↔
    Eq (α := TruncatedWittVector p n k)
      ((truncate n : (a : 𝕎 k) → TruncatedWittVector p n k) x : TruncatedWittVector p n k)
      ((truncate n : (a : 𝕎 k) → TruncatedWittVector p n k) y : TruncatedWittVector p n k)
have refine_1 : ∀ (h : ∀ i < n, x.coeff i = y.coeff i),
  Eq (α := TruncatedWittVector p n k)
    ((truncate n : (a : 𝕎 k) → TruncatedWittVector p n k) x : TruncatedWittVector p n k)
    ((truncate n : (a : 𝕎 k) → TruncatedWittVector p n k) y : TruncatedWittVector p n k)
Tactic: refine ⟨fun h => ?_, fun h i hi => ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Complete (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
x y : 𝕎 k
n : ℕ
refine_1 :
  ∀ (h : ∀ i < n, x.coeff i = y.coeff i),
    Eq (α := TruncatedWittVector p n k)
      ((truncate n : (a : 𝕎 k) → TruncatedWittVector p n k) x : TruncatedWittVector p n k)
      ((truncate n : (a : 𝕎 k) → TruncatedWittVector p n k) y : TruncatedWittVector p n k)
⊢ (∀ i < n, x.coeff i = y.coeff i) ↔
    Eq (α := TruncatedWittVector p n k)
      ((truncate n : (a : 𝕎 k) → TruncatedWittVector p n k) x : TruncatedWittVector p n k)
      ((truncate n : (a : 𝕎 k) → TruncatedWittVector p n k) y : TruncatedWittVector p n k)
have refine_2 : ∀
  (h :
    Eq (α := TruncatedWittVector p n k)
      ((truncate n : (a : 𝕎 k) → TruncatedWittVector p n k) x : TruncatedWittVector p n k)
      ((truncate n : (a : 𝕎 k) → TruncatedWittVector p n k) y : TruncatedWittVector p n k))
  (i : ℕ) (hi : i < n), x.coeff i = y.coeff i
Tactic: refine ⟨fun h => ?_, fun h i hi => ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Complete (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
x y : 𝕎 k
n : ℕ
h : ∀ i < n, x.coeff i = y.coeff i
⊢ Eq (α := TruncatedWittVector p n k)
    ((truncate n : (a : 𝕎 k) → TruncatedWittVector p n k) x : TruncatedWittVector p n k)
    ((truncate n : (a : 𝕎 k) → TruncatedWittVector p n k) y : TruncatedWittVector p n k)
have refine_1 : ∀ (i : Fin n),
  Eq.{u_1 + 1} (α := k) (TruncatedWittVector.coeff (p := p) i ((truncate n : (a : 𝕎 k) → TruncatedWittVector p n k) x))
    (TruncatedWittVector.coeff (p := p) i ((truncate n : (a : 𝕎 k) → TruncatedWittVector p n k) y))
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Complete (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
x y : 𝕎 k
n : ℕ
h :
  Eq (α := TruncatedWittVector p n k)
    ((truncate n : (a : 𝕎 k) → TruncatedWittVector p n k) x : TruncatedWittVector p n k)
    ((truncate n : (a : 𝕎 k) → TruncatedWittVector p n k) y : TruncatedWittVector p n k)
i : ℕ
hi : i < n
⊢ x.coeff i = y.coeff i
have refine_2 : TruncatedWittVector.coeff (p := p) (⟨i, hi⟩ : Fin n) ((truncate n : (a : 𝕎 k) → TruncatedWittVector p n k) x) =
  y.coeff i
Tactic: rw [← coeff_truncate x ⟨i, hi⟩, ← coeff_truncate y ⟨i, hi⟩, 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
x y : 𝕎 k
n : ℕ
h :
  Eq (α := TruncatedWittVector p n k)
    ((truncate n : (a : 𝕎 k) → TruncatedWittVector p n k) x : TruncatedWittVector p n k)
    ((truncate n : (a : 𝕎 k) → TruncatedWittVector p n k) y : TruncatedWittVector p n k)
i : ℕ
hi : i < n
refine_2 :
  TruncatedWittVector.coeff (p := p) (⟨i, hi⟩ : Fin n) ((truncate n : (a : 𝕎 k) → TruncatedWittVector p n k) x) =
    y.coeff i
⊢ x.coeff i = y.coeff i
have refine_2₁ : Eq.{u_1 + 1} (α := k)
  (TruncatedWittVector.coeff (p := p) (⟨i, hi⟩ : Fin n) ((truncate n : (a : 𝕎 k) → TruncatedWittVector p n k) x))
  (TruncatedWittVector.coeff (p := p) (⟨i, hi⟩ : Fin n) ((truncate n : (a : 𝕎 k) → TruncatedWittVector p n k) y))
Tactic: rw [← coeff_truncate x ⟨i, hi⟩, ← coeff_truncate y ⟨i, hi⟩, 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
x y : 𝕎 k
n : ℕ
h :
  Eq (α := TruncatedWittVector p n k)
    ((truncate n : (a : 𝕎 k) → TruncatedWittVector p n k) x : TruncatedWittVector p n k)
    ((truncate n : (a : 𝕎 k) → TruncatedWittVector p n k) y : TruncatedWittVector p n k)
i : ℕ
hi : i < n
refine_2 :
  TruncatedWittVector.coeff (p := p) (⟨i, hi⟩ : Fin n) ((truncate n : (a : 𝕎 k) → TruncatedWittVector p n k) x) =
    y.coeff i
refine_2₁ :
  Eq.{u_1 + 1} (α := k)
    (TruncatedWittVector.coeff (p := p) (⟨i, hi⟩ : Fin n) ((truncate n : (a : 𝕎 k) → TruncatedWittVector p n k) x))
    (TruncatedWittVector.coeff (p := p) (⟨i, hi⟩ : Fin n) ((truncate n : (a : 𝕎 k) → TruncatedWittVector p n k) y))
⊢ x.coeff i = y.coeff i
have refine_2₂ : Eq.{u_1 + 1} (α := k)
  (TruncatedWittVector.coeff (p := p) (⟨i, hi⟩ : Fin n) ((truncate n : (a : 𝕎 k) → TruncatedWittVector p n k) y))
  (TruncatedWittVector.coeff (p := p) (⟨i, hi⟩ : Fin n) ((truncate n : (a : 𝕎 k) → TruncatedWittVector p n k) y))
Tactic: rw [← coeff_truncate x ⟨i, hi⟩, ← coeff_truncate y ⟨i, hi⟩, 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
x y : 𝕎 k
n : ℕ
⊢ (∀ i < n, x.coeff i = y.coeff i) ↔ ∀ i < n, (x - y).coeff i = 0
have _ : (∀ i < n, x.coeff i = y.coeff i) ↔
  Eq (α := TruncatedWittVector p n k)
    ((truncate n : (a : 𝕎 k) → TruncatedWittVector p n k) x : TruncatedWittVector p n k)
    ((truncate n : (a : 𝕎 k) → TruncatedWittVector p n k) y : TruncatedWittVector p n k)
Tactic: calc
  _ ↔ x.truncate n = y.truncate n := by
    refine ⟨fun h => ?_, fun h i hi => ?_⟩
    · ext i
      simp [h i]
    · rw [← coeff_truncate x ⟨i, hi⟩, ← coeff_truncate y ⟨i, hi⟩, h]
  _ ↔ (x - y).truncate n = 0 := by
    simp only [map_sub, sub_eq_zero]
  _ ↔ _ := by simp only [← mem_ker_truncate, RingHom.mem_ker]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Complete (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
x y : 𝕎 k
n : ℕ
_ :
  (∀ i < n, x.coeff i = y.coeff i) ↔
    Eq (α := TruncatedWittVector p n k)
      ((truncate n : (a : 𝕎 k) → TruncatedWittVector p n k) x : TruncatedWittVector p n k)
      ((truncate n : (a : 𝕎 k) → TruncatedWittVector p n k) y : TruncatedWittVector p n k)
⊢ (∀ i < n, x.coeff i = y.coeff i) ↔ ∀ i < n, (x - y).coeff i = 0
have _₁ : Eq (α := TruncatedWittVector p n k) ((truncate n : (a : 𝕎 k) → TruncatedWittVector p n k) x : TruncatedWittVector p n k)
    ((truncate n : (a : 𝕎 k) → TruncatedWittVector p n k) y : TruncatedWittVector p n k) ↔
  Eq (α := TruncatedWittVector p n k)
    ((truncate n : (a : 𝕎 k) → TruncatedWittVector p n k) (x - y) : TruncatedWittVector p n k)
    (0 : TruncatedWittVector p n k)
Tactic: calc
  _ ↔ x.truncate n = y.truncate n := by
    refine ⟨fun h => ?_, fun h i hi => ?_⟩
    · ext i
      simp [h i]
    · rw [← coeff_truncate x ⟨i, hi⟩, ← coeff_truncate y ⟨i, hi⟩, h]
  _ ↔ (x - y).truncate n = 0 := by
    simp only [map_sub, sub_eq_zero]
  _ ↔ _ := by simp only [← mem_ker_truncate, RingHom.mem_ker]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Complete (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
x y : 𝕎 k
n : ℕ
_ :
  (∀ i < n, x.coeff i = y.coeff i) ↔
    Eq (α := TruncatedWittVector p n k)
      ((truncate n : (a : 𝕎 k) → TruncatedWittVector p n k) x : TruncatedWittVector p n k)
      ((truncate n : (a : 𝕎 k) → TruncatedWittVector p n k) y : TruncatedWittVector p n k)
_₁ :
  Eq (α := TruncatedWittVector p n k)
      ((truncate n : (a : 𝕎 k) → TruncatedWittVector p n k) x : TruncatedWittVector p n k)
      ((truncate n : (a : 𝕎 k) → TruncatedWittVector p n k) y : TruncatedWittVector p n k) ↔
    Eq (α := TruncatedWittVector p n k)
      ((truncate n : (a : 𝕎 k) → TruncatedWittVector p n k) (x - y) : TruncatedWittVector p n k)
      (0 : TruncatedWittVector p n k)
⊢ (∀ i < n, x.coeff i = y.coeff i) ↔ ∀ i < n, (x - y).coeff i = 0
have _₂ : Eq (α := TruncatedWittVector p n k)
    ((truncate n : (a : 𝕎 k) → TruncatedWittVector p n k) (x - y) : TruncatedWittVector p n k)
    (0 : TruncatedWittVector p n k) ↔
  ∀ i < n, (x - y).coeff i = 0
Tactic: calc
  _ ↔ x.truncate n = y.truncate n := by
    refine ⟨fun h => ?_, fun h i hi => ?_⟩
    · ext i
      simp [h i]
    · rw [← coeff_truncate x ⟨i, hi⟩, ← coeff_truncate y ⟨i, hi⟩, h]
  _ ↔ (x - y).truncate n = 0 := by
    simp only [map_sub, sub_eq_zero]
  _ ↔ _ := by simp only [← mem_ker_truncate, RingHom.mem_ker]
-- 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 * (↑p : 𝕎 k) = 0
⊢ x = 0
have rwa : ∀ (h : Eq (α := 𝕎 k) ((frobenius : (a : 𝕎 k) → 𝕎 k) ((verschiebung : (a : 𝕎 k) → 𝕎 k) x : 𝕎 k) : 𝕎 k) (0 : 𝕎 k)), x = 0
Tactic: rwa [← frobenius_verschiebung, _root_.map_eq_zero_iff _ (frobenius_bijective p k).injective,
      _root_.map_eq_zero_iff _ (verschiebung_injective p k)] at h
Cleared hypotheses: 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
h : x * (↑p : 𝕎 k) = 0
rwa :
  ∀ (h : Eq (α := 𝕎 k) ((frobenius : (a : 𝕎 k) → 𝕎 k) ((verschiebung : (a : 𝕎 k) → 𝕎 k) x : 𝕎 k) : 𝕎 k) (0 : 𝕎 k)),
    x = 0
⊢ x = 0
have rwa₁ : ∀ (h : Eq (α := 𝕎 k) ((verschiebung : (a : 𝕎 k) → 𝕎 k) x : 𝕎 k) (0 : 𝕎 k)), x = 0
Tactic: rwa [← frobenius_verschiebung, _root_.map_eq_zero_iff _ (frobenius_bijective p k).injective,
      _root_.map_eq_zero_iff _ (verschiebung_injective p k)] at h
Cleared hypotheses: 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
h : x * (↑p : 𝕎 k) = 0
rwa :
  ∀ (h : Eq (α := 𝕎 k) ((frobenius : (a : 𝕎 k) → 𝕎 k) ((verschiebung : (a : 𝕎 k) → 𝕎 k) x : 𝕎 k) : 𝕎 k) (0 : 𝕎 k)),
    x = 0
rwa₁ : ∀ (h : Eq (α := 𝕎 k) ((verschiebung : (a : 𝕎 k) → 𝕎 k) x : 𝕎 k) (0 : 𝕎 k)), x = 0
⊢ x = 0
have rwa₂ : ∀ (h : x = 0), x = 0
Tactic: rwa [← frobenius_verschiebung, _root_.map_eq_zero_iff _ (frobenius_bijective p k).injective,
      _root_.map_eq_zero_iff _ (verschiebung_injective p k)] at h
Cleared hypotheses: 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
⊢ Membership.mem (γ := Ideal (𝕎 k)) (Ideal.span {(↑p : 𝕎 k)}) x ↔ x.coeff 0 = 0
have simp_rw : (∃ (c : 𝕎 k), x = c * (↑p : 𝕎 k)) ↔ x.coeff 0 = 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
⊢ (∃ (c : 𝕎 k), x = c * (↑p : 𝕎 k)) ↔ x.coeff 0 = 0
have refine_1 : (∃ (c : 𝕎 k), x = c * (↑p : 𝕎 k)) → ∀ (u : 𝕎 k) (hu : x = u * (↑p : 𝕎 k)), x.coeff 0 = 0
Tactic: refine ⟨fun ⟨u, hu⟩ ↦ ?_, 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
refine_1 : (∃ (c : 𝕎 k), x = c * (↑p : 𝕎 k)) → ∀ (u : 𝕎 k) (hu : x = u * (↑p : 𝕎 k)), x.coeff 0 = 0
⊢ (∃ (c : 𝕎 k), x = c * (↑p : 𝕎 k)) ↔ x.coeff 0 = 0
have refine_2 : ∀ (h : x.coeff 0 = 0), ∃ (c : 𝕎 k), x = c * (↑p : 𝕎 k)
Tactic: refine ⟨fun ⟨u, hu⟩ ↦ ?_, 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
h : ∃ (c : 𝕎 k), x = c * (↑p : 𝕎 k)
u : 𝕎 k
hu : x = u * (↑p : 𝕎 k)
⊢ x.coeff 0 = 0
have refine_1 : (u * (↑p : 𝕎 k)).coeff 0 = 0
Tactic: rw [hu, mul_charP_coeff_zero]
-- 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 : ∃ (c : 𝕎 k), x = c * (↑p : 𝕎 k)
u : 𝕎 k
hu : x = u * (↑p : 𝕎 k)
refine_1 : (u * (↑p : 𝕎 k)).coeff 0 = 0
⊢ x.coeff 0 = 0
have refine_1₁ : Eq.{u_1 + 1} (α := k) 0 0
Tactic: rw [hu, mul_charP_coeff_zero]
-- 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
⊢ ∃ (c : 𝕎 k), x = c * (↑p : 𝕎 k)
have h₁ : x =
  HMul.hMul (α := 𝕎 k) (β := 𝕎 k) ((RingEquiv.symm (frobeniusEquiv p k) : (a : 𝕎 k) → 𝕎 k) (x.shift 1) : 𝕎 k)
    ((↑p : 𝕎 k) : 𝕎 k)
Tactic: use (frobeniusEquiv p k).symm (x.shift 1)
-- 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
⊢ (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)
      ((frobenius : (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) _]