-- Mathlib/RingTheory/WittVector/DiscreteValuationRing.lean
theorem irreducible : Irreducible (p : 𝕎 k)

Proof state:
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 : a.coeff 0 ≠ 0
b : 𝕎 k
hb : b.coeff 0 ≠ 0
n✝ : ℕ
ha0 : (⇑verschiebung)^[n✝ + 1] a ≠ 0
n : ℕ
hb0 : (⇑verschiebung)^[n + 1] b ≠ 0
hab : ↑p = (⇑verschiebung)^[n✝ + 1 + (n + 1)] ((⇑frobenius)^[n + 1] a * (⇑frobenius)^[n✝ + 1] b)
⊢ IsUnit ((⇑verschiebung)^[n✝ + 1] a) ∨ IsUnit ((⇑verschiebung)^[n + 1] b)

Tactic:
apply_fun fun x => coeff x 1 at hab

Result:
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 : a.coeff 0 ≠ 0
b : 𝕎 k
hb : b.coeff 0 ≠ 0
n✝ : ℕ
ha0 : (⇑verschiebung)^[n✝ + 1] a ≠ 0
n : ℕ
hb0 : (⇑verschiebung)^[n + 1] b ≠ 0
hab : (↑p).coeff 1 = ((⇑verschiebung)^[n✝ + 1 + (n + 1)] ((⇑frobenius)^[n + 1] a * (⇑frobenius)^[n✝ + 1] b)).coeff 1
⊢ IsUnit ((⇑verschiebung)^[n✝ + 1] a) ∨ IsUnit ((⇑verschiebung)^[n + 1] b)

Proof state:
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 : a.coeff 0 ≠ 0
b : 𝕎 k
hb : b.coeff 0 ≠ 0
n✝ : ℕ
ha0 : (⇑verschiebung)^[n✝ + 1] a ≠ 0
n : ℕ
hb0 : (⇑verschiebung)^[n + 1] b ≠ 0
hab : (↑p).coeff 1 = ((⇑verschiebung)^[n✝ + 1 + (n + 1)] ((⇑frobenius)^[n + 1] a * (⇑frobenius)^[n✝ + 1] b)).coeff 1
⊢ IsUnit ((⇑verschiebung)^[n✝ + 1] a) ∨ IsUnit ((⇑verschiebung)^[n + 1] b)

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

Result:
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 : a.coeff 0 ≠ 0
b : 𝕎 k
hb : b.coeff 0 ≠ 0
n✝ : ℕ
ha0 : (⇑verschiebung)^[n✝ + 1] a ≠ 0
n : ℕ
hb0 : (⇑verschiebung)^[n + 1] b ≠ 0
hab : 1 = 0
⊢ IsUnit ((⇑verschiebung)^[n✝ + 1] a) ∨ IsUnit ((⇑verschiebung)^[n + 1] b)

Proof state:
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 : a.coeff 0 ≠ 0
ha0 : (⇑verschiebung)^[m] a ≠ 0
n : ℕ
b : 𝕎 k
hb : b.coeff 0 ≠ 0
hb0 : (⇑verschiebung)^[n] b ≠ 0
hab : ↑p = (⇑verschiebung)^[m] a * (⇑verschiebung)^[n] b
⊢ IsUnit ((⇑verschiebung)^[m] a) ∨ IsUnit ((⇑verschiebung)^[n] b)

Tactic:
cases m

Result:
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 : a.coeff 0 ≠ 0
n : ℕ
b : 𝕎 k
hb : b.coeff 0 ≠ 0
hb0 : (⇑verschiebung)^[n] b ≠ 0
ha0 : (⇑verschiebung)^[0] a ≠ 0
hab : ↑p = (⇑verschiebung)^[0] a * (⇑verschiebung)^[n] b
⊢ IsUnit ((⇑verschiebung)^[0] a) ∨ IsUnit ((⇑verschiebung)^[n] b)

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 : a.coeff 0 ≠ 0
n : ℕ
b : 𝕎 k
hb : b.coeff 0 ≠ 0
hb0 : (⇑verschiebung)^[n] b ≠ 0
n✝ : ℕ
ha0 : (⇑verschiebung)^[n✝ + 1] a ≠ 0
hab : ↑p = (⇑verschiebung)^[n✝ + 1] a * (⇑verschiebung)^[n] b
⊢ IsUnit ((⇑verschiebung)^[n✝ + 1] a) ∨ IsUnit ((⇑verschiebung)^[n] b)

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

Tactic:
rw [h] at hab

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