[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k : ℕ
h : ∀ (i : ℕ), i < k + 1 → coeff x i = 0
⊢ ↑verschiebung (shift x (Nat.succ k)) = shift x k
[PROOFSTEP]
ext ⟨j⟩
[GOAL]
case h.zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k : ℕ
h : ∀ (i : ℕ), i < k + 1 → coeff x i = 0
⊢ coeff (↑verschiebung (shift x (Nat.succ k))) Nat.zero = coeff (shift x k) Nat.zero
[PROOFSTEP]
rw [verschiebung_coeff_zero, shift_coeff, h]
[GOAL]
case h.zero.a
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k : ℕ
h : ∀ (i : ℕ), i < k + 1 → coeff x i = 0
⊢ k + Nat.zero < k + 1
[PROOFSTEP]
apply Nat.lt_succ_self
[GOAL]
case h.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k : ℕ
h : ∀ (i : ℕ), i < k + 1 → coeff x i = 0
n✝ : ℕ
⊢ coeff (↑verschiebung (shift x (Nat.succ k))) (Nat.succ n✝) = coeff (shift x k) (Nat.succ n✝)
[PROOFSTEP]
simp only [verschiebung_coeff_succ, shift]
[GOAL]
case h.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k : ℕ
h : ∀ (i : ℕ), i < k + 1 → coeff x i = 0
n✝ : ℕ
⊢ coeff x (Nat.succ k + n✝) = coeff x (k + Nat.succ n✝)
[PROOFSTEP]
congr 1
[GOAL]
case h.succ.e_a
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k : ℕ
h : ∀ (i : ℕ), i < k + 1 → coeff x i = 0
n✝ : ℕ
⊢ Nat.succ k + n✝ = k + Nat.succ n✝
[PROOFSTEP]
rw [Nat.add_succ, add_comm, Nat.add_succ, add_comm]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
h : ∀ (i : ℕ), i < n → coeff x i = 0
⊢ x = (↑verschiebung)^[n] (shift x n)
[PROOFSTEP]
induction' n with k ih
[GOAL]
case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
h✝ : ∀ (i : ℕ), i < n → coeff x i = 0
h : ∀ (i : ℕ), i < Nat.zero → coeff x i = 0
⊢ x = (↑verschiebung)^[Nat.zero] (shift x Nat.zero)
[PROOFSTEP]
cases x
[GOAL]
case zero.mk'
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
coeff✝ : ℕ → R
h✝ : ∀ (i : ℕ), i < n → coeff { coeff := coeff✝ } i = 0
h : ∀ (i : ℕ), i < Nat.zero → coeff { coeff := coeff✝ } i = 0
⊢ { coeff := coeff✝ } = (↑verschiebung)^[Nat.zero] (shift { coeff := coeff✝ } Nat.zero)
[PROOFSTEP]
simp [shift]
[GOAL]
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
h✝ : ∀ (i : ℕ), i < n → coeff x i = 0
k : ℕ
ih : (∀ (i : ℕ), i < k → coeff x i = 0) → x = (↑verschiebung)^[k] (shift x k)
h : ∀ (i : ℕ), i < Nat.succ k → coeff x i = 0
⊢ x = (↑verschiebung)^[Nat.succ k] (shift x (Nat.succ k))
[PROOFSTEP]
dsimp
[GOAL]
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
h✝ : ∀ (i : ℕ), i < n → coeff x i = 0
k : ℕ
ih : (∀ (i : ℕ), i < k → coeff x i = 0) → x = (↑verschiebung)^[k] (shift x k)
h : ∀ (i : ℕ), i < Nat.succ k → coeff x i = 0
⊢ x = (↑verschiebung)^[k] (↑verschiebung (shift x (Nat.succ k)))
[PROOFSTEP]
rw [verschiebung_shift]
[GOAL]
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
h✝ : ∀ (i : ℕ), i < n → coeff x i = 0
k : ℕ
ih : (∀ (i : ℕ), i < k → coeff x i = 0) → x = (↑verschiebung)^[k] (shift x k)
h : ∀ (i : ℕ), i < Nat.succ k → coeff x i = 0
⊢ x = (↑verschiebung)^[k] (shift x k)
[PROOFSTEP]
exact ih fun i hi => h _ (hi.trans (Nat.lt_succ_self _))
[GOAL]
case succ.h
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
h✝ : ∀ (i : ℕ), i < n → coeff x i = 0
k : ℕ
ih : (∀ (i : ℕ), i < k → coeff x i = 0) → x = (↑verschiebung)^[k] (shift x k)
h : ∀ (i : ℕ), i < Nat.succ k → coeff x i = 0
⊢ ∀ (i : ℕ), i < k + 1 → coeff x i = 0
[PROOFSTEP]
exact h
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
hx : x ≠ 0
⊢ ∃ n x', coeff x' 0 ≠ 0 ∧ x = (↑verschiebung)^[n] x'
[PROOFSTEP]
have hex : ∃ k : ℕ, x.coeff k ≠ 0 := by
  by_contra' hall
  apply hx
  ext i
  simp only [hall, zero_coeff]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
hx : x ≠ 0
⊢ ∃ k, coeff x k ≠ 0
[PROOFSTEP]
by_contra' hall
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
hx : x ≠ 0
hall : ∀ (k : ℕ), coeff x k = 0
⊢ False
[PROOFSTEP]
apply hx
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
hx : x ≠ 0
hall : ∀ (k : ℕ), coeff x k = 0
⊢ x = 0
[PROOFSTEP]
ext i
[GOAL]
case h
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
hx : x ≠ 0
hall : ∀ (k : ℕ), coeff x k = 0
i : ℕ
⊢ coeff x i = coeff 0 i
[PROOFSTEP]
simp only [hall, zero_coeff]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
hx : x ≠ 0
hex : ∃ k, coeff x k ≠ 0
⊢ ∃ n x', coeff x' 0 ≠ 0 ∧ x = (↑verschiebung)^[n] x'
[PROOFSTEP]
let n := Nat.find hex
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
hx : x ≠ 0
hex : ∃ k, coeff x k ≠ 0
n : ℕ := Nat.find hex
⊢ ∃ n x', coeff x' 0 ≠ 0 ∧ x = (↑verschiebung)^[n] x'
[PROOFSTEP]
use n, x.shift n
[GOAL]
case h
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
hx : x ≠ 0
hex : ∃ k, coeff x k ≠ 0
n : ℕ := Nat.find hex
⊢ coeff (shift x n) 0 ≠ 0 ∧ x = (↑verschiebung)^[n] (shift x n)
[PROOFSTEP]
refine' ⟨Nat.find_spec hex, eq_iterate_verschiebung fun i hi => not_not.mp _⟩
[GOAL]
case h
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
hx : x ≠ 0
hex : ∃ k, coeff x k ≠ 0
n : ℕ := Nat.find hex
i : ℕ
hi : i < n
⊢ ¬¬coeff x i = 0
[PROOFSTEP]
exact Nat.find_min hex hi
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
x y : 𝕎 R
⊢ x * y = 0 → x = 0 ∨ y = 0
[PROOFSTEP]
contrapose!
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
x y : 𝕎 R
⊢ x ≠ 0 ∧ y ≠ 0 → x * y ≠ 0
[PROOFSTEP]
rintro ⟨ha, hb⟩
[GOAL]
case intro
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
x y : 𝕎 R
ha : x ≠ 0
hb : y ≠ 0
⊢ x * y ≠ 0
[PROOFSTEP]
rcases verschiebung_nonzero ha with ⟨na, wa, hwa0, rfl⟩
[GOAL]
case intro.intro.intro.intro
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
y : 𝕎 R
hb : y ≠ 0
na : ℕ
wa : 𝕎 R
hwa0 : coeff wa 0 ≠ 0
ha : (↑verschiebung)^[na] wa ≠ 0
⊢ (↑verschiebung)^[na] wa * y ≠ 0
[PROOFSTEP]
rcases verschiebung_nonzero hb with ⟨nb, wb, hwb0, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
na : ℕ
wa : 𝕎 R
hwa0 : coeff wa 0 ≠ 0
ha : (↑verschiebung)^[na] wa ≠ 0
nb : ℕ
wb : 𝕎 R
hwb0 : coeff wb 0 ≠ 0
hb : (↑verschiebung)^[nb] wb ≠ 0
⊢ (↑verschiebung)^[na] wa * (↑verschiebung)^[nb] wb ≠ 0
[PROOFSTEP]
refine' ne_of_apply_ne (fun x => x.coeff (na + nb)) _
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
na : ℕ
wa : 𝕎 R
hwa0 : coeff wa 0 ≠ 0
ha : (↑verschiebung)^[na] wa ≠ 0
nb : ℕ
wb : 𝕎 R
hwb0 : coeff wb 0 ≠ 0
hb : (↑verschiebung)^[nb] wb ≠ 0
⊢ (fun x => coeff x (na + nb)) ((↑verschiebung)^[na] wa * (↑verschiebung)^[nb] wb) ≠ (fun x => coeff x (na + nb)) 0
[PROOFSTEP]
dsimp only
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
na : ℕ
wa : 𝕎 R
hwa0 : coeff wa 0 ≠ 0
ha : (↑verschiebung)^[na] wa ≠ 0
nb : ℕ
wb : 𝕎 R
hwb0 : coeff wb 0 ≠ 0
hb : (↑verschiebung)^[nb] wb ≠ 0
⊢ coeff ((↑verschiebung)^[na] wa * (↑verschiebung)^[nb] wb) (na + nb) ≠ coeff 0 (na + nb)
[PROOFSTEP]
rw [iterate_verschiebung_mul_coeff, zero_coeff]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
na : ℕ
wa : 𝕎 R
hwa0 : coeff wa 0 ≠ 0
ha : (↑verschiebung)^[na] wa ≠ 0
nb : ℕ
wb : 𝕎 R
hwb0 : coeff wb 0 ≠ 0
hb : (↑verschiebung)^[nb] wb ≠ 0
⊢ coeff wa 0 ^ p ^ nb * coeff wb 0 ^ p ^ na ≠ 0
[PROOFSTEP]
exact mul_ne_zero (pow_ne_zero _ hwa0) (pow_ne_zero _ hwb0)
