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 : CommRing k
inst_1 : CharP k p
a : kˣ
A : 𝕎 k
hA : A.coeff 0 = (↑a : k)
n : ℕ
h : (A * { coeff := inverseCoeff a A : 𝕎 k }).coeff n = coeff (p := p) 1 n
H_coeff : k :=
  A.coeff (n + 1) * (↑(a⁻¹ ^ p ^ (n + 1)) : k) +
    nthRemainder p n (truncateFun (n + 1) A) fun (i : Fin (n + 1)) ↦ inverseCoeff a A (↑i : ℕ)
H : (↑(a ^ p ^ (n + 1)) : k) * (↑(a ^ p ^ (n + 1))⁻¹ : k) = 1
⊢ (A * { coeff := inverseCoeff a A : 𝕎 k }).coeff (n + 1) + -H_coeff * 1 -
      (coeff (p := p) 1 (n + 1) + -H_coeff * ((↑(a ^ p ^ (n + 1)) : k) * (↑(a ^ p ^ (n + 1))⁻¹ : k))) =
    0
have ha : (↑a : k) ^ p ^ (n + 1) = (↑(a ^ p ^ (n + 1)) : k)
Tactic: have ha : (a : k) ^ p ^ (n + 1) = ↑(a ^ p ^ (n + 1)) := by norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.DiscreteValuationRing (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
a : kˣ
A : 𝕎 k
hA : A.coeff 0 = (↑a : k)
n : ℕ
h : (A * { coeff := inverseCoeff a A : 𝕎 k }).coeff n = coeff (p := p) 1 n
H_coeff : k :=
  A.coeff (n + 1) * (↑(a⁻¹ ^ p ^ (n + 1)) : k) +
    nthRemainder p n (truncateFun (n + 1) A) fun (i : Fin (n + 1)) ↦ inverseCoeff a A (↑i : ℕ)
H : (↑(a ^ p ^ (n + 1)) : k) * (↑(a ^ p ^ (n + 1))⁻¹ : k) = 1
ha : (↑a : k) ^ p ^ (n + 1) = (↑(a ^ p ^ (n + 1)) : k)
⊢ (↑a⁻¹ : k) ^ p ^ (n + 1) = (↑(a ^ p ^ (n + 1))⁻¹ : k)
have norm_cast : a⁻¹ ^ p ^ (n + 1) = (a ^ p ^ (n + 1))⁻¹
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.DiscreteValuationRing (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
a : kˣ
A : 𝕎 k
hA : A.coeff 0 = (↑a : k)
n : ℕ
h : (A * { coeff := inverseCoeff a A : 𝕎 k }).coeff n = coeff (p := p) 1 n
H_coeff : k :=
  A.coeff (n + 1) * (↑(a⁻¹ ^ p ^ (n + 1)) : k) +
    nthRemainder p n (truncateFun (n + 1) A) fun (i : Fin (n + 1)) ↦ inverseCoeff a A (↑i : ℕ)
H : (↑(a ^ p ^ (n + 1)) : k) * (↑(a ^ p ^ (n + 1))⁻¹ : k) = 1
ha : (↑a : k) ^ p ^ (n + 1) = (↑(a ^ p ^ (n + 1)) : k)
⊢ (A * { coeff := inverseCoeff a A : 𝕎 k }).coeff (n + 1) + -H_coeff * 1 -
      (coeff (p := p) 1 (n + 1) + -H_coeff * ((↑(a ^ p ^ (n + 1)) : k) * (↑(a ^ p ^ (n + 1))⁻¹ : k))) =
    0
have ha_inv : (↑a⁻¹ : k) ^ p ^ (n + 1) = (↑(a ^ p ^ (n + 1))⁻¹ : k)
Tactic: have ha_inv : (↑a⁻¹ : k) ^ p ^ (n + 1) = ↑(a ^ p ^ (n + 1))⁻¹ := by norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.DiscreteValuationRing (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
a : kˣ
A : 𝕎 k
hA : A.coeff 0 = (↑a : k)
n : ℕ
h : (A * { coeff := inverseCoeff a A : 𝕎 k }).coeff n = coeff (p := p) 1 n
H_coeff : k :=
  A.coeff (n + 1) * (↑(a⁻¹ ^ p ^ (n + 1)) : k) +
    nthRemainder p n (truncateFun (n + 1) A) fun (i : Fin (n + 1)) ↦ inverseCoeff a A (↑i : ℕ)
H : (↑(a ^ p ^ (n + 1)) : k) * (↑(a ^ p ^ (n + 1))⁻¹ : k) = 1
ha : (↑a : k) ^ p ^ (n + 1) = (↑(a ^ p ^ (n + 1)) : k)
ha_inv : (↑a⁻¹ : k) ^ p ^ (n + 1) = (↑(a ^ p ^ (n + 1))⁻¹ : k)
⊢ (A * { coeff := inverseCoeff a A : 𝕎 k }).coeff (n + 1) + -H_coeff * 1 -
      (coeff (p := p) 1 (n + 1) + -H_coeff * ((↑(a ^ p ^ (n + 1)) : k) * (↑(a ^ p ^ (n + 1))⁻¹ : k))) =
    0
have a₁ : A.coeff (n + 1) * (↑(a ^ p ^ (n + 1))⁻¹ : k) +
          -(↑(a ^ p ^ (n + 1))⁻¹ : k) *
              (A.coeff (n + 1) * (↑(a ^ p ^ (n + 1))⁻¹ : k) +
                nthRemainder p n (truncateFun (n + 1) A) fun (i : Fin (n + 1)) ↦ inverseCoeff a A (↑i : ℕ)) *
            (↑(a ^ p ^ (n + 1)) : k) +
        nthRemainder p n (truncateFun (n + 1) A) (truncateFun (n + 1) { coeff := inverseCoeff a A : 𝕎 k }) +
      -H_coeff * 1 -
    (0 + -H_coeff * ((↑(a ^ p ^ (n + 1)) : k) * (↑(a ^ p ^ (n + 1))⁻¹ : k))) =
  0
Tactic: simp only [nthRemainder_spec, inverseCoeff, succNthValUnits, hA,
      one_coeff_eq_of_pos, Nat.succ_pos', ha_inv, ha, inv_pow]
-- 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
x : 𝕎 k
hx : x.coeff 0 ≠ 0
y : kˣ := Units.mk0 (x.coeff 0) hx
⊢ IsUnit x
have hy : x.coeff 0 = (↑y : k)
Tactic: have hy : x.coeff 0 = y := rfl
-- 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
⊢ Irreducible.{u_1} (M := 𝕎 k) (↑p : 𝕎 k)
have hp₁ : ¬IsUnit.{u_1} (M := 𝕎 k) (↑p : 𝕎 k)
Tactic: have hp : ¬IsUnit (p : 𝕎 k) := by
    intro hp
    simpa only [constantCoeff_apply, coeff_p_zero, not_isUnit_zero] using
      (constantCoeff : WittVector p k →+* _).isUnit_map hp
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.DiscreteValuationRing (goal)
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)
⊢ Irreducible.{u_1} (M := 𝕎 k) (↑p : 𝕎 k)
have refine : ∀ (a b : 𝕎 k) (hab : (↑p : 𝕎 k) = a * b), IsUnit a ∨ IsUnit b
Tactic: refine ⟨hp, fun a b hab => ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.DiscreteValuationRing (goal)
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 b : 𝕎 k
hab : (↑p : 𝕎 k) = a * b
⊢ a ≠ 0 ∧ b ≠ 0
have rw : a * b ≠ 0
Tactic: rw [← mul_ne_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.DiscreteValuationRing (hypothesis)
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 b : 𝕎 k
hab : (↑p : 𝕎 k) = a * b
h : a * b = 0
⊢ False
have hab₁ : Eq.{u_1 + 1} (α := 𝕎 k) (↑p : 𝕎 k) 0
Tactic: rw [h] at hab
Cleared hypotheses: hab, h
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.DiscreteValuationRing (hypothesis)
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 b : 𝕎 k
hab : (↑p : 𝕎 k) = a * b
⊢ IsUnit a ∨ IsUnit b
have ha0 : a ≠ 0
Tactic: obtain ⟨ha0, hb0⟩ : a ≠ 0 ∧ b ≠ 0 := by
    rw [← mul_ne_zero_iff]; intro h; rw [h] at hab; exact p_nonzero p k hab
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.DiscreteValuationRing (hypothesis)
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 b : 𝕎 k
hab : (↑p : 𝕎 k) = a * b
ha0 : a ≠ 0
⊢ IsUnit a ∨ IsUnit b
have hb0 : b ≠ 0
Tactic: obtain ⟨ha0, hb0⟩ : a ≠ 0 ∧ b ≠ 0 := by
    rw [← mul_ne_zero_iff]; intro h; rw [h] at hab; exact p_nonzero p k hab
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.DiscreteValuationRing (goal)
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 b : 𝕎 k
hab : (↑p : 𝕎 k) = a * b
ha0 : a ≠ 0
hb0 : b ≠ 0
⊢ IsUnit a ∨ IsUnit b
have obtain : ∀ (m : ℕ) (a : 𝕎 k) (ha : a.coeff 0 ≠ 0) (hab : (↑p : 𝕎 k) = (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] a * b)
  (ha0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] a ≠ 0), IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] a) ∨ IsUnit b
Tactic: obtain ⟨m, a, ha, rfl⟩ := verschiebung_nonzero ha0
Cleared hypotheses: a, hab, ha0
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.DiscreteValuationRing (goal)
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)
b : 𝕎 k
hb0 : b ≠ 0
m : ℕ
a : 𝕎 k
ha : a.coeff 0 ≠ 0
hab : (↑p : 𝕎 k) = (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] a * b
ha0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] a ≠ 0
⊢ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] a) ∨ IsUnit b
have obtain : ∀ (n : ℕ) (b : 𝕎 k) (hb : b.coeff 0 ≠ 0) (hb0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] b ≠ 0)
  (hab : (↑p : 𝕎 k) = (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] a * (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] b),
  IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] a) ∨ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] b)
