-- Mathlib/RingTheory/WittVector/Domain.lean
theorem verschiebung_nonzero {x : 𝕎 R} (hx : x ≠ 0) :
    ∃ n : ℕ, ∃ x' : 𝕎 R, x'.coeff 0 ≠ 0 ∧ x = verschiebung^[n] x'

Proof state:
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 x', x'.coeff 0 ≠ 0 ∧ x = (⇑verschiebung)^[n] x'

Tactic:
let n := Nat.find hex

Result:
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 hex
⊢ ∃ n x', x'.coeff 0 ≠ 0 ∧ x = (⇑verschiebung)^[n] x'

Proof state:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
hx : x ≠ 0
⊢ ∃ n x', x'.coeff 0 ≠ 0 ∧ x = (⇑verschiebung)^[n] x'

Tactic:
have hex : ∃ k : ℕ, x.coeff k ≠ 0 := by
  by_contra! hall
  apply hx
  ext i
  simp only [hall, zero_coeff]

Result:
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 x', x'.coeff 0 ≠ 0 ∧ x = (⇑verschiebung)^[n] x'

Proof state:
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

Tactic:
ext i

Result:
case h
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
hx : x ≠ 0
hall : ∀ (k : ℕ), x.coeff k = 0
i : ℕ
⊢ x.coeff i = coeff 0 i

Proof state:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
hx : x ≠ 0
⊢ ∃ n x', x'.coeff 0 ≠ 0 ∧ x = (⇑verschiebung)^[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

Result:
no goals

Proof state:
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

Tactic:
apply hx

Result:
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

Proof state:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
hx : x ≠ 0
⊢ ∃ k, x.coeff k ≠ 0

Tactic:
by_contra! hall

Result:
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

Proof state:
case h
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
hx : x ≠ 0
hall : ∀ (k : ℕ), x.coeff k = 0
i : ℕ
⊢ x.coeff i = coeff 0 i

Tactic:
simp only [hall, zero_coeff]

Result:
no goals

Proof state:
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 hex
⊢ ∃ n x', x'.coeff 0 ≠ 0 ∧ x = (⇑verschiebung)^[n] x'

Tactic:
use n, x.shift n

Result:
case h
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 hex
⊢ (x.shift n).coeff 0 ≠ 0 ∧ x = (⇑verschiebung)^[n] (x.shift n)

Proof state:
case h
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 hex
⊢ (x.shift n).coeff 0 ≠ 0 ∧ x = (⇑verschiebung)^[n] (x.shift n)

Tactic:
refine ⟨Nat.find_spec hex, eq_iterate_verschiebung fun i hi => not_not.mp ?_⟩

Result:
case h
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 hex
i : ℕ
hi : i < n
⊢ ¬¬x.coeff i = 0

Proof state:
case h
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 hex
i : ℕ
hi : i < n
⊢ ¬¬x.coeff i = 0

Tactic:
exact Nat.find_min hex hi

Result:
no goals