awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.DiscreteValuationRing (hypothesis)
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₁
⊢ ∃ (m : ℕ) (b : (𝕎 k)ˣ), a = HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * (↑b : 𝕎 k)
have hb₀ : b.coeff 0 = (↑b₀ : k)
Tactic: have hb₀ : b.coeff 0 = b₀ := rfl
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.DiscreteValuationRing (goal)
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)
have refine : ∀ {x : 𝕎 k} (hx : x ≠ 0), ∃ (n : ℕ), Associated (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n) x
Tactic: refine ⟨p, irreducible p, fun {x} hx => ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.DiscreteValuationRing (goal)
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 : ℕ), Associated (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n) x
have obtain : ∀ (n : ℕ) (b : (𝕎 k)ˣ) (hb : x = HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n * (↑b : 𝕎 k)),
  ∃ (n : ℕ), Associated (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n) x
Tactic: obtain ⟨n, b, hb⟩ := exists_eq_pow_p_mul' x hx
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Domain (goal)
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
⊢ (verschiebung : (a : 𝕎 R) → 𝕎 R) (x.shift k.succ) = x.shift k
have h₁ : coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) (x.shift k.succ)) 0 = (x.shift k).coeff 0
Tactic: ext ⟨j⟩
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Domain (goal)
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
⊢ (verschiebung : (a : 𝕎 R) → 𝕎 R) (x.shift k.succ) = x.shift k
have h₂ : ∀ (n : ℕ), coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) (x.shift k.succ)) (n + 1) = (x.shift k).coeff (n + 1)
Tactic: ext ⟨j⟩
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Domain (goal)
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
⊢ coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) (x.shift k.succ)) 0 = (x.shift k).coeff 0
have h₁ : k + 0 < k + 1
Tactic: rw [verschiebung_coeff_zero, shift_coeff, h]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Domain (goal)
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 : ℕ
⊢ coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) (x.shift k.succ)) (n + 1) = (x.shift k).coeff (n + 1)
have h₁ : x.coeff (k.succ + n) = x.coeff (k + (n + 1))
Tactic: simp only [verschiebung_coeff_succ, shift]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Domain (goal)
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 : ℕ
⊢ x.coeff (k.succ + n) = x.coeff (k + (n + 1))
have h₁ : k.succ + n = k + (n + 1)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Domain (goal)
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 : ℕ
⊢ k.succ + n = k + (n + 1)
have h₁ : k.succ + n = (k + n).succ
Tactic: rw [Nat.add_succ, add_comm, Nat.add_succ, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Domain (goal)
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
⊢ k.succ + n = k + (n + 1)
have h₂ : n + k.succ = (k + n).succ
Tactic: rw [Nat.add_succ, add_comm, Nat.add_succ, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Domain (goal)
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
⊢ k.succ + n = k + (n + 1)
have h₃ : (n + k).succ = (k + n).succ
Tactic: rw [Nat.add_succ, add_comm, Nat.add_succ, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Domain (goal)
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
⊢ k.succ + n = k + (n + 1)
have h₄ : (k + n).succ = (k + n).succ
Tactic: rw [Nat.add_succ, add_comm, Nat.add_succ, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Domain (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
h : ∀ i < 0, x.coeff i = 0
⊢ x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[0] (x.shift 0)
have 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))
Tactic: cases x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Domain (goal)
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 + 1] (x.shift (k + 1))
have succ : x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[k] ((verschiebung : (a : 𝕎 R) → 𝕎 R) (x.shift (k + 1)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Domain (goal)
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] ((verschiebung : (a : 𝕎 R) → 𝕎 R) (x.shift (k + 1)))
have succ : x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[k] (x.shift k)
Tactic: rw [verschiebung_shift]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Domain (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
n : ℕ
h : ∀ i < n, x.coeff i = 0
⊢ x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] (x.shift n)
have zero : ∀ (h : ∀ i < 0, x.coeff i = 0), x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[0] (x.shift 0)
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
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Domain (goal)
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)
⊢ x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] (x.shift n)
have 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))
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
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Domain (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
hx : x ≠ 0
⊢ ∃ (k : ℕ), x.coeff k ≠ 0
have by_contra! : ∀ (hall : ∀ (k : ℕ), x.coeff k = 0), False
Tactic: by_contra! hall
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Domain (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
hx : x ≠ 0
hall : ∀ (k : ℕ), x.coeff k = 0
⊢ False
have apply : x = 0
Tactic: apply hx
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Domain (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
hx : x ≠ 0
hall : ∀ (k : ℕ), x.coeff k = 0
⊢ x = 0
have h : ∀ (i : ℕ), x.coeff i = coeff (p := p) 0 i
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Domain (hypothesis)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
hx : x ≠ 0
⊢ ∃ (n : ℕ) (x' : 𝕎 R), x'.coeff 0 ≠ 0 ∧ x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] x'
have hex : ∃ (k : ℕ), x.coeff k ≠ 0
Tactic: have hex : ∃ k : ℕ, x.coeff k ≠ 0 := by
    by_contra! hall
    apply hx
    ext i
    simp only [hall, zero_coeff]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Domain (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
hx : x ≠ 0
hex : ∃ (k : ℕ), x.coeff k ≠ 0
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ x.coeff n ≠ 0) hex
⊢ ∃ (n : ℕ) (x' : 𝕎 R), x'.coeff 0 ≠ 0 ∧ x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] x'
have h : (x.shift n).coeff 0 ≠ 0 ∧ x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] (x.shift n)
Tactic: use n, x.shift n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Domain (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
hx : x ≠ 0
hex : ∃ (k : ℕ), x.coeff k ≠ 0
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ x.coeff n ≠ 0) hex
⊢ (x.shift n).coeff 0 ≠ 0 ∧ x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] (x.shift n)
have h : ∀ (i : ℕ) (hi : i < n), ¬¬x.coeff i = 0
Tactic: refine ⟨Nat.find_spec hex, eq_iterate_verschiebung fun i hi => not_not.mp ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Domain (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
hx : x ≠ 0
⊢ ∃ (n : ℕ) (x' : 𝕎 R), x'.coeff 0 ≠ 0 ∧ x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] x'
have have : ∃ (k : ℕ), x.coeff k ≠ 0
Tactic: classical
  have hex : ∃ k : ℕ, x.coeff k ≠ 0 := by
    by_contra! hall
    apply hx
    ext i
    simp only [hall, zero_coeff]
  let n := Nat.find hex
  use n, x.shift n
  refine ⟨Nat.find_spec hex, eq_iterate_verschiebung fun i hi => not_not.mp ?_⟩
  exact Nat.find_min hex hi
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Domain (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
hx : x ≠ 0
have : ∃ (k : ℕ), x.coeff k ≠ 0
⊢ ∃ (n : ℕ) (x' : 𝕎 R), x'.coeff 0 ≠ 0 ∧ x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] x'
have have₁ : ∀ (hex : ∃ (k : ℕ), x.coeff k ≠ 0), ∃ (n : ℕ) (x' : 𝕎 R), x'.coeff 0 ≠ 0 ∧ x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] x'
Tactic: classical
  have hex : ∃ k : ℕ, x.coeff k ≠ 0 := by
    by_contra! hall
    apply hx
    ext i
    simp only [hall, zero_coeff]
  let n := Nat.find hex
  use n, x.shift n
  refine ⟨Nat.find_spec hex, eq_iterate_verschiebung fun i hi => not_not.mp ?_⟩
  exact Nat.find_min hex hi
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Domain (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
hx : x ≠ 0
have : ∃ (k : ℕ), x.coeff k ≠ 0
have₁ :
  ∀ (hex : ∃ (k : ℕ), x.coeff k ≠ 0),
    ∃ (n : ℕ) (x' : 𝕎 R), x'.coeff 0 ≠ 0 ∧ x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] x'
have₂ : ∃ (k : ℕ), x.coeff k ≠ 0
have₃ have₄ have₅ :
  ∀ (hex : ∃ (k : ℕ), x.coeff k ≠ 0),
    ∃ (n : ℕ) (x' : 𝕎 R), x'.coeff 0 ≠ 0 ∧ x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] x'
⊢ ∃ (n : ℕ) (x' : 𝕎 R), x'.coeff 0 ≠ 0 ∧ x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] x'
have h : ∀ (hex : ∃ (k : ℕ), x.coeff k ≠ 0),
  let n := Nat.find (p := fun (n : ℕ) ↦ x.coeff n ≠ 0) hex;
  (x.shift n).coeff 0 ≠ 0 ∧ x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] (x.shift n)
Tactic: classical
  have hex : ∃ k : ℕ, x.coeff k ≠ 0 := by
    by_contra! hall
    apply hx
    ext i
    simp only [hall, zero_coeff]
  let n := Nat.find hex
  use n, x.shift n
  refine ⟨Nat.find_spec hex, eq_iterate_verschiebung fun i hi => not_not.mp ?_⟩
  exact Nat.find_min hex hi
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Domain (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
hx : x ≠ 0
have : ∃ (k : ℕ), x.coeff k ≠ 0
have₁ :
  ∀ (hex : ∃ (k : ℕ), x.coeff k ≠ 0),
    ∃ (n : ℕ) (x' : 𝕎 R), x'.coeff 0 ≠ 0 ∧ x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] x'
have₂ : ∃ (k : ℕ), x.coeff k ≠ 0
have₃ have₄ have₅ :
  ∀ (hex : ∃ (k : ℕ), x.coeff k ≠ 0),
    ∃ (n : ℕ) (x' : 𝕎 R), x'.coeff 0 ≠ 0 ∧ x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] x'
h :
  ∀ (hex : ∃ (k : ℕ), x.coeff k ≠ 0),
    let n := Nat.find (p := fun (n : ℕ) ↦ x.coeff n ≠ 0) hex;
    (x.shift n).coeff 0 ≠ 0 ∧ x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] (x.shift n)
⊢ ∃ (n : ℕ) (x' : 𝕎 R), x'.coeff 0 ≠ 0 ∧ x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] x'
have h₁ : ∀ (hex : ∃ (k : ℕ), x.coeff k ≠ 0),
  let n := Nat.find (p := fun (n : ℕ) ↦ x.coeff n ≠ 0) hex;
  ∀ (i : ℕ) (hi : i < n), ¬¬x.coeff i = 0
Tactic: classical
  have hex : ∃ k : ℕ, x.coeff k ≠ 0 := by
    by_contra! hall
    apply hx
    ext i
    simp only [hall, zero_coeff]
  let n := Nat.find hex
  use n, x.shift n
  refine ⟨Nat.find_spec hex, eq_iterate_verschiebung fun i hi => not_not.mp ?_⟩
  exact Nat.find_min hex hi
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Domain (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
inst_2 : NoZeroDivisors R
x y : 𝕎 R
⊢ x * y = 0 → x = 0 ∨ y = 0
have contrapose! : x ≠ 0 ∧ y ≠ 0 → x * y ≠ 0
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Domain (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
inst_2 : NoZeroDivisors R
x y : 𝕎 R
ha : x ≠ 0
hb : y ≠ 0
⊢ x * y ≠ 0
have rcases : ∀ (na : ℕ) (wa : 𝕎 R) (hwa0 : wa.coeff 0 ≠ 0) (ha : (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[na] wa ≠ 0),
  (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[na] wa * y ≠ 0
Tactic: rcases verschiebung_nonzero ha with ⟨na, wa, hwa0, rfl⟩
Cleared hypotheses: x, ha
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Domain (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
inst_2 : NoZeroDivisors R
y : 𝕎 R
hb : y ≠ 0
na : ℕ
wa : 𝕎 R
hwa0 : wa.coeff 0 ≠ 0
ha : (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[na] wa ≠ 0
⊢ (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[na] wa * y ≠ 0
have rcases : ∀ (nb : ℕ) (wb : 𝕎 R) (hwb0 : wb.coeff 0 ≠ 0) (hb : (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[nb] wb ≠ 0),
  (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[na] wa * (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[nb] wb ≠ 0
Tactic: rcases verschiebung_nonzero hb with ⟨nb, wb, hwb0, rfl⟩
Cleared hypotheses: y, hb
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Domain (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
inst_2 : NoZeroDivisors R
na : ℕ
wa : 𝕎 R
hwa0 : wa.coeff 0 ≠ 0
ha : (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[na] wa ≠ 0
nb : ℕ
wb : 𝕎 R
hwb0 : wb.coeff 0 ≠ 0
hb : (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[nb] wb ≠ 0
⊢ (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[na] wa * (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[nb] wb ≠ 0
have refine : Ne.{u_1 + 1} (α := R)
  ((fun (x : 𝕎 R) ↦ x.coeff (na + nb))
    ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[na] wa * (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[nb] wb))
  ((fun (x : 𝕎 R) ↦ x.coeff (na + nb)) 0)
Tactic: refine ne_of_apply_ne (fun x => x.coeff (na + nb)) ?_
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Domain (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
inst_2 : NoZeroDivisors R
na : ℕ
wa : 𝕎 R
hwa0 : wa.coeff 0 ≠ 0
ha : (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[na] wa ≠ 0
nb : ℕ
wb : 𝕎 R
hwb0 : wb.coeff 0 ≠ 0
hb : (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[nb] wb ≠ 0
⊢ ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[na] wa * (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[nb] wb).coeff (na + nb) ≠
    coeff (p := p) 0 (na + nb)
have rw : wa.coeff 0 ^ p ^ nb * wb.coeff 0 ^ p ^ na ≠ 0
Tactic: rw [iterate_verschiebung_mul_coeff, zero_coeff]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ Eq (α := MvPolynomial ℕ ℚ)
    ((bind₁ fun (n : ℕ) ↦
            (bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ)
              (xInTermsOfW p ℚ n) :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ)
        (wittPolynomial p ℚ n) :
      MvPolynomial ℕ ℚ)
    (wittPolynomial p ℚ (n + 1) : MvPolynomial ℕ ℚ)
have rw : Eq (α := MvPolynomial ℕ ℚ)
  ((bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ)
      ((bind₁ (xInTermsOfW p ℚ) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (wittPolynomial p ℚ n)) :
    MvPolynomial ℕ ℚ)
  (wittPolynomial p ℚ (n + 1) : MvPolynomial ℕ ℚ)
Tactic: rw [← bind₁_bind₁, bind₁_xInTermsOfW_wittPolynomial, bind₁_X_right, Function.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
rw :
  Eq (α := MvPolynomial ℕ ℚ)
    ((bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ)
        ((bind₁ (xInTermsOfW p ℚ) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (wittPolynomial p ℚ n)) :
      MvPolynomial ℕ ℚ)
    (wittPolynomial p ℚ (n + 1) : MvPolynomial ℕ ℚ)
⊢ Eq (α := MvPolynomial ℕ ℚ)
    ((bind₁ fun (n : ℕ) ↦
            (bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ)
              (xInTermsOfW p ℚ n) :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ)
        (wittPolynomial p ℚ n) :
      MvPolynomial ℕ ℚ)
    (wittPolynomial p ℚ (n + 1) : MvPolynomial ℕ ℚ)
have rw₁ : Eq (α := MvPolynomial ℕ ℚ)
  ((bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (X n) :
    MvPolynomial ℕ ℚ)
  (wittPolynomial p ℚ (n + 1) : MvPolynomial ℕ ℚ)
Tactic: rw [← bind₁_bind₁, bind₁_xInTermsOfW_wittPolynomial, bind₁_X_right, Function.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
rw :
  Eq (α := MvPolynomial ℕ ℚ)
    ((bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ)
        ((bind₁ (xInTermsOfW p ℚ) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (wittPolynomial p ℚ n)) :
      MvPolynomial ℕ ℚ)
    (wittPolynomial p ℚ (n + 1) : MvPolynomial ℕ ℚ)
rw₁ :
  Eq (α := MvPolynomial ℕ ℚ)
    ((bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (X n) :
      MvPolynomial ℕ ℚ)
    (wittPolynomial p ℚ (n + 1) : MvPolynomial ℕ ℚ)
⊢ Eq (α := MvPolynomial ℕ ℚ)
    ((bind₁ fun (n : ℕ) ↦
            (bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ)
              (xInTermsOfW p ℚ n) :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ)
        (wittPolynomial p ℚ n) :
      MvPolynomial ℕ ℚ)
    (wittPolynomial p ℚ (n + 1) : MvPolynomial ℕ ℚ)
have rw₂ : Eq (α := MvPolynomial ℕ ℚ) ((wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) n) (wittPolynomial p ℚ (n + 1))
Tactic: rw [← bind₁_bind₁, bind₁_xInTermsOfW_wittPolynomial, bind₁_X_right, Function.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
rw :
  Eq (α := MvPolynomial ℕ ℚ)
    ((bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ)
        ((bind₁ (xInTermsOfW p ℚ) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (wittPolynomial p ℚ n)) :
      MvPolynomial ℕ ℚ)
    (wittPolynomial p ℚ (n + 1) : MvPolynomial ℕ ℚ)
rw₁ :
  Eq (α := MvPolynomial ℕ ℚ)
    ((bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (X n) :
      MvPolynomial ℕ ℚ)
    (wittPolynomial p ℚ (n + 1) : MvPolynomial ℕ ℚ)
rw₂ : Eq (α := MvPolynomial ℕ ℚ) ((wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) n) (wittPolynomial p ℚ (n + 1))
⊢ Eq (α := MvPolynomial ℕ ℚ)
    ((bind₁ fun (n : ℕ) ↦
            (bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ)
              (xInTermsOfW p ℚ n) :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ)
        (wittPolynomial p ℚ n) :
      MvPolynomial ℕ ℚ)
    (wittPolynomial p ℚ (n + 1) : MvPolynomial ℕ ℚ)
have rw₃ : Eq (α := MvPolynomial ℕ ℚ) (wittPolynomial p ℚ (n + 1)) (wittPolynomial p ℚ (n + 1))
Tactic: rw [← bind₁_bind₁, bind₁_xInTermsOfW_wittPolynomial, bind₁_X_right, Function.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p n : ℕ
⊢ frobeniusPolyAux p n =
    HSub.hSub (α := MvPolynomial ℕ ℤ) (X (n + 1))
      (∑ i ∈ range n,
        ∑ j ∈ range (p ^ (n - i)),
          HPow.hPow (α := MvPolynomial ℕ ℤ) (X i) p ^ (p ^ (n - i) - (j + 1)) * frobeniusPolyAux p i ^ (j + 1) *
            (C : (a : ℤ) → MvPolynomial ℕ ℤ)
              (↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1))) : ℤ))
have rw : HSub.hSub (α := MvPolynomial ℕ ℤ) (X (n + 1))
    (∑ i : Fin n,
      have x := sorry;
      ∑ j ∈ range (p ^ (n - (↑i : ℕ))),
        HPow.hPow (α := MvPolynomial ℕ ℤ) (X (↑i : ℕ)) p ^ (p ^ (n - (↑i : ℕ)) - (j + 1)) *
            frobeniusPolyAux p (↑i : ℕ) ^ (j + 1) *
          (C : (a : ℤ) → MvPolynomial ℕ ℤ)
            (↑((p ^ (n - (↑i : ℕ))).choose (j + 1) / p ^ (n - (↑i : ℕ) - v p (j + 1)) * p ^ (j - v p (j + 1))) : ℤ)) =
  HSub.hSub (α := MvPolynomial ℕ ℤ) (X (n + 1))
    (∑ i ∈ range n,
      ∑ j ∈ range (p ^ (n - i)),
        HPow.hPow (α := MvPolynomial ℕ ℤ) (X i) p ^ (p ^ (n - i) - (j + 1)) * frobeniusPolyAux p i ^ (j + 1) *
          (C : (a : ℤ) → MvPolynomial ℕ ℤ)
            (↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1))) : ℤ))
Tactic: rw [frobeniusPolyAux, ← Fin.sum_univ_eq_sum_range]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p n : ℕ
rw :
  HSub.hSub (α := MvPolynomial ℕ ℤ) (X (n + 1))
      (∑ i : Fin n,
        have x := ⋯;
        ∑ j ∈ range (p ^ (n - (↑i : ℕ))),
          HPow.hPow (α := MvPolynomial ℕ ℤ) (X (↑i : ℕ)) p ^ (p ^ (n - (↑i : ℕ)) - (j + 1)) *
              frobeniusPolyAux p (↑i : ℕ) ^ (j + 1) *
            (C : (a : ℤ) → MvPolynomial ℕ ℤ)
              (↑((p ^ (n - (↑i : ℕ))).choose (j + 1) / p ^ (n - (↑i : ℕ) - v p (j + 1)) * p ^ (j - v p (j + 1))) : ℤ)) =
    HSub.hSub (α := MvPolynomial ℕ ℤ) (X (n + 1))
      (∑ i ∈ range n,
        ∑ j ∈ range (p ^ (n - i)),
          HPow.hPow (α := MvPolynomial ℕ ℤ) (X i) p ^ (p ^ (n - i) - (j + 1)) * frobeniusPolyAux p i ^ (j + 1) *
            (C : (a : ℤ) → MvPolynomial ℕ ℤ)
              (↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1))) : ℤ))
⊢ frobeniusPolyAux p n =
    HSub.hSub (α := MvPolynomial ℕ ℤ) (X (n + 1))
      (∑ i ∈ range n,
        ∑ j ∈ range (p ^ (n - i)),
          HPow.hPow (α := MvPolynomial ℕ ℤ) (X i) p ^ (p ^ (n - i) - (j + 1)) * frobeniusPolyAux p i ^ (j + 1) *
            (C : (a : ℤ) → MvPolynomial ℕ ℤ)
              (↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1))) : ℤ))
have rw₁ : HSub.hSub (α := MvPolynomial ℕ ℤ) (X (n + 1))
    (∑ i : Fin n,
      have x := sorry;
      ∑ j ∈ range (p ^ (n - (↑i : ℕ))),
        HPow.hPow (α := MvPolynomial ℕ ℤ) (X (↑i : ℕ)) p ^ (p ^ (n - (↑i : ℕ)) - (j + 1)) *
            frobeniusPolyAux p (↑i : ℕ) ^ (j + 1) *
          (C : (a : ℤ) → MvPolynomial ℕ ℤ)
            (↑((p ^ (n - (↑i : ℕ))).choose (j + 1) / p ^ (n - (↑i : ℕ) - v p (j + 1)) * p ^ (j - v p (j + 1))) : ℤ)) =
  HSub.hSub (α := MvPolynomial ℕ ℤ) (X (n + 1))
    (∑ i : Fin n,
      ∑ j ∈ range (p ^ (n - (↑i : ℕ))),
        HPow.hPow (α := MvPolynomial ℕ ℤ) (X (↑i : ℕ)) p ^ (p ^ (n - (↑i : ℕ)) - (j + 1)) *
            frobeniusPolyAux p (↑i : ℕ) ^ (j + 1) *
          (C : (a : ℤ) → MvPolynomial ℕ ℤ)
            (↑((p ^ (n - (↑i : ℕ))).choose (j + 1) / p ^ (n - (↑i : ℕ) - v p (j + 1)) * p ^ (j - v p (j + 1))) : ℤ))
Tactic: rw [frobeniusPolyAux, ← Fin.sum_univ_eq_sum_range]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n j : ℕ
hj : j < p ^ n
⊢ p ^ (n - v p (j + 1)) ∣ (p ^ n).choose (j + 1)
have hk : (↑(n - v p (j + 1)) : ℕ∞) ≤ emultiplicity p ((p ^ n).choose (j + 1))
Tactic: apply pow_dvd_of_le_emultiplicity