awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
n : ℕ
k : 𝕜
hk : k ∈ σ a
⊢ k ^ n ∈ σ (a ^ n)

Tactic:
pow_image_subset a n ⟨k, ⟨hk, rfl⟩⟩

Premises used: spectrum.pow_image_subset, And.intro, Exists.intro, rfl
-- Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : IsAlgClosed 𝕜
a : A
n : ℕ
hn : 0 < n
rwa : LT.lt (α := WithBot ℕ) 0 (↑n : WithBot ℕ)
rwa₁ rwa₂ rwa₃ rwa₄ : 0 < n
⊢ 0 < (HPow.hPow (α := 𝕜[X]) X n).degree

Tactic:
rwa [degree_X_pow, Nat.cast_pos]

Premises used: Nat.cast_pos, Polynomial.degree_X_pow
-- Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : IsAlgClosed 𝕜
a : A
n : ℕ
hn : 0 < n
⊢ σ (a ^ n) = (fun (x : 𝕜) ↦ x ^ n) '' σ a

Tactic:
simpa only [aeval_X_pow, eval_X_pow]
    using map_polynomial_aeval_of_degree_pos a (X ^ n : 𝕜[X]) (by rwa [degree_X_pow, Nat.cast_pos])

Premises used: Polynomial.aeval_X_pow, Polynomial.eval_X_pow, HPow.hPow, spectrum.map_polynomial_aeval_of_degree_pos, Polynomial.X
-- Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : IsAlgClosed 𝕜
a : A
ha : (σ a).Nonempty
n : ℕ
⊢ σ (a ^ n) = (fun (x : 𝕜) ↦ x ^ n) '' σ a

Tactic:
simpa only [aeval_X_pow, eval_X_pow] using map_polynomial_aeval_of_nonempty a (X ^ n) ha

Premises used: Polynomial.aeval_X_pow, Polynomial.eval_X_pow, spectrum.map_polynomial_aeval_of_nonempty, HPow.hPow, Polynomial.X
-- Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : IsAlgClosed 𝕜
inst_4 : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
obtain : ∀ (p : 𝕜[X]) (h_mon : p.Monic) (h_eval_p : eval₂ ↑ₐ a p = 0), (σ a).Nonempty
⊢ (σ a).Nonempty

Tactic:
obtain ⟨p, ⟨h_mon, h_eval_p⟩⟩ := isIntegral_of_noetherian (IsNoetherian.iff_fg.2 I) a

Premises used: Iff.mpr, isIntegral_of_noetherian, IsNoetherian.iff_fg
-- Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : IsAlgClosed 𝕜
inst_4 : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : p.Monic
h_eval_p : eval₂ ↑ₐ a p = 0
⊢ Eq.{v + 1} (α := A) ((aeval a : (a : 𝕜[X]) → A) p : A) (0 : A)

Tactic:
rw [← aeval_def] at h_eval_p

Premises used: Polynomial.aeval_def
-- Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : IsAlgClosed 𝕜
inst_4 : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : p.Monic
h_eval_p : Eq.{v + 1} (α := A) ((aeval a : (a : 𝕜[X]) → A) p : A) (0 : A)
rw : ¬IsUnit.{v} (M := A) 0
⊢ ¬IsUnit.{v} (M := A) ((aeval a : (a : 𝕜[X]) → A) p : A)

Tactic:
rw [h_eval_p]
-- Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : IsAlgClosed 𝕜
inst_4 : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : p.Monic
h_eval_p : Eq.{v + 1} (α := A) ((aeval a : (a : 𝕜[X]) → A) p : A) (0 : A)
⊢ ¬IsUnit.{v} (M := A) 0

Tactic:
simp
-- Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : IsAlgClosed 𝕜
inst_4 : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : p.Monic
h_eval_p : eval₂ ↑ₐ a p = 0
⊢ ¬IsUnit.{v} (M := A) ((aeval a : (a : 𝕜[X]) → A) p : A)

