awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp_1 : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
hp : ¬IsUnit.{u_1} (M := 𝕎 k) (↑p : 𝕎 k)
a : 𝕎 k
ha : a.coeff 0 ≠ 0
b : 𝕎 k
hb : b.coeff 0 ≠ 0
n_1 : ℕ
ha0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1] a ≠ 0
n : ℕ
hb0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n + 1] b ≠ 0
hab :
  coeff (p := p) (↑p : 𝕎 k) 1 =
    ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1 + (n + 1)]
          ((⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[n + 1] a * (⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1] b)).coeff
      1
⊢ Eq.{u_1 + 1} (α := k) 1 0

Tactic:
simp only [coeff_p_one, Nat.add_succ, add_comm _ n, Function.iterate_succ', Function.comp_apply,
    verschiebung_coeff_add_one, verschiebung_coeff_zero] at hab

Premises used: Function.iterate_succ', WittVector.verschiebung_coeff_zero, add_comm, Nat.add_succ, Function.comp_apply, WittVector.verschiebung_coeff_add_one, WittVector.coeff_p_one
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp_1 : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
hp : ¬IsUnit.{u_1} (M := 𝕎 k) (↑p : 𝕎 k)
a : 𝕎 k
ha : a.coeff 0 ≠ 0
b : 𝕎 k
hb : b.coeff 0 ≠ 0
n_1 : ℕ
ha0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1] a ≠ 0
n : ℕ
hb0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n + 1] b ≠ 0
hab : Eq.{u_1 + 1} (α := k) 1 0
⊢ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1] a) ∨ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n + 1] b)

Tactic:
(one_ne_zero hab).elim

Premises used: False.elim, one_ne_zero
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp_1 : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
hp : ¬IsUnit.{u_1} (M := 𝕎 k) (↑p : 𝕎 k)
a : 𝕎 k
ha : a.coeff 0 ≠ 0
b : 𝕎 k
hb : b.coeff 0 ≠ 0
n_1 : ℕ
ha0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1] a ≠ 0
n : ℕ
hb0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n + 1] b ≠ 0
hab : Eq.{u_1 + 1} (α := k) 1 0
⊢ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1] a) ∨ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n + 1] b)

Tactic:
exact (one_ne_zero hab).elim

Premises used: False.elim, one_ne_zero
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
obtain :
  ∀ (m : ℕ) (c : 𝕎 k) (hc : c.coeff 0 ≠ 0) (hcm : a = (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] c),
    ∃ (m : ℕ) (b : 𝕎 k), b.coeff 0 ≠ 0 ∧ a = HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * b
⊢ ∃ (m : ℕ) (b : 𝕎 k), b.coeff 0 ≠ 0 ∧ a = HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * b

Tactic:
obtain ⟨m, c, hc, hcm⟩ := WittVector.verschiebung_nonzero ha