Tactic: obtain ⟨n, b, hb, rfl⟩ := verschiebung_nonzero hb0
Cleared hypotheses: b, hb0, hab
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.DiscreteValuationRing (goal)
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)
m : ℕ
a : 𝕎 k
ha : a.coeff 0 ≠ 0
ha0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] a ≠ 0
n : ℕ
b : 𝕎 k
hb : b.coeff 0 ≠ 0
hb0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] b ≠ 0
hab : (↑p : 𝕎 k) = (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] a * (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] b
⊢ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] a) ∨ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] b)
have zero : ∀ (ha0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[0] a ≠ 0)
  (hab : (↑p : 𝕎 k) = (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[0] a * (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] b),
  IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[0] a) ∨ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] b)
Tactic: cases m
Cleared hypotheses: m, ha0, hab
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.DiscreteValuationRing (goal)
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)
m : ℕ
a : 𝕎 k
ha : a.coeff 0 ≠ 0
ha0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] a ≠ 0
n : ℕ
b : 𝕎 k
hb : b.coeff 0 ≠ 0
hb0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] b ≠ 0
hab : (↑p : 𝕎 k) = (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] a * (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] b
zero :
  ∀ (ha0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[0] a ≠ 0)
    (hab : (↑p : 𝕎 k) = (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[0] a * (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] b),
    IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[0] a) ∨ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] b)