Tactic:
have nu : ¬IsUnit (aeval a p) := by rw [← aeval_def] at h_eval_p; rw [h_eval_p]; simp
-- Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : IsAlgClosed 𝕜
inst_4 : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : p.Monic
h_eval_p : eval₂ ↑ₐ a p = 0
nu : ¬IsUnit.{v} (M := A) ((aeval a : (a : 𝕜[X]) → A) p : A)
⊢ ¬IsUnit.{v} (M := A)
      ((aeval a : (a : 𝕜[X]) → A)
          (Multiset.prod
            (Multiset.map (fun (x : 𝕜) ↦ HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) x : 𝕜[X]))
              p.roots)) :
        A)

Tactic:
rw [(IsAlgClosed.splits p).eq_prod_roots_of_monic h_mon] at nu

Premises used: Polynomial.Splits.eq_prod_roots_of_monic, IsAlgClosed.splits
-- Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : IsAlgClosed 𝕜
inst_4 : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : p.Monic
h_eval_p : eval₂ ↑ₐ a p = 0
nu :
  ¬IsUnit.{v} (M := A)
      ((aeval a : (a : 𝕜[X]) → A)
          (Multiset.prod
            (Multiset.map (fun (x : 𝕜) ↦ HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) x : 𝕜[X]))
              p.roots)) :
        A)
obtain : ∀ (k : 𝕜) (hk : k ∈ σ a), eval k p = 0 → (σ a).Nonempty
⊢ (σ a).Nonempty

Tactic:
obtain ⟨k, hk, _⟩ := exists_mem_of_not_isUnit_aeval_prod nu

Premises used: spectrum.exists_mem_of_not_isUnit_aeval_prod
-- Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : IsAlgClosed 𝕜
inst_4 : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : p.Monic
h_eval_p : eval₂ ↑ₐ a p = 0
nu :
  ¬IsUnit.{v} (M := A)
      ((aeval a : (a : 𝕜[X]) → A)
          (Multiset.prod
            (Multiset.map (fun (x : 𝕜) ↦ HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) x : 𝕜[X]))
              p.roots)) :
        A)
k : 𝕜
hk : k ∈ σ a
right : eval k p = 0
⊢ (σ a).Nonempty

Tactic:
⟨k, hk⟩

Premises used: Set.Nonempty, Exists.intro
-- Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : IsAlgClosed 𝕜
inst_4 : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : p.Monic
h_eval_p : eval₂ ↑ₐ a p = 0
nu :
  ¬IsUnit.{v} (M := A)
      ((aeval a : (a : 𝕜[X]) → A)
          (Multiset.prod
            (Multiset.map (fun (x : 𝕜) ↦ HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) x : 𝕜[X]))
              p.roots)) :
        A)
k : 𝕜
hk : k ∈ σ a
right : eval k p = 0
⊢ (σ a).Nonempty

Tactic:
exact ⟨k, hk⟩
-- Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
p : A
hp : IsIdempotentElem p
⊢ Nontrivial A

Tactic:
nontriviality A
-- Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
p : A
hp : IsIdempotentElem p
h : Nontrivial A
apply :
  Subset (α := Set 𝕜)
    ((fun (x : 𝕜) ↦ eval x (HPow.hPow (α := 𝕜[X]) (β := ℕ) X 2 - X)) ⁻¹'
      spectrum.{u_1, u_2} 𝕜 (A := A) ((aeval p : (a : 𝕜[X]) → A) (HPow.hPow (α := 𝕜[X]) (β := ℕ) X 2 - X) : A))
    {0, 1}
⊢ spectrum 𝕜 p ⊆ {0, 1}

Tactic:
apply Set.image_subset_iff.mp (spectrum.subset_polynomial_aeval p (X ^ 2 - X)) |>.trans

Premises used: HSub.hSub, HasSubset.Subset.trans, spectrum.subset_polynomial_aeval, HPow.hPow, Iff.mp, Set.image_subset_iff, OfNat.ofNat, Polynomial.X
-- Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
p : A
hp : IsIdempotentElem p
h : Nontrivial A
⊢ Subset (α := Set 𝕜)
    ((fun (x : 𝕜) ↦ eval x (HPow.hPow (α := 𝕜[X]) (β := ℕ) X 2 - X)) ⁻¹'
      spectrum.{u_1, u_2} 𝕜 (A := A) ((aeval p : (a : 𝕜[X]) → A) (HPow.hPow (α := 𝕜[X]) (β := ℕ) X 2 - X) : A))
    {0, 1}

