awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.WittVector.Compare
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₁))
rw₃ 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₁))
⊢ 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₁))

Tactic:
rw [← RingHom.comp_assoc, commutes, RingHom.comp_assoc,
    PadicInt.zmod_cast_comp_toZModPow _ _ hk]

Premises used: RingHom.comp_assoc, PadicInt.zmod_cast_comp_toZModPow, TruncatedWittVector.commutes
-- Module: Mathlib.RingTheory.WittVector.Compare
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
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]))
⊢ Eq (α := ℤ_[p] →+* ℤ_[p]) (RingHom.comp (toPadicInt p) (fromPadicInt p)) (RingHom.id ℤ_[p])

Tactic:
rw [← PadicInt.toZModPow_eq_iff_ext]

Premises used: PadicInt.toZModPow_eq_iff_ext
-- Module: Mathlib.RingTheory.WittVector.Compare
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
rw :
  Eq (α := ℤ_[p] →+* ZMod (p ^ n)) (RingHom.comp (toZModPow p n) (fromPadicInt p))
    (RingHom.comp (PadicInt.toZModPow n) (RingHom.id ℤ_[p]))
⊢ 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 [← RingHom.comp_assoc, toPadicInt, PadicInt.lift_spec]

Premises used: WittVector.toPadicInt, RingHom.comp_assoc, PadicInt.lift_spec
-- Module: Mathlib.RingTheory.WittVector.Compare
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
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)) ⋯))
    (PadicInt.toZModPow n)
⊢ Eq (α := ℤ_[p] →+* ZMod (p ^ n)) (RingHom.comp (toZModPow p n) (fromPadicInt p))
    (RingHom.comp (PadicInt.toZModPow n) (RingHom.id ℤ_[p]))

Tactic:
simp only [fromPadicInt, toZModPow, RingHom.comp_id]

Premises used: WittVector.toZModPow, RingHom.comp_id, WittVector.fromPadicInt
-- Module: Mathlib.RingTheory.WittVector.Compare
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
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)
⊢ 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)

Tactic:
rw [RingHom.comp_assoc, truncate_comp_lift, ← RingHom.comp_assoc]

Premises used: WittVector.truncate_comp_lift, RingHom.comp_assoc
-- Module: Mathlib.RingTheory.WittVector.Compare
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ 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:
simp only [RingEquiv.symm_toRingHom_comp_toRingHom, RingHom.id_comp]

Premises used: RingEquiv.symm_toRingHom_comp_toRingHom, RingHom.id_comp
-- Module: Mathlib.RingTheory.WittVector.Compare
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
rw rw₁ :
  Eq (α := ℤ_[p]) ((RingHom.id ℤ_[p] : (a : ℤ_[p]) → ℤ_[p]) x : ℤ_[p])
    ((RingHom.id ℤ_[p] : (a : ℤ_[p]) → ℤ_[p]) x : ℤ_[p])
⊢ Eq (α := ℤ_[p]) ((RingHom.comp (toPadicInt p) (fromPadicInt p) : (a : ℤ_[p]) → ℤ_[p]) x : ℤ_[p])
    ((RingHom.id ℤ_[p] : (a : ℤ_[p]) → ℤ_[p]) x : ℤ_[p])

Tactic:
rw [toPadicInt_comp_fromPadicInt]

Premises used: WittVector.toPadicInt_comp_fromPadicInt
-- Module: Mathlib.RingTheory.WittVector.Compare
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
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))))
⊢ Eq (α := 𝕎 (ZMod p) →+* 𝕎 (ZMod p)) (RingHom.comp (fromPadicInt p) (toPadicInt p)) (RingHom.id (𝕎 (ZMod p)))

Tactic:
apply WittVector.hom_ext

Premises used: WittVector.hom_ext
-- Module: Mathlib.RingTheory.WittVector.Compare
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
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))))
⊢ 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))))

Tactic:
rw [fromPadicInt, ← RingHom.comp_assoc, truncate_comp_lift, RingHom.comp_assoc]

Premises used: WittVector.truncate_comp_lift, RingHom.comp_assoc, WittVector.fromPadicInt
-- Module: Mathlib.RingTheory.WittVector.Compare
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ 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:
simp only [toPadicInt, toZModPow, RingHom.comp_id, PadicInt.lift_spec, RingHom.id_comp, ←
    RingHom.comp_assoc, RingEquiv.toRingHom_comp_symm_toRingHom]

