[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : kˣ
A : 𝕎 k
hA : coeff A 0 = ↑a
⊢ A * { coeff := inverseCoeff a A } = 1
[PROOFSTEP]
ext n
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : kˣ
A : 𝕎 k
hA : coeff A 0 = ↑a
n : ℕ
⊢ coeff (A * { coeff := inverseCoeff a A }) n = coeff 1 n
[PROOFSTEP]
induction' n with n _
[GOAL]
case h.zero
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : kˣ
A : 𝕎 k
hA : coeff A 0 = ↑a
⊢ coeff (A * { coeff := inverseCoeff a A }) Nat.zero = coeff 1 Nat.zero
[PROOFSTEP]
simp [WittVector.mul_coeff_zero, inverseCoeff, hA]
[GOAL]
case h.succ
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : kˣ
A : 𝕎 k
hA : coeff A 0 = ↑a
n : ℕ
n_ih✝ : coeff (A * { coeff := inverseCoeff a A }) n = coeff 1 n
⊢ coeff (A * { coeff := inverseCoeff a A }) (Nat.succ n) = coeff 1 (Nat.succ n)
[PROOFSTEP]
let H_coeff :=
  A.coeff (n + 1) * ↑(a⁻¹ ^ p ^ (n + 1)) +
    nthRemainder p n (truncateFun (n + 1) A) fun i : Fin (n + 1) => inverseCoeff a A i
[GOAL]
case h.succ
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : kˣ
A : 𝕎 k
hA : coeff A 0 = ↑a
n : ℕ
n_ih✝ : coeff (A * { coeff := inverseCoeff a A }) n = coeff 1 n
H_coeff : k :=
  coeff A (n + 1) * ↑(a⁻¹ ^ p ^ (n + 1)) + nthRemainder p n (truncateFun (n + 1) A) fun i => inverseCoeff a A ↑i
⊢ coeff (A * { coeff := inverseCoeff a A }) (Nat.succ n) = coeff 1 (Nat.succ n)
[PROOFSTEP]
have H := Units.mul_inv (a ^ p ^ (n + 1))
[GOAL]
case h.succ
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : kˣ
A : 𝕎 k
hA : coeff A 0 = ↑a
n : ℕ
n_ih✝ : coeff (A * { coeff := inverseCoeff a A }) n = coeff 1 n
H_coeff : k :=
  coeff A (n + 1) * ↑(a⁻¹ ^ p ^ (n + 1)) + nthRemainder p n (truncateFun (n + 1) A) fun i => inverseCoeff a A ↑i
H : ↑(a ^ p ^ (n + 1)) * ↑(a ^ p ^ (n + 1))⁻¹ = 1
⊢ coeff (A * { coeff := inverseCoeff a A }) (Nat.succ n) = coeff 1 (Nat.succ n)
[PROOFSTEP]
linear_combination (norm := skip) -H_coeff * H
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : kˣ
A : 𝕎 k
hA : coeff A 0 = ↑a
n : ℕ
n_ih✝ : coeff (A * { coeff := inverseCoeff a A }) n = coeff 1 n
H_coeff : k :=
  coeff A (n + 1) * ↑(a⁻¹ ^ p ^ (n + 1)) + nthRemainder p n (truncateFun (n + 1) A) fun i => inverseCoeff a A ↑i
H : ↑(a ^ p ^ (n + 1)) * ↑(a ^ p ^ (n + 1))⁻¹ = 1
⊢ coeff (A * { coeff := inverseCoeff a A }) (Nat.succ n) - coeff 1 (Nat.succ n) -
      (-H_coeff * (↑(a ^ p ^ (n + 1)) * ↑(a ^ p ^ (n + 1))⁻¹) - -H_coeff * 1) =
    0
[PROOFSTEP]
skip
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : kˣ
A : 𝕎 k
hA : coeff A 0 = ↑a
n : ℕ
n_ih✝ : coeff (A * { coeff := inverseCoeff a A }) n = coeff 1 n
H_coeff : k :=
  coeff A (n + 1) * ↑(a⁻¹ ^ p ^ (n + 1)) + nthRemainder p n (truncateFun (n + 1) A) fun i => inverseCoeff a A ↑i
H : ↑(a ^ p ^ (n + 1)) * ↑(a ^ p ^ (n + 1))⁻¹ = 1
⊢ coeff (A * { coeff := inverseCoeff a A }) (Nat.succ n) - coeff 1 (Nat.succ n) -
      (-H_coeff * (↑(a ^ p ^ (n + 1)) * ↑(a ^ p ^ (n + 1))⁻¹) - -H_coeff * 1) =
    0
[PROOFSTEP]
have ha : (a : k) ^ p ^ (n + 1) = ↑(a ^ p ^ (n + 1)) := by norm_cast
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : kˣ
A : 𝕎 k
hA : coeff A 0 = ↑a
n : ℕ
n_ih✝ : coeff (A * { coeff := inverseCoeff a A }) n = coeff 1 n
H_coeff : k :=
  coeff A (n + 1) * ↑(a⁻¹ ^ p ^ (n + 1)) + nthRemainder p n (truncateFun (n + 1) A) fun i => inverseCoeff a A ↑i
H : ↑(a ^ p ^ (n + 1)) * ↑(a ^ p ^ (n + 1))⁻¹ = 1
⊢ ↑a ^ p ^ (n + 1) = ↑(a ^ p ^ (n + 1))
[PROOFSTEP]
norm_cast
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : kˣ
A : 𝕎 k
hA : coeff A 0 = ↑a
n : ℕ
n_ih✝ : coeff (A * { coeff := inverseCoeff a A }) n = coeff 1 n
H_coeff : k :=
  coeff A (n + 1) * ↑(a⁻¹ ^ p ^ (n + 1)) + nthRemainder p n (truncateFun (n + 1) A) fun i => inverseCoeff a A ↑i
H : ↑(a ^ p ^ (n + 1)) * ↑(a ^ p ^ (n + 1))⁻¹ = 1
ha : ↑a ^ p ^ (n + 1) = ↑(a ^ p ^ (n + 1))
⊢ coeff (A * { coeff := inverseCoeff a A }) (Nat.succ n) - coeff 1 (Nat.succ n) -
      (-H_coeff * (↑(a ^ p ^ (n + 1)) * ↑(a ^ p ^ (n + 1))⁻¹) - -H_coeff * 1) =
    0
[PROOFSTEP]
have ha_inv : (↑a⁻¹ : k) ^ p ^ (n + 1) = ↑(a ^ p ^ (n + 1))⁻¹ := by norm_cast; norm_num
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : kˣ
A : 𝕎 k
hA : coeff A 0 = ↑a
n : ℕ
n_ih✝ : coeff (A * { coeff := inverseCoeff a A }) n = coeff 1 n
H_coeff : k :=
  coeff A (n + 1) * ↑(a⁻¹ ^ p ^ (n + 1)) + nthRemainder p n (truncateFun (n + 1) A) fun i => inverseCoeff a A ↑i
H : ↑(a ^ p ^ (n + 1)) * ↑(a ^ p ^ (n + 1))⁻¹ = 1
ha : ↑a ^ p ^ (n + 1) = ↑(a ^ p ^ (n + 1))
⊢ ↑a⁻¹ ^ p ^ (n + 1) = ↑(a ^ p ^ (n + 1))⁻¹
[PROOFSTEP]
norm_cast
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : kˣ
A : 𝕎 k
hA : coeff A 0 = ↑a
n : ℕ
n_ih✝ : coeff (A * { coeff := inverseCoeff a A }) n = coeff 1 n
H_coeff : k :=
  coeff A (n + 1) * ↑(a⁻¹ ^ p ^ (n + 1)) + nthRemainder p n (truncateFun (n + 1) A) fun i => inverseCoeff a A ↑i
H : ↑(a ^ p ^ (n + 1)) * ↑(a ^ p ^ (n + 1))⁻¹ = 1
ha : ↑a ^ p ^ (n + 1) = ↑(a ^ p ^ (n + 1))
⊢ a⁻¹ ^ p ^ (n + 1) = (a ^ p ^ (n + 1))⁻¹
[PROOFSTEP]
norm_num
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : kˣ
A : 𝕎 k
hA : coeff A 0 = ↑a
n : ℕ
n_ih✝ : coeff (A * { coeff := inverseCoeff a A }) n = coeff 1 n
H_coeff : k :=
  coeff A (n + 1) * ↑(a⁻¹ ^ p ^ (n + 1)) + nthRemainder p n (truncateFun (n + 1) A) fun i => inverseCoeff a A ↑i
H : ↑(a ^ p ^ (n + 1)) * ↑(a ^ p ^ (n + 1))⁻¹ = 1
ha : ↑a ^ p ^ (n + 1) = ↑(a ^ p ^ (n + 1))
ha_inv : ↑a⁻¹ ^ p ^ (n + 1) = ↑(a ^ p ^ (n + 1))⁻¹
⊢ coeff (A * { coeff := inverseCoeff a A }) (Nat.succ n) - coeff 1 (Nat.succ n) -
      (-H_coeff * (↑(a ^ p ^ (n + 1)) * ↑(a ^ p ^ (n + 1))⁻¹) - -H_coeff * 1) =
    0
[PROOFSTEP]
simp only [nthRemainder_spec, inverseCoeff, succNthValUnits, hA, one_coeff_eq_of_pos, Nat.succ_pos', ha_inv, ha,
  inv_pow]
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : kˣ
A : 𝕎 k
hA : coeff A 0 = ↑a
n : ℕ
n_ih✝ : coeff (A * { coeff := inverseCoeff a A }) n = coeff 1 n
H_coeff : k :=
  coeff A (n + 1) * ↑(a⁻¹ ^ p ^ (n + 1)) + nthRemainder p n (truncateFun (n + 1) A) fun i => inverseCoeff a A ↑i
H : ↑(a ^ p ^ (n + 1)) * ↑(a ^ p ^ (n + 1))⁻¹ = 1
ha : ↑a ^ p ^ (n + 1) = ↑(a ^ p ^ (n + 1))
ha_inv : ↑a⁻¹ ^ p ^ (n + 1) = ↑(a ^ p ^ (n + 1))⁻¹
⊢ coeff A (n + 1) * ↑(a ^ p ^ (n + 1))⁻¹ +
            -↑(a ^ p ^ (n + 1))⁻¹ *
                (coeff A (n + 1) * ↑(a ^ p ^ (n + 1))⁻¹ +
                  nthRemainder p n (truncateFun (n + 1) A) fun i => inverseCoeff a A ↑i) *
              ↑(a ^ p ^ (n + 1)) +
          nthRemainder p n (truncateFun (n + 1) A) (truncateFun (n + 1) { coeff := inverseCoeff a A }) -
        0 -
      (-(coeff A (n + 1) * ↑(a ^ p ^ (n + 1))⁻¹ +
              nthRemainder p n (truncateFun (n + 1) A) fun i => inverseCoeff a A ↑i) *
          (↑(a ^ p ^ (n + 1)) * ↑(a ^ p ^ (n + 1))⁻¹) -
        -(coeff A (n + 1) * ↑(a ^ p ^ (n + 1))⁻¹ +
              nthRemainder p n (truncateFun (n + 1) A) fun i => inverseCoeff a A ↑i) *
          1) =
    0
[PROOFSTEP]
ring!
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
x : 𝕎 k
hx : coeff x 0 ≠ 0
⊢ IsUnit x
[PROOFSTEP]
let y : kˣ := Units.mk0 (x.coeff 0) hx
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
x : 𝕎 k
hx : coeff x 0 ≠ 0
y : kˣ := Units.mk0 (coeff x 0) hx
⊢ IsUnit x
[PROOFSTEP]
have hy : x.coeff 0 = y := rfl
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
x : 𝕎 k
hx : coeff x 0 ≠ 0
y : kˣ := Units.mk0 (coeff x 0) hx
hy : coeff x 0 = ↑y
⊢ IsUnit x
[PROOFSTEP]
exact (mkUnit hy).isUnit
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
⊢ Irreducible ↑p
[PROOFSTEP]
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
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
⊢ ¬IsUnit ↑p
[PROOFSTEP]
intro hp
[GOAL]
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : IsUnit ↑p
⊢ False
[PROOFSTEP]
simpa only [constantCoeff_apply, coeff_p_zero, not_isUnit_zero] using
  (constantCoeff : WittVector p k →+* _).isUnit_map hp
[GOAL]
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
⊢ Irreducible ↑p
[PROOFSTEP]
refine' ⟨hp, fun a b hab => _⟩
[GOAL]
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a b : 𝕎 k
hab : ↑p = a * b
⊢ IsUnit a ∨ IsUnit b
[PROOFSTEP]
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
[GOAL]
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a b : 𝕎 k
hab : ↑p = a * b
⊢ a ≠ 0 ∧ b ≠ 0
[PROOFSTEP]
rw [← mul_ne_zero_iff]
[GOAL]
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a b : 𝕎 k
hab : ↑p = a * b
⊢ a * b ≠ 0
[PROOFSTEP]
intro h
[GOAL]
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a b : 𝕎 k
hab : ↑p = a * b
h : a * b = 0
⊢ False
[PROOFSTEP]
rw [h] at hab 
[GOAL]
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a b : 𝕎 k
hab : ↑p = 0
h : a * b = 0
⊢ False
[PROOFSTEP]
exact p_nonzero p k hab
[GOAL]
case intro
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a b : 𝕎 k
hab : ↑p = a * b
ha0 : a ≠ 0
hb0 : b ≠ 0
⊢ IsUnit a ∨ IsUnit b
[PROOFSTEP]
obtain ⟨m, a, ha, rfl⟩ := verschiebung_nonzero ha0
[GOAL]
case intro.intro.intro.intro
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
b : 𝕎 k
hb0 : b ≠ 0
m : ℕ
a : 𝕎 k
ha : coeff a 0 ≠ 0
hab : ↑p = (↑verschiebung)^[m] a * b
ha0 : (↑verschiebung)^[m] a ≠ 0
⊢ IsUnit ((↑verschiebung)^[m] a) ∨ IsUnit b
[PROOFSTEP]
obtain ⟨n, b, hb, rfl⟩ := verschiebung_nonzero hb0
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
m : ℕ
a : 𝕎 k
ha : coeff a 0 ≠ 0
ha0 : (↑verschiebung)^[m] a ≠ 0
n : ℕ
b : 𝕎 k
hb : coeff b 0 ≠ 0
hb0 : (↑verschiebung)^[n] b ≠ 0
hab : ↑p = (↑verschiebung)^[m] a * (↑verschiebung)^[n] b
⊢ IsUnit ((↑verschiebung)^[m] a) ∨ IsUnit ((↑verschiebung)^[n] b)
[PROOFSTEP]
cases m
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.zero
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a : 𝕎 k
ha : coeff a 0 ≠ 0
n : ℕ
b : 𝕎 k
hb : coeff b 0 ≠ 0
hb0 : (↑verschiebung)^[n] b ≠ 0
ha0 : (↑verschiebung)^[Nat.zero] a ≠ 0
hab : ↑p = (↑verschiebung)^[Nat.zero] a * (↑verschiebung)^[n] b
⊢ IsUnit ((↑verschiebung)^[Nat.zero] a) ∨ IsUnit ((↑verschiebung)^[n] b)
[PROOFSTEP]
exact Or.inl (isUnit_of_coeff_zero_ne_zero a ha)
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.succ
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a : 𝕎 k
ha : coeff a 0 ≠ 0
n : ℕ
b : 𝕎 k
hb : coeff b 0 ≠ 0
hb0 : (↑verschiebung)^[n] b ≠ 0
n✝ : ℕ
ha0 : (↑verschiebung)^[Nat.succ n✝] a ≠ 0
hab : ↑p = (↑verschiebung)^[Nat.succ n✝] a * (↑verschiebung)^[n] b
⊢ IsUnit ((↑verschiebung)^[Nat.succ n✝] a) ∨ IsUnit ((↑verschiebung)^[n] b)
[PROOFSTEP]
cases' n with n
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.succ.zero
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a : 𝕎 k
ha : coeff a 0 ≠ 0
b : 𝕎 k
hb : coeff b 0 ≠ 0
n✝ : ℕ
ha0 : (↑verschiebung)^[Nat.succ n✝] a ≠ 0
hb0 : (↑verschiebung)^[Nat.zero] b ≠ 0
hab : ↑p = (↑verschiebung)^[Nat.succ n✝] a * (↑verschiebung)^[Nat.zero] b
⊢ IsUnit ((↑verschiebung)^[Nat.succ n✝] a) ∨ IsUnit ((↑verschiebung)^[Nat.zero] b)
[PROOFSTEP]
exact Or.inr (isUnit_of_coeff_zero_ne_zero b hb)
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.succ.succ
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a : 𝕎 k
ha : coeff a 0 ≠ 0
b : 𝕎 k
hb : coeff b 0 ≠ 0
n✝ : ℕ
ha0 : (↑verschiebung)^[Nat.succ n✝] a ≠ 0
n : ℕ
hb0 : (↑verschiebung)^[Nat.succ n] b ≠ 0
hab : ↑p = (↑verschiebung)^[Nat.succ n✝] a * (↑verschiebung)^[Nat.succ n] b
⊢ IsUnit ((↑verschiebung)^[Nat.succ n✝] a) ∨ IsUnit ((↑verschiebung)^[Nat.succ n] b)
[PROOFSTEP]
rw [iterate_verschiebung_mul] at hab 
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.succ.succ
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a : 𝕎 k
ha : coeff a 0 ≠ 0
b : 𝕎 k
hb : coeff b 0 ≠ 0
n✝ : ℕ
ha0 : (↑verschiebung)^[Nat.succ n✝] a ≠ 0
n : ℕ
hb0 : (↑verschiebung)^[Nat.succ n] b ≠ 0
hab : ↑p = (↑verschiebung)^[Nat.succ n✝ + Nat.succ n] ((↑frobenius)^[Nat.succ n] a * (↑frobenius)^[Nat.succ n✝] b)
⊢ IsUnit ((↑verschiebung)^[Nat.succ n✝] a) ∨ IsUnit ((↑verschiebung)^[Nat.succ n] b)
[PROOFSTEP]
apply_fun fun x => coeff x 1 at hab 
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.succ.succ
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a : 𝕎 k
ha : coeff a 0 ≠ 0
b : 𝕎 k
hb : coeff b 0 ≠ 0
n✝ : ℕ
ha0 : (↑verschiebung)^[Nat.succ n✝] a ≠ 0
n : ℕ
hb0 : (↑verschiebung)^[Nat.succ n] b ≠ 0
hab :
  coeff (↑p) 1 =
    coeff ((↑verschiebung)^[Nat.succ n✝ + Nat.succ n] ((↑frobenius)^[Nat.succ n] a * (↑frobenius)^[Nat.succ n✝] b)) 1
⊢ IsUnit ((↑verschiebung)^[Nat.succ n✝] a) ∨ IsUnit ((↑verschiebung)^[Nat.succ n] b)
[PROOFSTEP]
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 
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.succ.succ
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a : 𝕎 k
ha : coeff a 0 ≠ 0
b : 𝕎 k
hb : coeff b 0 ≠ 0
n✝ : ℕ
ha0 : (↑verschiebung)^[Nat.succ n✝] a ≠ 0
n : ℕ
hb0 : (↑verschiebung)^[Nat.succ n] b ≠ 0
hab : 1 = 0
⊢ IsUnit ((↑verschiebung)^[Nat.succ n✝] a) ∨ IsUnit ((↑verschiebung)^[Nat.succ n] b)
[PROOFSTEP]
exact (one_ne_zero hab).elim
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
⊢ ∃ m b, coeff b 0 ≠ 0 ∧ a = ↑p ^ m * b
[PROOFSTEP]
obtain ⟨m, c, hc, hcm⟩ := WittVector.verschiebung_nonzero ha
[GOAL]
case intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
c : 𝕎 k
hc : coeff c 0 ≠ 0
hcm : a = (↑verschiebung)^[m] c
⊢ ∃ m b, coeff b 0 ≠ 0 ∧ a = ↑p ^ m * b
[PROOFSTEP]
obtain ⟨b, rfl⟩ := (frobenius_bijective p k).surjective.iterate m c
[GOAL]
case intro.intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : coeff ((↑frobenius)^[m] b) 0 ≠ 0
hcm : a = (↑verschiebung)^[m] ((↑frobenius)^[m] b)
⊢ ∃ m b, coeff b 0 ≠ 0 ∧ a = ↑p ^ m * b
[PROOFSTEP]
rw [WittVector.iterate_frobenius_coeff] at hc 
[GOAL]
case intro.intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : coeff b 0 ^ p ^ m ≠ 0
hcm : a = (↑verschiebung)^[m] ((↑frobenius)^[m] b)
⊢ ∃ m b, coeff b 0 ≠ 0 ∧ a = ↑p ^ m * b
[PROOFSTEP]
have := congr_fun (WittVector.verschiebung_frobenius_comm.comp_iterate m) b
[GOAL]
case intro.intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : coeff b 0 ^ p ^ m ≠ 0
hcm : a = (↑verschiebung)^[m] ((↑frobenius)^[m] b)
this : (↑verschiebung ∘ ↑frobenius)^[m] b = ((↑verschiebung)^[m] ∘ (↑frobenius)^[m]) b
⊢ ∃ m b, coeff b 0 ≠ 0 ∧ a = ↑p ^ m * b
[PROOFSTEP]
simp only [Function.comp_apply] at this 
[GOAL]
case intro.intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : coeff b 0 ^ p ^ m ≠ 0
hcm : a = (↑verschiebung)^[m] ((↑frobenius)^[m] b)
this : (↑verschiebung ∘ ↑frobenius)^[m] b = (↑verschiebung)^[m] ((↑frobenius)^[m] b)
⊢ ∃ m b, coeff b 0 ≠ 0 ∧ a = ↑p ^ m * b
[PROOFSTEP]
rw [← this] at hcm 
[GOAL]
case intro.intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : coeff b 0 ^ p ^ m ≠ 0
hcm : a = (↑verschiebung ∘ ↑frobenius)^[m] b
this : (↑verschiebung ∘ ↑frobenius)^[m] b = (↑verschiebung)^[m] ((↑frobenius)^[m] b)
⊢ ∃ m b, coeff b 0 ≠ 0 ∧ a = ↑p ^ m * b
[PROOFSTEP]
refine' ⟨m, b, _, _⟩
[GOAL]
case intro.intro.intro.intro.refine'_1
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : coeff b 0 ^ p ^ m ≠ 0
hcm : a = (↑verschiebung ∘ ↑frobenius)^[m] b
this : (↑verschiebung ∘ ↑frobenius)^[m] b = (↑verschiebung)^[m] ((↑frobenius)^[m] b)
⊢ coeff b 0 ≠ 0
[PROOFSTEP]
contrapose! hc
[GOAL]
case intro.intro.intro.intro.refine'_1
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hcm : a = (↑verschiebung ∘ ↑frobenius)^[m] b
this : (↑verschiebung ∘ ↑frobenius)^[m] b = (↑verschiebung)^[m] ((↑frobenius)^[m] b)
hc : coeff b 0 = 0
⊢ coeff b 0 ^ p ^ m = 0
[PROOFSTEP]
have : 0 < p ^ m := pow_pos (Nat.Prime.pos Fact.out) _
[GOAL]
case intro.intro.intro.intro.refine'_1
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hcm : a = (↑verschiebung ∘ ↑frobenius)^[m] b
this✝ : (↑verschiebung ∘ ↑frobenius)^[m] b = (↑verschiebung)^[m] ((↑frobenius)^[m] b)
hc : coeff b 0 = 0
this : 0 < p ^ m
⊢ coeff b 0 ^ p ^ m = 0
[PROOFSTEP]
simp [hc, zero_pow this]
[GOAL]
case intro.intro.intro.intro.refine'_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : coeff b 0 ^ p ^ m ≠ 0
hcm : a = (↑verschiebung ∘ ↑frobenius)^[m] b
this : (↑verschiebung ∘ ↑frobenius)^[m] b = (↑verschiebung)^[m] ((↑frobenius)^[m] b)
⊢ a = ↑p ^ m * b
[PROOFSTEP]
simp_rw [← mul_left_iterate (p : 𝕎 k) m]
[GOAL]
case intro.intro.intro.intro.refine'_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : coeff b 0 ^ p ^ m ≠ 0
hcm : a = (↑verschiebung ∘ ↑frobenius)^[m] b
this : (↑verschiebung ∘ ↑frobenius)^[m] b = (↑verschiebung)^[m] ((↑frobenius)^[m] b)
⊢ a = (fun x => ↑p * x)^[m] b
[PROOFSTEP]
convert hcm using 2
[GOAL]
case h.e'_3.h.e'_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : coeff b 0 ^ p ^ m ≠ 0
hcm : a = (↑verschiebung ∘ ↑frobenius)^[m] b
this : (↑verschiebung ∘ ↑frobenius)^[m] b = (↑verschiebung)^[m] ((↑frobenius)^[m] b)
⊢ (fun x => ↑p * x) = ↑verschiebung ∘ ↑frobenius
[PROOFSTEP]
ext1 x
[GOAL]
case h.e'_3.h.e'_2.h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : coeff b 0 ^ p ^ m ≠ 0
hcm : a = (↑verschiebung ∘ ↑frobenius)^[m] b
this : (↑verschiebung ∘ ↑frobenius)^[m] b = (↑verschiebung)^[m] ((↑frobenius)^[m] b)
x : 𝕎 k
⊢ ↑p * x = (↑verschiebung ∘ ↑frobenius) x
[PROOFSTEP]
rw [mul_comm, ← WittVector.verschiebung_frobenius x]
[GOAL]
case h.e'_3.h.e'_2.h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : coeff b 0 ^ p ^ m ≠ 0
hcm : a = (↑verschiebung ∘ ↑frobenius)^[m] b
this : (↑verschiebung ∘ ↑frobenius)^[m] b = (↑verschiebung)^[m] ((↑frobenius)^[m] b)
x : 𝕎 k
⊢ ↑verschiebung (↑frobenius x) = (↑verschiebung ∘ ↑frobenius) x
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
⊢ ∃ m b, a = ↑p ^ m * ↑b
[PROOFSTEP]
obtain ⟨m, b, h₁, h₂⟩ := exists_eq_pow_p_mul a ha
[GOAL]
case intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
h₁ : coeff b 0 ≠ 0
h₂ : a = ↑p ^ m * b
⊢ ∃ m b, a = ↑p ^ m * ↑b
[PROOFSTEP]
let b₀ := Units.mk0 (b.coeff 0) h₁
[GOAL]
case intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
h₁ : coeff b 0 ≠ 0
h₂ : a = ↑p ^ m * b
b₀ : kˣ := Units.mk0 (coeff b 0) h₁
⊢ ∃ m b, a = ↑p ^ m * ↑b
[PROOFSTEP]
have hb₀ : b.coeff 0 = b₀ := rfl
[GOAL]
case intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
h₁ : coeff b 0 ≠ 0
h₂ : a = ↑p ^ m * b
b₀ : kˣ := Units.mk0 (coeff b 0) h₁
hb₀ : coeff b 0 = ↑b₀
⊢ ∃ m b, a = ↑p ^ m * ↑b
[PROOFSTEP]
exact ⟨m, mkUnit hb₀, h₂⟩
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
⊢ DiscreteValuationRing.HasUnitMulPowIrreducibleFactorization (𝕎 k)
[PROOFSTEP]
refine' ⟨p, irreducible p, fun {x} hx => _⟩
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
hx : x ≠ 0
⊢ ∃ n, Associated (↑p ^ n) x
[PROOFSTEP]
obtain ⟨n, b, hb⟩ := exists_eq_pow_p_mul' x hx
[GOAL]
case intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
hx : x ≠ 0
n : ℕ
b : (𝕎 k)ˣ
hb : x = ↑p ^ n * ↑b
⊢ ∃ n, Associated (↑p ^ n) x
[PROOFSTEP]
exact ⟨n, b, hb.symm⟩