Tactic:
fun a ha => eq_zero_or_one_of_sq_eq_self ?_

Premises used: Set.insert, Set.Mem, setOf, Set.Subset, eq_zero_or_one_of_sq_eq_self, Set.singleton
-- Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
p : A
hp : IsIdempotentElem p
h : Nontrivial A
refine :
  ∀ (a : 𝕜)
    (ha :
      Membership.mem (γ := Set 𝕜)
        ((fun (x : 𝕜) ↦ eval x (HPow.hPow (α := 𝕜[X]) (β := ℕ) X 2 - X)) ⁻¹'
          spectrum.{u_1, u_2} 𝕜 (A := A) ((aeval p : (a : 𝕜[X]) → A) (HPow.hPow (α := 𝕜[X]) (β := ℕ) X 2 - X) : A))
        a),
    HPow.hPow (β := ℕ) a 2 = a
⊢ Subset (α := Set 𝕜)
    ((fun (x : 𝕜) ↦ eval x (HPow.hPow (α := 𝕜[X]) (β := ℕ) X 2 - X)) ⁻¹'
      spectrum.{u_1, u_2} 𝕜 (A := A) ((aeval p : (a : 𝕜[X]) → A) (HPow.hPow (α := 𝕜[X]) (β := ℕ) X 2 - X) : A))
    {0, 1}

Tactic:
refine fun a ha => eq_zero_or_one_of_sq_eq_self ?_

Premises used: eq_zero_or_one_of_sq_eq_self
-- Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
p : A
hp : IsIdempotentElem p
h : Nontrivial A
a : 𝕜
ha :
  Membership.mem (γ := Set 𝕜)
    ((fun (x : 𝕜) ↦ eval x (HPow.hPow (α := 𝕜[X]) (β := ℕ) X 2 - X)) ⁻¹'
      spectrum.{u_1, u_2} 𝕜 (A := A) ((aeval p : (a : 𝕜[X]) → A) (HPow.hPow (α := 𝕜[X]) (β := ℕ) X 2 - X) : A))
    a
⊢ HPow.hPow (β := ℕ) a 2 = a

Tactic:
simpa [pow_two p, hp.eq, sub_eq_zero] using ha

Premises used: pow_two, sub_eq_zero, IsIdempotentElem.eq
-- Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
p : A
hp : IsIdempotentElem p
⊢ Ne.{u_1 + 1} (α := 𝕜) 0 1

Tactic:
simp
-- Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : NonUnitalRing A
inst_2 : Module 𝕜 A
inst_3 : IsScalarTower 𝕜 A A
inst_4 : SMulCommClass 𝕜 A A
p : A
hp : IsIdempotentElem p
⊢ quasispectrum 𝕜 p ⊆ {0, 1}

Tactic:
quasispectrum_eq_spectrum_inr' 𝕜 𝕜 p ▸ (hp.inr _ |>.spectrum_subset _)

Premises used: IsIdempotentElem.spectrum_subset, Eq.rec, Unitization.quasispectrum_eq_spectrum_inr', Eq.symm
-- Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : NonUnitalRing A
inst_2 : Module 𝕜 A
inst_3 : IsScalarTower 𝕜 A A
inst_4 : SMulCommClass 𝕜 A A
p : A
hp : IsIdempotentElem p
⊢ Ne.{u_1 + 1} (α := 𝕜) 0 1

Tactic:
simp
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
pos : ∀ (hp : 1 < p), LE.le (α := Ideal R) (pNilradical R p) (nilradical R)
neg : ∀ (hp : ¬1 < p), LE.le (α := Ideal R) (pNilradical R p) (nilradical R)
⊢ LE.le (α := Ideal R) (pNilradical R p) (nilradical R)

Tactic:
by_cases hp : 1 < p
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : 1 < p
pos : LE.le (α := Ideal R) (if 1 < p then nilradical R else ⊥) (nilradical R)
pos₁ pos₂ : LE.le (α := Ideal R) (nilradical R) (nilradical R)
⊢ LE.le (α := Ideal R) (pNilradical R p) (nilradical R)

Tactic:
rw [pNilradical, if_pos hp]