Premises used: WittVector.toPadicInt, RingHom.comp_assoc, WittVector.toZModPow, RingHom.comp_id, PadicInt.lift_spec, RingEquiv.toRingHom_comp_symm_toRingHom, RingHom.id_comp
-- Module: Mathlib.RingTheory.WittVector.Compare
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : 𝕎 (ZMod p)
rw 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))
⊢ 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))

Tactic:
rw [fromPadicInt_comp_toPadicInt]

Premises used: WittVector.fromPadicInt_comp_toPadicInt
-- Module: Mathlib.RingTheory.WittVector.Complete
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)

Tactic:
⟨fun h => ?_, fun h i hi => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.RingTheory.WittVector.Complete
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)
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
⊢ (∀ 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 => ?_⟩
-- Module: Mathlib.RingTheory.WittVector.Complete
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
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))
⊢ 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:
ext i
-- Module: Mathlib.RingTheory.WittVector.Complete
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
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:
simp [h i]

Premises used: Fin.val
-- Module: Mathlib.RingTheory.WittVector.Complete
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))
refine_2₂ 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))
⊢ x.coeff i = y.coeff i

Tactic:
rw [← coeff_truncate x ⟨i, hi⟩, ← coeff_truncate y ⟨i, hi⟩, h]

Premises used: WittVector.coeff_truncate, Fin.mk
-- Module: Mathlib.RingTheory.WittVector.Complete
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
x y : 𝕎 k
n : ℕ
⊢ 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:
simp only [map_sub, sub_eq_zero]

Premises used: map_sub, sub_eq_zero
-- Module: Mathlib.RingTheory.WittVector.Complete
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
x y : 𝕎 k
n : ℕ
⊢ 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:
simp only [← mem_ker_truncate, RingHom.mem_ker]

Premises used: RingHom.mem_ker, WittVector.mem_ker_truncate
-- Module: Mathlib.RingTheory.WittVector.Complete
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)
_₂ :
  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
⊢ (∀ i < n, x.coeff i = y.coeff i) ↔ ∀ 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]

Premises used: HSub.hSub, WittVector.truncate, DFunLike.coe
-- Module: Mathlib.RingTheory.WittVector.Complete
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
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (h : x = 0), 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

Premises used: WittVector.verschiebung_injective, WittVector.frobenius_bijective, Function.Bijective.injective, map_eq_zero_iff, WittVector.frobenius_verschiebung
-- Module: Mathlib.RingTheory.WittVector.Complete
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
simp_rw : (∃ (c : 𝕎 k), x = c * (↑p : 𝕎 k)) ↔ x.coeff 0 = 0
⊢ Membership.mem (γ := Ideal (𝕎 k)) (Ideal.span {(↑p : 𝕎 k)}) x ↔ x.coeff 0 = 0

Tactic:
simp_rw [Ideal.mem_span_singleton, dvd_def, mul_comm]

Premises used: dvd_def, mul_comm, Ideal.mem_span_singleton
-- Module: Mathlib.RingTheory.WittVector.Complete
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

Tactic:
⟨fun ⟨u, hu⟩ ↦ ?_, fun h ↦ ?_⟩

Premises used: _private.0.WittVector.mem_span_p_iff_coeff_zero_eq_zero.match_2, Iff.intro, WittVector.coeff, OfNat.ofNat, Eq
-- Module: Mathlib.RingTheory.WittVector.Complete
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
refine_2 : ∀ (h : x.coeff 0 = 0), ∃ (c : 𝕎 k), x = c * (↑p : 𝕎 k)
⊢ (∃ (c : 𝕎 k), x = c * (↑p : 𝕎 k)) ↔ x.coeff 0 = 0

Tactic:
refine ⟨fun ⟨u, hu⟩ ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.RingTheory.WittVector.Complete
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
refine_1₁ refine_1₂ : Eq.{u_1 + 1} (α := k) 0 0
⊢ x.coeff 0 = 0

Tactic:
rw [hu, mul_charP_coeff_zero]

Premises used: WittVector.mul_charP_coeff_zero
-- Module: Mathlib.RingTheory.WittVector.Complete
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
h₁ :
  x =
    HMul.hMul (α := 𝕎 k) (β := 𝕎 k) ((RingEquiv.symm (frobeniusEquiv p k) : (a : 𝕎 k) → 𝕎 k) (x.shift 1) : 𝕎 k)
      ((↑p : 𝕎 k) : 𝕎 k)
⊢ ∃ (c : 𝕎 k), x = c * (↑p : 𝕎 k)

Tactic:
use (frobeniusEquiv p k).symm (x.shift 1)