⊢ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] a) ∨ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] b)
have succ : ∀ (n_1 : ℕ) (ha0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1] a ≠ 0)
  (hab : (↑p : 𝕎 k) = (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1] a * (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] b),
  IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1] a) ∨ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] b)
Tactic: cases m
Cleared hypotheses: m, ha0, hab
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.DiscreteValuationRing (goal)
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
n : ℕ
b : 𝕎 k
hb : b.coeff 0 ≠ 0
hb0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] b ≠ 0
n_1 : ℕ
ha0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1] a ≠ 0
hab : (↑p : 𝕎 k) = (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1] a * (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] b
⊢ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1] a) ∨ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] b)
have succ : ∀ (hb0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[0] b ≠ 0)
  (hab : (↑p : 𝕎 k) = (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1] a * (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[0] b),
  IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1] a) ∨ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[0] b)
Tactic: rcases n with - | n
Cleared hypotheses: n, hb0, hab
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.DiscreteValuationRing (goal)
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
n : ℕ
b : 𝕎 k
hb : b.coeff 0 ≠ 0
hb0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] b ≠ 0
n_1 : ℕ
ha0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1] a ≠ 0
hab : (↑p : 𝕎 k) = (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1] a * (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] b
succ :
  ∀ (hb0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[0] b ≠ 0)
    (hab : (↑p : 𝕎 k) = (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1] a * (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[0] b),
    IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1] a) ∨ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[0] b)
⊢ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1] a) ∨ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] b)
have succ₁ : ∀ (n : ℕ) (hb0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n + 1] b ≠ 0)
  (hab : (↑p : 𝕎 k) = (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1] a * (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n + 1] b),
  IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1] a) ∨ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n + 1] b)