Premises used: pNilradical, if_pos
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : ¬1 < p
neg : LE.le (α := Ideal R) (if 1 < p then nilradical R else ⊥) (nilradical R)
neg₁ : LE.le (α := Ideal R) ⊥ (nilradical R)
⊢ LE.le (α := Ideal R) (pNilradical R p) (nilradical R)

Tactic:
simp_rw [pNilradical, if_neg hp, bot_le]

Premises used: pNilradical, if_neg, bot_le
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : 1 < p
rw : Eq (α := Ideal R) (if 1 < p then nilradical R else ⊥) (nilradical R)
rw₁ rw₂ : Eq (α := Ideal R) (nilradical R) (nilradical R)
⊢ Eq (α := Ideal R) (pNilradical R p) (nilradical R)

Tactic:
rw [pNilradical, if_pos hp]

Premises used: pNilradical, if_pos
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : ¬1 < p
rw : Eq (α := Ideal R) (if 1 < p then nilradical R else ⊥) ⊥
rw₁ rw₂ : Eq.{u_1 + 1} (α := Ideal R) ⊥ ⊥
⊢ Eq (α := Ideal R) (pNilradical R p) ⊥

Tactic:
rw [pNilradical, if_neg hp]

Premises used: pNilradical, if_neg
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : p ≤ 1
⊢ Eq (α := Ideal R) (pNilradical R p) ⊥

Tactic:
pNilradical_eq_bot (not_lt.2 hp)

Premises used: Iff.mpr, pNilradical_eq_bot, not_lt
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : Nat.Prime p
⊢ Eq (α := Ideal R) (pNilradical R p) (nilradical R)

Tactic:
pNilradical_eq_nilradical hp.one_lt

Premises used: Nat.Prime.one_lt, pNilradical_eq_nilradical
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
R : Type u_1
inst : CommSemiring R
⊢ Eq (α := Ideal R) (pNilradical R 1) ⊥

Tactic:
pNilradical_eq_bot' rfl.le

Premises used: Eq.le, pNilradical_eq_bot', rfl
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
x : R
pos : ∀ (hp : 1 < p), Membership.mem (γ := Ideal R) (pNilradical R p) x ↔ ∃ (n : ℕ), x ^ p ^ n = 0
neg : ∀ (hp : ¬1 < p), Membership.mem (γ := Ideal R) (pNilradical R p) x ↔ ∃ (n : ℕ), x ^ p ^ n = 0
⊢ Membership.mem (γ := Ideal R) (pNilradical R p) x ↔ ∃ (n : ℕ), x ^ p ^ n = 0

Tactic:
by_cases hp : 1 < p
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
x : R
hp : 1 < p
pos : Membership.mem (γ := Ideal R) (nilradical R) x ↔ ∃ (n : ℕ), x ^ p ^ n = 0
⊢ Membership.mem (γ := Ideal R) (pNilradical R p) x ↔ ∃ (n : ℕ), x ^ p ^ n = 0

Tactic:
rw [pNilradical_eq_nilradical hp]

Premises used: pNilradical_eq_nilradical
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
x : R
hp : 1 < p
⊢ Membership.mem (γ := Ideal R) (nilradical R) x ↔ ∃ (n : ℕ), x ^ p ^ n = 0

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

Premises used: Membership.mem, Exists, _private.0.mem_pNilradical.match_2, HPow.hPow, Iff.intro, Exists.intro, OfNat.ofNat, _private.0.mem_pNilradical.match_1, Eq, nilradical
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
x : R
hp : 1 < p
pos :
  Membership.mem (γ := Ideal R) (nilradical R) x →
    ∀ (n : ℕ) (h : Membership.mem (γ := Ideal R) 0 (x ^ n)), x ^ p ^ n = 0
⊢ Membership.mem (γ := Ideal R) (nilradical R) x ↔ ∃ (n : ℕ), x ^ p ^ n = 0

Tactic:
refine ⟨fun ⟨n, h⟩ ↦ ⟨n, ?_⟩, fun ⟨n, h⟩ ↦ ⟨p ^ n, h⟩⟩
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
x : R
hp : 1 < p
h_1 : Membership.mem (γ := Ideal R) (nilradical R) x
n : ℕ
h : Membership.mem (γ := Ideal R) 0 (x ^ n)
pos : x ^ (p ^ n - n + n) = 0
pos₁ : x ^ (p ^ n - n) * x ^ n = 0
pos₂ : x ^ (p ^ n - n) * 0 = 0
pos₃ pos₄ : Eq.{u_1 + 1} (α := R) 0 0
⊢ x ^ p ^ n = 0

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