Premises used: WittVector.frobeniusEquiv, WittVector.shift, OfNat.ofNat, DFunLike.coe, RingEquiv.symm
-- Module: Mathlib.RingTheory.WittVector.Complete
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
⊢ ∀ i < 1, x.coeff i = 0

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.WittVector.Complete
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)

Tactic:
simpa using eq_iterate_verschiebung (n := 1) (by simp [h])

Premises used: WittVector.eq_iterate_verschiebung
-- Module: Mathlib.RingTheory.WittVector.Complete
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)
rw₂ rw₃ :
  Eq (α := 𝕎 k) ((verschiebung : (a : 𝕎 k) → 𝕎 k) (x.shift 1) : 𝕎 k)
    ((verschiebung : (a : 𝕎 k) → 𝕎 k) (x.shift 1) : 𝕎 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)

Tactic:
rw [← verschiebung_frobenius, ← frobeniusEquiv_apply,
          RingEquiv.apply_symm_apply (frobeniusEquiv p k) _]

Premises used: RingEquiv.apply_symm_apply, WittVector.frobeniusEquiv, WittVector.verschiebung_frobenius, WittVector.frobeniusEquiv_apply
-- Module: Mathlib.RingTheory.WittVector.Complete
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)
_₁ :
  (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)
⊢ x =
    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) _]

Premises used: WittVector.shift, OfNat.ofNat, DFunLike.coe, WittVector.verschiebung
-- Module: Mathlib.RingTheory.WittVector.Complete
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 : ℕ
simp_rw : (∃ (c : 𝕎 k), x = c * HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n) ↔ ∀ m < n, x.coeff m = 0
⊢ Membership.mem (γ := Ideal (𝕎 k)) (Ideal.span {HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n}) x ↔ ∀ m < n, x.coeff m = 0

Tactic:
simp_rw [Ideal.mem_span_singleton, dvd_def, mul_comm]

Premises used: dvd_def, mul_comm, Ideal.mem_span_singleton
-- Module: Mathlib.RingTheory.WittVector.Complete
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

Tactic:
⟨fun ⟨u, hu⟩ m hm ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro, _private.0.WittVector.mem_span_p_pow_iff_le_coeff_eq_zero.match_1, WittVector.coeff, OfNat.ofNat, Eq
-- Module: Mathlib.RingTheory.WittVector.Complete
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
refine_2 : ∀ (h : ∀ m < n, x.coeff m = 0), ∃ (c : 𝕎 k), x = c * HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n
⊢ (∃ (c : 𝕎 k), x = c * HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n) ↔ ∀ m < n, x.coeff m = 0

Tactic:
refine ⟨fun ⟨u, hu⟩ m hm ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.RingTheory.WittVector.Complete
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
refine_1₁ refine_1₂ : Eq.{u_1 + 1} (α := k) 0 0
⊢ x.coeff m = 0

Tactic:
rw [hu, mul_pow_charP_coeff_zero _ hm]

Premises used: WittVector.mul_pow_charP_coeff_zero
-- Module: Mathlib.RingTheory.WittVector.Complete
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
h₁ : x = (⇑(RingEquiv.symm (frobeniusEquiv p k)) : (a : 𝕎 k) → 𝕎 k)^[n] (x.shift n) * HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n
⊢ ∃ (c : 𝕎 k), x = c * HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n

Tactic:
use (frobeniusEquiv p k).symm^[n] (x.shift n)

Premises used: WittVector.frobeniusEquiv, Nat.iterate, WittVector.shift, DFunLike.coe, RingEquiv.symm
-- Module: Mathlib.RingTheory.WittVector.Complete
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
h₁ :
  x =
    (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n]
      ((⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[n] ((⇑(RingEquiv.symm (frobeniusEquiv p k)) : (a : 𝕎 k) → 𝕎 k)^[n] (x.shift n)))
⊢ x = (⇑(RingEquiv.symm (frobeniusEquiv p k)) : (a : 𝕎 k) → 𝕎 k)^[n] (x.shift n) * HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n

Tactic:
rw [← iterate_verschiebung_iterate_frobenius]

Premises used: WittVector.iterate_verschiebung_iterate_frobenius
-- Module: Mathlib.RingTheory.WittVector.Complete
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)

Tactic:
simpa using eq_iterate_verschiebung (x := x) (n := n) h

Premises used: WittVector.eq_iterate_verschiebung
-- Module: Mathlib.RingTheory.WittVector.Complete
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 =
    (⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[n] ((⇑(RingEquiv.symm (frobeniusEquiv p k)) : (a : 𝕎 k) → 𝕎 k)^[n] (x.shift n))
⊢ (⇑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:
congr