Premises used: WittVector.verschiebung_nonzero
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
c : 𝕎 k
hc : c.coeff 0 ≠ 0
hcm : a = (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] c
obtain :
  ∀ (b : 𝕎 k) (hc : ((⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[m] b).coeff 0 ≠ 0)
    (hcm : a = (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] ((⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[m] b)),
    ∃ (m : ℕ) (b : 𝕎 k), b.coeff 0 ≠ 0 ∧ a = HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * b
⊢ ∃ (m : ℕ) (b : 𝕎 k), b.coeff 0 ≠ 0 ∧ a = HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * b

Tactic:
obtain ⟨b, rfl⟩ := (frobenius_bijective p k).surjective.iterate m c

Premises used: WittVector.frobenius_bijective, Function.Bijective.surjective, Function.Surjective.iterate, rfl
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : ((⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[m] b).coeff 0 ≠ 0
hcm : a = (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] ((⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[m] b)
⊢ b.coeff 0 ^ p ^ m ≠ 0

Tactic:
rw [WittVector.iterate_frobenius_coeff] at hc

Premises used: WittVector.iterate_frobenius_coeff
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : ((⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[m] b).coeff 0 ≠ 0
hcm : a = (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] ((⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[m] b)
hc₁ : b.coeff 0 ^ p ^ m ≠ 0
⊢ a = (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] ((⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[m] b)

Tactic:
rw [WittVector.iterate_frobenius_coeff] at hc

Premises used: WittVector.iterate_frobenius_coeff
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : b.coeff 0 ^ p ^ m ≠ 0
hcm : a = (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] ((⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[m] b)
⊢ (Function.comp (β := 𝕎 k) (⇑verschiebung : (a : 𝕎 k) → 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k))^[m] b =
    ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] ∘ (⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[m]) b

Tactic:
have := congr_fun (WittVector.verschiebung_frobenius_comm.comp_iterate m) b
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : b.coeff 0 ^ p ^ m ≠ 0
hcm : a = (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] ((⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[m] b)
this :
  (Function.comp (β := 𝕎 k) (⇑verschiebung : (a : 𝕎 k) → 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k))^[m] b =
    (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] ((⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[m] b)
⊢ a = (Function.comp (β := 𝕎 k) (⇑verschiebung : (a : 𝕎 k) → 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k))^[m] b

Tactic:
rw [← this] at hcm
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : b.coeff 0 ^ p ^ m ≠ 0
hcm : a = (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] ((⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[m] b)
this :
  (Function.comp (β := 𝕎 k) (⇑verschiebung : (a : 𝕎 k) → 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k))^[m] b =
    (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] ((⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[m] b)
hcm₁ : a = (Function.comp (β := 𝕎 k) (⇑verschiebung : (a : 𝕎 k) → 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k))^[m] b
⊢ (Function.comp (β := 𝕎 k) (⇑verschiebung : (a : 𝕎 k) → 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k))^[m] b =
    (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] ((⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[m] b)

Tactic:
rw [← this] at hcm
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : b.coeff 0 ^ p ^ m ≠ 0
hcm : a = (Function.comp (β := 𝕎 k) (⇑verschiebung : (a : 𝕎 k) → 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k))^[m] b
this :
  (Function.comp (β := 𝕎 k) (⇑verschiebung : (a : 𝕎 k) → 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k))^[m] b =
    (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] ((⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[m] b)
⊢ ∃ (m : ℕ) (b : 𝕎 k), b.coeff 0 ≠ 0 ∧ a = HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * b

Tactic:
⟨m, b, ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : b.coeff 0 ^ p ^ m ≠ 0
hcm : a = (Function.comp (β := 𝕎 k) (⇑verschiebung : (a : 𝕎 k) → 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k))^[m] b
this :
  (Function.comp (β := 𝕎 k) (⇑verschiebung : (a : 𝕎 k) → 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k))^[m] b =
    (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] ((⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[m] b)
refine_1 : b.coeff 0 ≠ 0
refine_2 : a = HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * b
⊢ ∃ (m : ℕ) (b : 𝕎 k), b.coeff 0 ≠ 0 ∧ a = HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * b

Tactic:
refine ⟨m, b, ?_, ?_⟩
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : b.coeff 0 ^ p ^ m ≠ 0
hcm : a = (Function.comp (β := 𝕎 k) (⇑verschiebung : (a : 𝕎 k) → 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k))^[m] b
this :
  (Function.comp (β := 𝕎 k) (⇑verschiebung : (a : 𝕎 k) → 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k))^[m] b =
    (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] ((⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[m] b)
refine_1 : ∀ (hc : b.coeff 0 = 0), b.coeff 0 ^ p ^ m = 0
⊢ b.coeff 0 ≠ 0

Tactic:
contrapose hc
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hcm : a = (Function.comp (β := 𝕎 k) (⇑verschiebung : (a : 𝕎 k) → 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k))^[m] b
this :
  (Function.comp (β := 𝕎 k) (⇑verschiebung : (a : 𝕎 k) → 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k))^[m] b =
    (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] ((⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[m] b)
hc : b.coeff 0 = 0
⊢ b.coeff 0 ^ p ^ m = 0

Tactic:
simp [hc, zero_pow <| pow_ne_zero _ hp.out.ne_zero]

Premises used: pow_ne_zero, Nat.Prime.ne_zero, zero_pow, Fact.out
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : b.coeff 0 ^ p ^ m ≠ 0
hcm : a = (Function.comp (β := 𝕎 k) (⇑verschiebung : (a : 𝕎 k) → 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k))^[m] b
this :
  (Function.comp (β := 𝕎 k) (⇑verschiebung : (a : 𝕎 k) → 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k))^[m] b =
    (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] ((⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[m] b)
refine_2 : a = (fun (x : 𝕎 k) ↦ (↑p : 𝕎 k) * x)^[m] b
⊢ a = HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * b

Tactic:
simp_rw [← mul_left_iterate (p : 𝕎 k) m]
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : b.coeff 0 ^ p ^ m ≠ 0
hcm : a = (Function.comp (β := 𝕎 k) (⇑verschiebung : (a : 𝕎 k) → 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k))^[m] b
this :
  (Function.comp (β := 𝕎 k) (⇑verschiebung : (a : 𝕎 k) → 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k))^[m] b =
    (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] ((⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[m] b)
⊢ a = (Function.comp (β := 𝕎 k) (⇑verschiebung : (a : 𝕎 k) → 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k))^[m] b

Tactic:
hcm
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : b.coeff 0 ^ p ^ m ≠ 0
hcm : a = (Function.comp (β := 𝕎 k) (⇑verschiebung : (a : 𝕎 k) → 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k))^[m] b
this :
  (Function.comp (β := 𝕎 k) (⇑verschiebung : (a : 𝕎 k) → 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k))^[m] b =
    (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] ((⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[m] b)
h :
  Eq.{u_1 + 1} (α := 𝕎 k → 𝕎 k) (fun (x : 𝕎 k) ↦ (↑p : 𝕎 k) * x)
    (Function.comp (β := 𝕎 k) (⇑verschiebung : (a : 𝕎 k) → 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k))
⊢ a = (fun (x : 𝕎 k) ↦ (↑p : 𝕎 k) * x)^[m] b

Tactic:
convert! hcm using 2
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : b.coeff 0 ^ p ^ m ≠ 0
hcm : a = (Function.comp (β := 𝕎 k) (⇑verschiebung : (a : 𝕎 k) → 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k))^[m] b
this :
  (Function.comp (β := 𝕎 k) (⇑verschiebung : (a : 𝕎 k) → 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k))^[m] b =
    (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] ((⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[m] b)
h :
  ∀ (x : 𝕎 k),
    (↑p : 𝕎 k) * x = Function.comp (β := 𝕎 k) (⇑verschiebung : (a : 𝕎 k) → 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k) x
⊢ Eq.{u_1 + 1} (α := 𝕎 k → 𝕎 k) (fun (x : 𝕎 k) ↦ (↑p : 𝕎 k) * x)
    (Function.comp (β := 𝕎 k) (⇑verschiebung : (a : 𝕎 k) → 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k))

Tactic:
ext1 x
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : b.coeff 0 ^ p ^ m ≠ 0
hcm : a = (Function.comp (β := 𝕎 k) (⇑verschiebung : (a : 𝕎 k) → 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k))^[m] b
this :
  (Function.comp (β := 𝕎 k) (⇑verschiebung : (a : 𝕎 k) → 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k))^[m] b =
    (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] ((⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[m] b)
x : 𝕎 k
h :
  Eq (α := 𝕎 k) ((verschiebung : (a : 𝕎 k) → 𝕎 k) ((frobenius : (a : 𝕎 k) → 𝕎 k) x : 𝕎 k) : 𝕎 k)
    (Function.comp (β := 𝕎 k) (⇑verschiebung : (a : 𝕎 k) → 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k) x : 𝕎 k)
⊢ (↑p : 𝕎 k) * x = Function.comp (β := 𝕎 k) (⇑verschiebung : (a : 𝕎 k) → 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k) x

Tactic:
rw [mul_comm, ← WittVector.verschiebung_frobenius x]

Premises used: WittVector.verschiebung_frobenius, mul_comm
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : b.coeff 0 ^ p ^ m ≠ 0
hcm : a = (Function.comp (β := 𝕎 k) (⇑verschiebung : (a : 𝕎 k) → 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k))^[m] b
this :
  (Function.comp (β := 𝕎 k) (⇑verschiebung : (a : 𝕎 k) → 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k))^[m] b =
    (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] ((⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[m] b)
x : 𝕎 k
⊢ Eq (α := 𝕎 k) ((verschiebung : (a : 𝕎 k) → 𝕎 k) ((frobenius : (a : 𝕎 k) → 𝕎 k) x : 𝕎 k) : 𝕎 k)
    (Function.comp (β := 𝕎 k) (⇑verschiebung : (a : 𝕎 k) → 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k) x : 𝕎 k)

Tactic:
rfl
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
inst_2 : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
obtain :
  ∀ (m : ℕ) (b : 𝕎 k) (h₁ : b.coeff 0 ≠ 0) (h₂ : a = HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * b),
    ∃ (m : ℕ) (b : (𝕎 k)ˣ), a = HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * (↑b : 𝕎 k)
⊢ ∃ (m : ℕ) (b : (𝕎 k)ˣ), a = HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * (↑b : 𝕎 k)

Tactic:
obtain ⟨m, b, h₁, h₂⟩ := exists_eq_pow_p_mul a ha

Premises used: WittVector.exists_eq_pow_p_mul
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
inst_2 : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
h₁ : b.coeff 0 ≠ 0
h₂ : a = HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * b
b₀ : kˣ := Units.mk0 (b.coeff 0) h₁
⊢ b.coeff 0 = (↑b₀ : k)

Tactic:
have hb₀ : b.coeff 0 = b₀ := rfl
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
inst_2 : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
h₁ : b.coeff 0 ≠ 0
h₂ : a = HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * b
b₀ : kˣ := Units.mk0 (b.coeff 0) h₁
hb₀ : b.coeff 0 = (↑b₀ : k)
⊢ ∃ (m : ℕ) (b : (𝕎 k)ˣ), a = HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * (↑b : 𝕎 k)

Tactic:
⟨m, mkUnit hb₀, h₂⟩

Premises used: Exists.intro, WittVector.mkUnit
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
inst_2 : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
h₁ : b.coeff 0 ≠ 0
h₂ : a = HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * b
b₀ : kˣ := Units.mk0 (b.coeff 0) h₁
hb₀ : b.coeff 0 = (↑b₀ : k)
⊢ ∃ (m : ℕ) (b : (𝕎 k)ˣ), a = HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * (↑b : 𝕎 k)

Tactic:
exact ⟨m, mkUnit hb₀, h₂⟩
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
inst_2 : PerfectRing k p
⊢ IsDiscreteValuationRing.HasUnitMulPowIrreducibleFactorization.{u_1} (𝕎 k)

Tactic:
⟨p, irreducible p, fun {x} hx => ?_⟩

Premises used: Nat.cast, WittVector.irreducible, IsDiscreteValuationRing.HasUnitMulPowIrreducibleFactorization, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
inst_2 : PerfectRing k p
refine : ∀ {x : 𝕎 k} (hx : x ≠ 0), ∃ (n : ℕ), Associated (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n) x
⊢ IsDiscreteValuationRing.HasUnitMulPowIrreducibleFactorization.{u_1} (𝕎 k)

Tactic:
refine ⟨p, irreducible p, fun {x} hx => ?_⟩
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
inst_2 : PerfectRing k p
x : 𝕎 k
hx : x ≠ 0
obtain :
  ∀ (n : ℕ) (b : (𝕎 k)ˣ) (hb : x = HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n * (↑b : 𝕎 k)),
    ∃ (n : ℕ), Associated (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n) x
⊢ ∃ (n : ℕ), Associated (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n) x

Tactic:
obtain ⟨n, b, hb⟩ := exists_eq_pow_p_mul' x hx

Premises used: WittVector.exists_eq_pow_p_mul'
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
inst_2 : PerfectRing k p
x : 𝕎 k
hx : x ≠ 0
n : ℕ
b : (𝕎 k)ˣ
hb : x = HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n * (↑b : 𝕎 k)
⊢ ∃ (n : ℕ), Associated (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n) x

Tactic:
⟨n, b, hb.symm⟩

Premises used: Exists.intro, Eq.symm
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
inst_2 : PerfectRing k p
x : 𝕎 k
hx : x ≠ 0
n : ℕ
b : (𝕎 k)ˣ
hb : x = HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n * (↑b : 𝕎 k)
⊢ ∃ (n : ℕ), Associated (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n) x

Tactic:
exact ⟨n, b, hb.symm⟩
-- Module: Mathlib.RingTheory.WittVector.Domain
Goal:
p : ℕ
R : Type u_1
x : 𝕎 R
n k : ℕ
⊢ (x.shift n).coeff k = x.coeff (n + k)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.WittVector.Domain
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
k : ℕ
h : ∀ i < k + 1, x.coeff i = 0
h₁ : coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) (x.shift k.succ)) 0 = (x.shift k).coeff 0
h₂ : ∀ (n : ℕ), coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) (x.shift k.succ)) (n + 1) = (x.shift k).coeff (n + 1)
⊢ (verschiebung : (a : 𝕎 R) → 𝕎 R) (x.shift k.succ) = x.shift k

Tactic:
ext ⟨j⟩
-- Module: Mathlib.RingTheory.WittVector.Domain
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
k : ℕ
h : ∀ i < k + 1, x.coeff i = 0
h₁ : k + 0 < k + 1
⊢ coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) (x.shift k.succ)) 0 = (x.shift k).coeff 0

Tactic:
rw [verschiebung_coeff_zero, shift_coeff, h]

Premises used: WittVector.verschiebung_coeff_zero, WittVector.shift_coeff
-- Module: Mathlib.RingTheory.WittVector.Domain
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
k : ℕ
h : ∀ i < k + 1, x.coeff i = 0
⊢ k + 0 < k + 1

Tactic:
apply Nat.lt_succ_self

Premises used: Nat.lt_succ_self
-- Module: Mathlib.RingTheory.WittVector.Domain
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
k : ℕ
h : ∀ i < k + 1, x.coeff i = 0
n : ℕ
h₁ : x.coeff (k.succ + n) = x.coeff (k + (n + 1))
⊢ coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) (x.shift k.succ)) (n + 1) = (x.shift k).coeff (n + 1)

Tactic:
simp only [verschiebung_coeff_succ, shift]

Premises used: WittVector.verschiebung_coeff_succ, WittVector.shift
-- Module: Mathlib.RingTheory.WittVector.Domain
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
k : ℕ
h : ∀ i < k + 1, x.coeff i = 0
n : ℕ
h₁ : k.succ + n = k + (n + 1)
⊢ x.coeff (k.succ + n) = x.coeff (k + (n + 1))

Tactic:
congr 1
-- Module: Mathlib.RingTheory.WittVector.Domain
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
k : ℕ
h : ∀ i < k + 1, x.coeff i = 0
n : ℕ
h₁ : k.succ + n = (k + n).succ
h₂ : n + k.succ = (k + n).succ
h₃ : (n + k).succ = (k + n).succ
h₄ h₅ : (k + n).succ = (k + n).succ
⊢ k.succ + n = k + (n + 1)

Tactic:
rw [Nat.add_succ, add_comm, Nat.add_succ, add_comm]

Premises used: add_comm, Nat.add_succ
-- Module: Mathlib.RingTheory.WittVector.Domain
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
h : ∀ i < 0, x.coeff i = 0
zero :
  ∀ (coeff : ℕ → R) (h : ∀ i < 0, WittVector.coeff (p := p) { coeff := coeff : 𝕎 R } i = 0),
    Eq (α := 𝕎 R) { coeff := coeff } ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[0] (shift { coeff := coeff } 0))
⊢ x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[0] (x.shift 0)

Tactic:
cases x
-- Module: Mathlib.RingTheory.WittVector.Domain
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
coeff : ℕ → R
h : ∀ i < 0, WittVector.coeff (p := p) { coeff := coeff : 𝕎 R } i = 0
⊢ Eq (α := 𝕎 R) { coeff := coeff } ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[0] (shift { coeff := coeff } 0))

Tactic:
simp [shift]

Premises used: WittVector.shift
-- Module: Mathlib.RingTheory.WittVector.Domain
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
k : ℕ
ih : ∀ (h : ∀ i < k, x.coeff i = 0), x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[k] (x.shift k)
h : ∀ i < k + 1, x.coeff i = 0
succ : x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[k] ((verschiebung : (a : 𝕎 R) → 𝕎 R) (x.shift (k + 1)))
⊢ x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[k + 1] (x.shift (k + 1))

Tactic:
dsimp
-- Module: Mathlib.RingTheory.WittVector.Domain
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
k : ℕ
ih : ∀ (h : ∀ i < k, x.coeff i = 0), x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[k] (x.shift k)
h : ∀ i < k + 1, x.coeff i = 0
succ : x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[k] (x.shift k)
succ₁ : ∀ i < k + 1, x.coeff i = 0
⊢ x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[k] ((verschiebung : (a : 𝕎 R) → 𝕎 R) (x.shift (k + 1)))

Tactic:
rw [verschiebung_shift]

Premises used: WittVector.verschiebung_shift
-- Module: Mathlib.RingTheory.WittVector.Domain
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
k : ℕ
ih : ∀ (h : ∀ i < k, x.coeff i = 0), x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[k] (x.shift k)
h : ∀ i < k + 1, x.coeff i = 0
⊢ x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[k] (x.shift k)

Tactic:
ih fun i hi => h _ (hi.trans (Nat.lt_succ_self _))

Premises used: Nat.lt_succ_self, LT.lt.trans
-- Module: Mathlib.RingTheory.WittVector.Domain
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
k : ℕ
ih : ∀ (h : ∀ i < k, x.coeff i = 0), x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[k] (x.shift k)
h : ∀ i < k + 1, x.coeff i = 0
⊢ x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[k] (x.shift k)

Tactic:
exact ih fun i hi => h _ (hi.trans (Nat.lt_succ_self _))

Premises used: Nat.lt_succ_self, LT.lt.trans
-- Module: Mathlib.RingTheory.WittVector.Domain
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
k : ℕ
ih : ∀ (h : ∀ i < k, x.coeff i = 0), x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[k] (x.shift k)
h : ∀ i < k + 1, x.coeff i = 0
⊢ ∀ i < k + 1, x.coeff i = 0

Tactic:
h
-- Module: Mathlib.RingTheory.WittVector.Domain
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
k : ℕ
ih : ∀ (h : ∀ i < k, x.coeff i = 0), x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[k] (x.shift k)
h : ∀ i < k + 1, x.coeff i = 0
⊢ ∀ i < k + 1, x.coeff i = 0

Tactic:
exact h
-- Module: Mathlib.RingTheory.WittVector.Domain
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
n : ℕ
h : ∀ i < n, x.coeff i = 0
zero : ∀ (h : ∀ i < 0, x.coeff i = 0), x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[0] (x.shift 0)
succ :
  ∀ (k : ℕ) (ih : ∀ (h : ∀ i < k, x.coeff i = 0), x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[k] (x.shift k))
    (h : ∀ i < k + 1, x.coeff i = 0), x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[k + 1] (x.shift (k + 1))
⊢ x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] (x.shift n)

Tactic:
induction n with
  | zero => cases x; simp [shift]
  | succ k ih =>
    dsimp; rw [verschiebung_shift]
    · exact ih fun i hi => h _ (hi.trans (Nat.lt_succ_self _))
    · exact h

Premises used: WittVector.verschiebung_shift, WittVector.shift