Premises used: Nat.lt_pow_self, pow_add, LT.lt.le, MulZeroClass.mul_zero, Nat.sub_add_cancel
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
x : R
hp : ¬1 < p
neg : x = 0 ↔ ∃ (n : ℕ), x ^ p ^ n = 0
⊢ Membership.mem (γ := Ideal R) (pNilradical R p) x ↔ ∃ (n : ℕ), x ^ p ^ n = 0

Tactic:
rw [pNilradical_eq_bot hp, Ideal.mem_bot]

Premises used: Ideal.mem_bot, pNilradical_eq_bot
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
x : R
hp : ¬1 < p
h : x = 0
rw : HPow.hPow (β := ℕ) x 1 = 0
rw₁ : x = 0
rw₂ rw₃ : Eq.{u_1 + 1} (α := R) 0 0
⊢ x ^ HPow.hPow (β := ℕ) p 0 = 0

Tactic:
rw [pow_zero, pow_one, h]

Premises used: pow_zero, pow_one
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
x : R
hp : ¬1 < p
neg : (∃ (n : ℕ), x ^ p ^ n = 0) → ∀ (n : ℕ) (h : x ^ p ^ n = 0), x = 0
⊢ x = 0 ↔ ∃ (n : ℕ), x ^ p ^ n = 0

Tactic:
refine ⟨fun h ↦ ⟨0, by rw [pow_zero, pow_one, h]⟩, fun ⟨n, h⟩ ↦ ?_⟩
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
x : R
hp : ¬1 < p
h_1 : ∃ (n : ℕ), x ^ p ^ n = 0
n : ℕ
h : x ^ p ^ n = 0
neg : ∀ (hp : p = 0), x = 0
neg₁ : ∀ (hp : p = 1), x = 0
⊢ x = 0

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

Premises used: Nat.le_one_iff_eq_zero_or_eq_one, not_lt, Iff.mp
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
x : R
hp_1 : ¬1 < p
h_1 : ∃ (n : ℕ), x ^ p ^ n = 0
n : ℕ
h : x ^ p ^ n = 0
hp : p = 0
pos : ∀ (hn : n = 0), x = 0
neg : ∀ (hn : ¬n = 0), x = 0
⊢ x = 0

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
x : R
hp_1 : ¬1 < p
h_1 : ∃ (n : ℕ), x ^ p ^ n = 0
n : ℕ
h : x ^ p ^ n = 0
hp : p = 0
hn : n = 0
pos : ∀ (h : x ^ HPow.hPow (β := ℕ) p 0 = 0) (hp : p = 0) (hn : n = 0), x = 0
pos₁ : ∀ (h : HPow.hPow (β := ℕ) x 1 = 0) (hp : p = 0) (hn : n = 0), x = 0
pos₂ pos₃ pos₄ pos₅ : ∀ (h : x = 0) (hp : p = 0) (hn : n = 0), x = 0
⊢ x = 0

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

Premises used: pow_zero, pow_one
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
x : R
hp_1 : ¬1 < p
h_1 : ∃ (n : ℕ), x ^ p ^ n = 0
n : ℕ
h : x ^ p ^ n = 0
hp : p = 0
hn : ¬n = 0
⊢ Eq.{u_1 + 1} (α := R) 1 0

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

Premises used: pow_zero, zero_pow
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
x : R
hp_1 : ¬1 < p
h_1 : ∃ (n : ℕ), x ^ p ^ n = 0
n : ℕ
h : x ^ p ^ n = 0
hp : p = 0
hn : ¬n = 0
h₁ : Eq.{u_1 + 1} (α := R) 1 0
⊢ p = 0

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

Premises used: pow_zero, zero_pow
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
x : R
hp_1 : ¬1 < p
h_1 : ∃ (n : ℕ), x ^ p ^ n = 0
n : ℕ
h : x ^ p ^ n = 0
hp : p = 0
hn : ¬n = 0
h₁ : Eq.{u_1 + 1} (α := R) 1 0
hp₁ : p = 0
⊢ ¬n = 0

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

