-- Mathlib/FieldTheory/IsPerfectClosure.lean
theorem mem_pNilradical {R : Type*} [CommSemiring R] {p : ℕ} {x : R} :
    x ∈ pNilradical R p ↔ ∃ n : ℕ, x ^ p ^ n = 0

Proof state:
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp : ¬1 < p
h : x = 0
⊢ x ^ p ^ 0 = 0

Tactic:
rw [pow_zero, pow_one, h]

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp✝ : ¬1 < p
x✝ : ∃ n, x ^ p ^ n = 0
n : ℕ
h : 1 = 0
hp : p = 0
hn : ¬n = 0
⊢ x = 0

Tactic:
subsingleton [subsingleton_of_zero_eq_one h.symm]

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp : ¬1 < p
⊢ x = 0 ↔ ∃ n, x ^ p ^ n = 0

Tactic:
refine ⟨fun h ↦ ⟨0, by rw [pow_zero, pow_one, h]⟩, fun ⟨n, h⟩ ↦ ?_⟩

Result:
case neg
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp : ¬1 < p
x✝ : ∃ n, x ^ p ^ n = 0
n : ℕ
h : x ^ p ^ n = 0
⊢ x = 0

Proof state:
case neg.inl
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp✝ : ¬1 < p
x✝ : ∃ n, x ^ p ^ n = 0
n : ℕ
h : x ^ p ^ n = 0
hp : p = 0
⊢ x = 0

Tactic:
by_cases hn : n = 0

Result:
case pos
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp✝ : ¬1 < p
x✝ : ∃ n, x ^ p ^ n = 0
n : ℕ
h : x ^ p ^ n = 0
hp : p = 0
hn : n = 0
⊢ x = 0

case neg
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp✝ : ¬1 < p
x✝ : ∃ n, x ^ p ^ n = 0
n : ℕ
h : x ^ p ^ n = 0
hp : p = 0
hn : ¬n = 0
⊢ x = 0

Proof state:
case neg
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp✝ : ¬1 < p
x✝ : ∃ n, x ^ p ^ n = 0
n : ℕ
h : x ^ p ^ n = 0
hp : p = 0
hn : ¬n = 0
⊢ x = 0

Tactic:
rw [hp, zero_pow hn, pow_zero] at h

Result:
case neg
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp✝ : ¬1 < p
x✝ : ∃ n, x ^ p ^ n = 0
n : ℕ
h : 1 = 0
hp : p = 0
hn : ¬n = 0
⊢ x = 0

Proof state:
case pos
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp : 1 < p
x✝ : x ∈ nilradical R
n : ℕ
h : x ^ n ∈ 0
⊢ x ^ p ^ n = 0

Tactic:
rw [← Nat.sub_add_cancel ((n.lt_pow_self hp).le), pow_add, h, mul_zero]

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp : ¬1 < p
⊢ x ∈ pNilradical R p ↔ ∃ n, x ^ p ^ n = 0

Tactic:
rw [pNilradical_eq_bot hp, Ideal.mem_bot]

Result:
case neg
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp : ¬1 < p
⊢ x = 0 ↔ ∃ n, x ^ p ^ n = 0

Proof state:
case neg.inr
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp✝ : ¬1 < p
x✝ : ∃ n, x ^ p ^ n = 0
n : ℕ
h : x ^ p ^ n = 0
hp : p = 1
⊢ x = 0

Tactic:
rwa [hp, one_pow, pow_one] at h

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp : 1 < p
⊢ x ∈ nilradical R ↔ ∃ n, x ^ p ^ n = 0

Tactic:
refine ⟨fun ⟨n, h⟩ ↦ ⟨n, ?_⟩, fun ⟨n, h⟩ ↦ ⟨p ^ n, h⟩⟩

Result:
case pos
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp : 1 < p
x✝ : x ∈ nilradical R
n : ℕ
h : x ^ n ∈ 0
⊢ x ^ p ^ n = 0

Proof state:
case pos
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp : 1 < p
⊢ x ∈ pNilradical R p ↔ ∃ n, x ^ p ^ n = 0

Tactic:
rw [pNilradical_eq_nilradical hp]

Result:
case pos
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp : 1 < p
⊢ x ∈ nilradical R ↔ ∃ n, x ^ p ^ n = 0

Proof state:
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
⊢ x ∈ pNilradical R p ↔ ∃ n, x ^ p ^ n = 0

Tactic:
by_cases hp : 1 < p

Result:
case pos
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp : 1 < p
⊢ x ∈ pNilradical R p ↔ ∃ n, x ^ p ^ n = 0

case neg
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp : ¬1 < p
⊢ x ∈ pNilradical R p ↔ ∃ n, x ^ p ^ n = 0

Proof state:
case pos
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp✝ : ¬1 < p
x✝ : ∃ n, x ^ p ^ n = 0
n : ℕ
h : x ^ p ^ n = 0
hp : p = 0
hn : n = 0
⊢ x = 0

Tactic:
rwa [hn, pow_zero, pow_one] at h

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp : ¬1 < p
x✝ : ∃ n, x ^ p ^ n = 0
n : ℕ
h : x ^ p ^ n = 0
⊢ x = 0

Tactic:
rcases Nat.le_one_iff_eq_zero_or_eq_one.1 (not_lt.1 hp) with hp | hp

Result:
case neg.inl
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp✝ : ¬1 < p
x✝ : ∃ n, x ^ p ^ n = 0
n : ℕ
h : x ^ p ^ n = 0
hp : p = 0
⊢ x = 0

case neg.inr
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp✝ : ¬1 < p
x✝ : ∃ n, x ^ p ^ n = 0
n : ℕ
h : x ^ p ^ n = 0
hp : p = 1
⊢ x = 0