-- Mathlib/FieldTheory/IsPerfectClosure.lean
theorem IsPRadical.comap_pNilradical [IsPRadical i p] :
    (pNilradical L p).comap i = pNilradical K p

Proof state:
case refine_2
K : Type u_1
L : Type u_2
inst✝² : CommSemiring K
inst✝¹ : CommSemiring L
i : K →+* L
p : ℕ
inst✝ : IsPRadical i p
x : K
h : x ∈ pNilradical K p
⊢ x ∈ Ideal.comap i (pNilradical L p)

Tactic:
simp only [Ideal.mem_comap, mem_pNilradical] at h ⊢

Result:
case refine_2
K : Type u_1
L : Type u_2
inst✝² : CommSemiring K
inst✝¹ : CommSemiring L
i : K →+* L
p : ℕ
inst✝ : IsPRadical i p
x : K
h : ∃ n, x ^ p ^ n = 0
⊢ ∃ n, i x ^ p ^ n = 0

Proof state:
case refine_1.intro.intro
K : Type u_1
L : Type u_2
inst✝² : CommSemiring K
inst✝¹ : CommSemiring L
i : K →+* L
p : ℕ
inst✝ : IsPRadical i p
x : K
h✝¹ : x ∈ Ideal.comap i (pNilradical L p)
n : ℕ
h✝ : i x ^ p ^ n = 0
m : ℕ
h : (x ^ p ^ n) ^ p ^ m = 0
⊢ ∃ n, x ^ p ^ n = 0

Tactic:
exact ⟨n + m, by rwa [pow_add, pow_mul]⟩

Result:
no goals

Proof state:
K : Type u_1
L : Type u_2
inst✝² : CommSemiring K
inst✝¹ : CommSemiring L
i : K →+* L
p : ℕ
inst✝ : IsPRadical i p
x : K
h✝¹ : x ∈ Ideal.comap i (pNilradical L p)
n : ℕ
h✝ : i x ^ p ^ n = 0
m : ℕ
h : (x ^ p ^ n) ^ p ^ m = 0
⊢ x ^ p ^ (n + m) = 0

Tactic:
rwa [pow_add, pow_mul]

Result:
no goals

Proof state:
K : Type u_1
L : Type u_2
inst✝² : CommSemiring K
inst✝¹ : CommSemiring L
i : K →+* L
p : ℕ
inst✝ : IsPRadical i p
⊢ Ideal.comap i (pNilradical L p) = pNilradical K p

Tactic:
refine le_antisymm (fun x h ↦ mem_pNilradical.2 ?_) (fun x h ↦ ?_)

Result:
case refine_1
K : Type u_1
L : Type u_2
inst✝² : CommSemiring K
inst✝¹ : CommSemiring L
i : K →+* L
p : ℕ
inst✝ : IsPRadical i p
x : K
h : x ∈ Ideal.comap i (pNilradical L p)
⊢ ∃ n, x ^ p ^ n = 0

case refine_2
K : Type u_1
L : Type u_2
inst✝² : CommSemiring K
inst✝¹ : CommSemiring L
i : K →+* L
p : ℕ
inst✝ : IsPRadical i p
x : K
h : x ∈ pNilradical K p
⊢ x ∈ Ideal.comap i (pNilradical L p)

Proof state:
case refine_1.intro
K : Type u_1
L : Type u_2
inst✝² : CommSemiring K
inst✝¹ : CommSemiring L
i : K →+* L
p : ℕ
inst✝ : IsPRadical i p
x : K
h✝ : x ∈ Ideal.comap i (pNilradical L p)
n : ℕ
h : i x ^ p ^ n = 0
⊢ ∃ n, x ^ p ^ n = 0

Tactic:
obtain ⟨m, h⟩ := mem_pNilradical.1 <| ker_le i p ((map_pow i x _).symm ▸ h)

Result:
case refine_1.intro.intro
K : Type u_1
L : Type u_2
inst✝² : CommSemiring K
inst✝¹ : CommSemiring L
i : K →+* L
p : ℕ
inst✝ : IsPRadical i p
x : K
h✝¹ : x ∈ Ideal.comap i (pNilradical L p)
n : ℕ
h✝ : i x ^ p ^ n = 0
m : ℕ
h : (x ^ p ^ n) ^ p ^ m = 0
⊢ ∃ n, x ^ p ^ n = 0

Proof state:
case refine_2
K : Type u_1
L : Type u_2
inst✝² : CommSemiring K
inst✝¹ : CommSemiring L
i : K →+* L
p : ℕ
inst✝ : IsPRadical i p
x : K
h : ∃ n, x ^ p ^ n = 0
⊢ ∃ n, i x ^ p ^ n = 0

Tactic:
obtain ⟨n, h⟩ := h

Result:
case refine_2.intro
K : Type u_1
L : Type u_2
inst✝² : CommSemiring K
inst✝¹ : CommSemiring L
i : K →+* L
p : ℕ
inst✝ : IsPRadical i p
x : K
n : ℕ
h : x ^ p ^ n = 0
⊢ ∃ n, i x ^ p ^ n = 0

Proof state:
case refine_1
K : Type u_1
L : Type u_2
inst✝² : CommSemiring K
inst✝¹ : CommSemiring L
i : K →+* L
p : ℕ
inst✝ : IsPRadical i p
x : K
h : x ∈ Ideal.comap i (pNilradical L p)
⊢ ∃ n, x ^ p ^ n = 0

Tactic:
obtain ⟨n, h⟩ := mem_pNilradical.1 <| Ideal.mem_comap.1 h

Result:
case refine_1.intro
K : Type u_1
L : Type u_2
inst✝² : CommSemiring K
inst✝¹ : CommSemiring L
i : K →+* L
p : ℕ
inst✝ : IsPRadical i p
x : K
h✝ : x ∈ Ideal.comap i (pNilradical L p)
n : ℕ
h : i x ^ p ^ n = 0
⊢ ∃ n, x ^ p ^ n = 0

Proof state:
K : Type u_1
L : Type u_2
inst✝² : CommSemiring K
inst✝¹ : CommSemiring L
i : K →+* L
p : ℕ
inst✝ : IsPRadical i p
x : K
n : ℕ
h : x ^ p ^ n = 0
⊢ i x ^ p ^ n = 0

Tactic:
simpa only [map_pow, map_zero] using congr(i $h)

Result:
no goals

Proof state:
case refine_2.intro
K : Type u_1
L : Type u_2
inst✝² : CommSemiring K
inst✝¹ : CommSemiring L
i : K →+* L
p : ℕ
inst✝ : IsPRadical i p
x : K
n : ℕ
h : x ^ p ^ n = 0
⊢ ∃ n, i x ^ p ^ n = 0

Tactic:
exact ⟨n, by simpa only [map_pow, map_zero] using congr(i $h)⟩

Result:
no goals