Premises used: pow_zero, zero_pow
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
x : R
hp_1 : ¬1 < p
h_1 : ∃ (n : ℕ), x ^ p ^ n = 0
n : ℕ
h : Eq.{u_1 + 1} (α := R) 1 0
hp : p = 0
hn : ¬n = 0
⊢ x = 0

Tactic:
subsingleton [subsingleton_of_zero_eq_one h.symm]

Premises used: subsingleton_of_zero_eq_one, Eq.symm
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
x : R
hp_1 : ¬1 < p
h_1 : ∃ (n : ℕ), x ^ p ^ n = 0
n : ℕ
h : x ^ p ^ n = 0
hp : p = 1
neg : ∀ (h : x ^ HPow.hPow (α := ℕ) 1 n = 0) (hp : p = 1), x = 0
neg₁ : ∀ (h : HPow.hPow (β := ℕ) x 1 = 0) (hp : p = 1), x = 0
neg₂ neg₃ neg₄ neg₅ : ∀ (h : x = 0) (hp : p = 1), x = 0
⊢ x = 0

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

Premises used: one_pow, pow_one
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
inst_1 : ExpChar R p
x y : R
simp_rw : (∃ (n : ℕ), (x - y) ^ p ^ n = 0) ↔ ∃ (n : ℕ), x ^ p ^ n = y ^ p ^ n
simp_rw₁ : (∃ (n : ℕ), x ^ p ^ n - y ^ p ^ n = 0) ↔ ∃ (n : ℕ), x ^ p ^ n = y ^ p ^ n
⊢ Membership.mem (γ := Ideal R) (pNilradical R p) (x - y) ↔ ∃ (n : ℕ), x ^ p ^ n = y ^ p ^ n

Tactic:
simp_rw [mem_pNilradical, sub_pow_expChar_pow, sub_eq_zero]

Premises used: sub_eq_zero, mem_pNilradical, sub_pow_expChar_pow
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
inst_1 : ExpChar R p
h : Eq (α := Ideal R) (pNilradical R p) ⊥
n : ℕ
⊢ Function.Injective (β := R) fun (x : R) ↦ x ^ p ^ n

Tactic:
fun _ _ H ↦
  sub_eq_zero.1 <| Ideal.mem_bot.1 <| h ▸ sub_mem_pNilradical_iff_pow_expChar_pow_eq.2 ⟨n, H⟩

Premises used: Ideal.mem_bot, Iff.mpr, sub_eq_zero, sub_mem_pNilradical_iff_pow_expChar_pow_eq, Eq.rec, Exists.intro, Iff.mp, Function.Injective
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
h : Function.Injective (α := R) (β := R) (⇑(frobenius R p) : (a : R) → R)
x : R
rw : (∃ (n : ℕ), x ^ p ^ n = 0) → x = 0
⊢ Membership.mem (γ := Submodule R R) (pNilradical R p) x → Membership.mem (γ := Submodule R R) ⊥ x

Tactic:
rw [mem_pNilradical, Ideal.mem_bot]

Premises used: Ideal.mem_bot, mem_pNilradical
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
h : Function.Injective (α := R) (β := R) (⇑(frobenius R p) : (a : R) → R)
x : R
h_1 : ∃ (n : ℕ), x ^ p ^ n = 0
n : ℕ
h_2 : x ^ p ^ n = 0
rwa : Eq (α := R) ((iterateFrobenius R p n : (a : R) → R) x : R) ((iterateFrobenius R p n : (a : R) → R) 0 : R)
rwa₁ rwa₂ rwa₃ rwa₄ : Eq (α := R) ((iterateFrobenius R p n : (a : R) → R) x : R) (0 : R)
⊢ (⇑(frobenius R p) : (a : R) → R)^[n] x = (⇑(frobenius R p) : (a : R) → R)^[n] 0

Tactic:
rwa [← coe_iterateFrobenius, map_zero]

Premises used: map_zero, coe_iterateFrobenius
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
h : Function.Injective (α := R) (β := R) (⇑(frobenius R p) : (a : R) → R)
x : R
⊢ (∃ (n : ℕ), x ^ p ^ n = 0) → x = 0