Tactic: rcases n with - | n
Cleared hypotheses: n, hb0, hab
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.DiscreteValuationRing (hypothesis)
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 : (↑p : 𝕎 k) = (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1] a * (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n + 1] b
⊢ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1] a) ∨ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n + 1] b)
have hab₁ : (↑p : 𝕎 k) =
  (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1 + (n + 1)]
    ((⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[n + 1] a * (⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1] b)
Tactic: rw [iterate_verschiebung_mul] at hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.DiscreteValuationRing (hypothesis)
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 :
  (↑p : 𝕎 k) =
    (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1 + (n + 1)]
      ((⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[n + 1] a * (⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1] b)
⊢ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1] a) ∨ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n + 1] b)
have 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
Tactic: apply_fun fun x => coeff x 1 at hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.DiscreteValuationRing (hypothesis)
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
⊢ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1] a) ∨ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n + 1] b)
have hab₁ : 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
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.DiscreteValuationRing (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
a : 𝕎 k
ha : a ≠ 0
⊢ ∃ (m : ℕ) (b : 𝕎 k), b.coeff 0 ≠ 0 ∧ a = HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * b
have 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
Tactic: obtain ⟨m, c, hc, hcm⟩ := WittVector.verschiebung_nonzero ha
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.DiscreteValuationRing (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
a : 𝕎 k
ha : a ≠ 0
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
have 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
Tactic: obtain ⟨b, rfl⟩ := (frobenius_bijective p k).surjective.iterate m c
Cleared hypotheses: c, hc, hcm
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.DiscreteValuationRing (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
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)
⊢ ∃ (m : ℕ) (b : 𝕎 k), b.coeff 0 ≠ 0 ∧ a = HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * b
have hc₁ : b.coeff 0 ^ p ^ m ≠ 0
Tactic: rw [WittVector.iterate_frobenius_coeff] at hc
Cleared hypotheses: hc, hcm
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.DiscreteValuationRing (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
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)
⊢ ∃ (m : ℕ) (b : 𝕎 k), b.coeff 0 ≠ 0 ∧ a = HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * b
have 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
Tactic: have := congr_fun (WittVector.verschiebung_frobenius_comm.comp_iterate m) b
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.DiscreteValuationRing (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
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)
⊢ ∃ (m : ℕ) (b : 𝕎 k), b.coeff 0 ≠ 0 ∧ a = HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * b
have hcm₁ : a = (Function.comp (β := 𝕎 k) (⇑verschiebung : (a : 𝕎 k) → 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k))^[m] b
Tactic: rw [← this] at hcm
Cleared hypotheses: hcm, this
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.DiscreteValuationRing (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
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
have refine_1 : b.coeff 0 ≠ 0
Tactic: refine ⟨m, b, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.DiscreteValuationRing (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
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
⊢ ∃ (m : ℕ) (b : 𝕎 k), b.coeff 0 ≠ 0 ∧ a = HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * b
have refine_2 : a = HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * b
Tactic: refine ⟨m, b, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.DiscreteValuationRing (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
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)
⊢ b.coeff 0 ≠ 0
have refine_1 : ∀ (hc : b.coeff 0 = 0), b.coeff 0 ^ p ^ m = 0
Tactic: contrapose hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.DiscreteValuationRing (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
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 = HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * b
have refine_2 : a = (fun (x : 𝕎 k) ↦ (↑p : 𝕎 k) * x)^[m] b
Tactic: simp_rw [← mul_left_iterate (p : 𝕎 k) m]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.DiscreteValuationRing (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
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 = (fun (x : 𝕎 k) ↦ (↑p : 𝕎 k) * x)^[m] b
have h : Eq.{u_1 + 1} (α := 𝕎 k → 𝕎 k) (fun (x : 𝕎 k) ↦ (↑p : 𝕎 k) * x)
  (Function.comp (β := 𝕎 k) (⇑verschiebung : (a : 𝕎 k) → 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k))
Tactic: convert! hcm using 2
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.DiscreteValuationRing (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
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)
⊢ Eq.{u_1 + 1} (α := 𝕎 k → 𝕎 k) (fun (x : 𝕎 k) ↦ (↑p : 𝕎 k) * x)
    (Function.comp (β := 𝕎 k) (⇑verschiebung : (a : 𝕎 k) → 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k))
have h : ∀ (x : 𝕎 k),
  (↑p : 𝕎 k) * x = Function.comp (β := 𝕎 k) (⇑verschiebung : (a : 𝕎 k) → 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k) x
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.DiscreteValuationRing (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
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
⊢ (↑p : 𝕎 k) * x = Function.comp (β := 𝕎 k) (⇑verschiebung : (a : 𝕎 k) → 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k) x
have 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)
Tactic: rw [mul_comm, ← WittVector.verschiebung_frobenius x]
-- 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
a : 𝕎 k
ha : a ≠ 0
⊢ ∃ (m : ℕ) (b : (𝕎 k)ˣ), a = HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * (↑b : 𝕎 k)
have 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)
Tactic: obtain ⟨m, b, h₁, h₂⟩ := exists_eq_pow_p_mul a ha