Tactic:
exact fun ⟨n, _⟩ ↦ h.iterate n (by rwa [← coe_iterateFrobenius, map_zero])
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
⊢ Eq (α := Ideal R) (pNilradical R p) ⊥

Tactic:
pNilradical_eq_bot_of_frobenius_inj R p (injective_frobenius R p)

Premises used: injective_frobenius, pNilradical_eq_bot_of_frobenius_inj
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
inst : CommSemiring K
inst_1 : CommSemiring L
i : K →+* L
p : ℕ
inst_2 : IsPRadical i p
x : L
⊢ ∃ (n : ℕ) (y : K), (i : (a : K) → L) y = x ^ p ^ n

Tactic:
pow_mem' x

Premises used: IsPRadical.pow_mem'
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
inst : CommSemiring K
inst_1 : CommSemiring L
i : K →+* L
p : ℕ
inst_2 : IsPRadical i p
⊢ LE.le (α := Ideal K) (RingHom.ker i) (pNilradical K p)

Tactic:
ker_le'

Premises used: IsPRadical.ker_le'
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
inst : CommSemiring K
inst_1 : CommSemiring L
i : K →+* L
p : ℕ
inst_2 : IsPRadical i p
⊢ Eq (α := Ideal K) (Ideal.comap i (pNilradical L p)) (pNilradical K p)

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

Premises used: Iff.mpr, le_antisymm, mem_pNilradical
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
inst : CommSemiring K
inst_1 : CommSemiring L
i : K →+* L
p : ℕ
inst_2 : IsPRadical i p
refine_1 :
  ∀ (x : K) (h : Membership.mem (γ := Submodule K K) (Ideal.comap i (pNilradical L p)) x), ∃ (n : ℕ), x ^ p ^ n = 0
refine_2 :
  ∀ (x : K) (h : Membership.mem (γ := Submodule K K) (pNilradical K p) x),
    Membership.mem (γ := Submodule K K) (Ideal.comap i (pNilradical L p)) x
⊢ Eq (α := Ideal K) (Ideal.comap i (pNilradical L p)) (pNilradical K p)

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

Premises used: le_antisymm
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
inst : CommSemiring K
inst_1 : CommSemiring L
i : K →+* L
p : ℕ
inst_2 : IsPRadical i p
x : K
h : Membership.mem (γ := Submodule K K) (Ideal.comap i (pNilradical L p)) x
refine_1 : ∀ (n : ℕ) (h : HPow.hPow (α := L) ((i : (a : K) → L) x : L) (p ^ n) = 0), ∃ (n : ℕ), x ^ p ^ n = 0
⊢ ∃ (n : ℕ), x ^ p ^ n = 0

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

Premises used: mem_pNilradical, Iff.mp, Ideal.mem_comap
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
inst : CommSemiring K
inst_1 : CommSemiring L
i : K →+* L
p : ℕ
inst_2 : IsPRadical i p
x : K
h_1 : Membership.mem (γ := Submodule K K) (Ideal.comap i (pNilradical L p)) x
n : ℕ
h : HPow.hPow (α := L) ((i : (a : K) → L) x : L) (p ^ n) = 0
refine_1 : ∀ (m : ℕ) (h : (x ^ p ^ n) ^ p ^ m = 0), ∃ (n : ℕ), 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)

Premises used: IsPRadical.ker_le, mem_pNilradical, Iff.mp
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
inst : CommSemiring K
inst_1 : CommSemiring L
i : K →+* L
p : ℕ
inst_2 : IsPRadical i p
x : K
h_1 : Membership.mem (γ := Submodule K K) (Ideal.comap i (pNilradical L p)) x
n : ℕ
h_2 : HPow.hPow (α := L) ((i : (a : K) → L) x : L) (p ^ n) = 0
m : ℕ
h : (x ^ p ^ n) ^ p ^ m = 0
rwa : x ^ (p ^ n * p ^ m) = 0
rwa₁ rwa₂ rwa₃ rwa₄ : (x ^ p ^ n) ^ p ^ m = 0
⊢ x ^ p ^ (n + m) = 0

Tactic:
rwa [pow_add, pow_mul]

Premises used: pow_add, pow_mul