awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Spectrum (hypothesis)
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < p.degree
k : 𝕜
hk : k ∈ spectrum.{u, v} 𝕜 (A := A) ((aeval a : (a : 𝕜[X]) → A) p : A)
hprod :
  HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p =
    HMul.hMul (α := 𝕜[X]) (β := 𝕜[X])
      ((C : (a : 𝕜) → 𝕜[X]) (HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p).leadingCoeff : 𝕜[X])
      (Multiset.prod
          (Multiset.map (fun (x : 𝕜) ↦ HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) x : 𝕜[X]))
            (HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p).roots) :
        𝕜[X])
h_ne : HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p ≠ 0
lead_ne : (HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p).leadingCoeff ≠ 0
lead_unit :
  IsUnit.{v} (M := A)
    (↑(((Units.map (↑↑ₐ : 𝕜 →* A) : MonoidHom.{u, v} 𝕜ˣ Aˣ) : (a : 𝕜ˣ) → Aˣ)
          (Units.mk0 (HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p).leadingCoeff lead_ne)) :
      A)
⊢ Membership.mem (γ := Set 𝕜) ((fun (x : 𝕜) ↦ eval x p) '' σ a) k
have p_a_eq : (aeval a : (a : 𝕜[X]) → A) (HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p) =
  HSub.hSub (α := A) (β := A) ((↑ₐ : (a : 𝕜) → A) k : A) ((aeval a : (a : 𝕜[X]) → A) p : A)
Tactic: have p_a_eq : aeval a (C k - p) = ↑ₐ k - aeval a p := by
    simp only [aeval_C, map_sub]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Spectrum (hypothesis)
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < p.degree
k : 𝕜
hk : k ∈ spectrum.{u, v} 𝕜 (A := A) ((aeval a : (a : 𝕜[X]) → A) p : A)
hprod :
  HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p =
    HMul.hMul (α := 𝕜[X]) (β := 𝕜[X])
      ((C : (a : 𝕜) → 𝕜[X]) (HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p).leadingCoeff : 𝕜[X])
      (Multiset.prod
          (Multiset.map (fun (x : 𝕜) ↦ HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) x : 𝕜[X]))
            (HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p).roots) :
        𝕜[X])
h_ne : HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p ≠ 0
lead_ne : (HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p).leadingCoeff ≠ 0
lead_unit :
  IsUnit.{v} (M := A)
    (↑(((Units.map (↑↑ₐ : 𝕜 →* A) : MonoidHom.{u, v} 𝕜ˣ Aˣ) : (a : 𝕜ˣ) → Aˣ)
          (Units.mk0 (HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p).leadingCoeff lead_ne)) :
      A)
p_a_eq :
  (aeval a : (a : 𝕜[X]) → A) (HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p) =
    HSub.hSub (α := A) (β := A) ((↑ₐ : (a : 𝕜) → A) k : A) ((aeval a : (a : 𝕜[X]) → A) p : A)
⊢ Membership.mem (γ := Set 𝕜) ((fun (x : 𝕜) ↦ eval x p) '' σ a) k
have hk₁ : ¬(IsUnit.{v} (M := A) ((↑ₐ : (a : 𝕜) → A) (HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p).leadingCoeff : 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]))
              (HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p).roots)) :
        A))
Tactic: rw [mem_iff, ← p_a_eq, hprod, aeval_mul,
    ((Commute.all _ _).map (aeval a : 𝕜[X] →ₐ[𝕜] A)).isUnit_mul_iff, aeval_C] at hk
Cleared hypotheses: hk, hprod, h_ne, lead_ne, lead_unit, p_a_eq
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Spectrum (hypothesis)
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < p.degree
k : 𝕜
hk :
  ¬(IsUnit.{v} (M := A)
        ((↑ₐ : (a : 𝕜) → A) (HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p).leadingCoeff : 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]))
                (HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p).roots)) :
          A))
hprod :
  HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p =
    HMul.hMul (α := 𝕜[X]) (β := 𝕜[X])
      ((C : (a : 𝕜) → 𝕜[X]) (HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p).leadingCoeff : 𝕜[X])
      (Multiset.prod
          (Multiset.map (fun (x : 𝕜) ↦ HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) x : 𝕜[X]))
            (HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p).roots) :
        𝕜[X])
h_ne : HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p ≠ 0
lead_ne : (HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p).leadingCoeff ≠ 0
lead_unit :
  IsUnit.{v} (M := A)
    (↑(((Units.map (↑↑ₐ : 𝕜 →* A) : MonoidHom.{u, v} 𝕜ˣ Aˣ) : (a : 𝕜ˣ) → Aˣ)
          (Units.mk0 (HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p).leadingCoeff lead_ne)) :
      A)
p_a_eq :
  (aeval a : (a : 𝕜[X]) → A) (HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p) =
    HSub.hSub (α := A) (β := A) ((↑ₐ : (a : 𝕜) → A) k : A) ((aeval a : (a : 𝕜[X]) → A) p : A)
⊢ Membership.mem (γ := Set 𝕜) ((fun (x : 𝕜) ↦ eval x p) '' σ a) k
have hk₁ : ∃ k_1 ∈ σ a, eval k_1 (HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p) = 0
Tactic: replace hk := exists_mem_of_not_isUnit_aeval_prod (not_and.mp hk lead_unit)
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Spectrum (goal)
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < p.degree
k : 𝕜
hprod :
  HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p =
    HMul.hMul (α := 𝕜[X]) (β := 𝕜[X])
      ((C : (a : 𝕜) → 𝕜[X]) (HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p).leadingCoeff : 𝕜[X])
      (Multiset.prod
          (Multiset.map (fun (x : 𝕜) ↦ HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) x : 𝕜[X]))
            (HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p).roots) :
        𝕜[X])
h_ne : HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p ≠ 0
lead_ne : (HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p).leadingCoeff ≠ 0
lead_unit :
  IsUnit.{v} (M := A)
    (↑(((Units.map (↑↑ₐ : 𝕜 →* A) : MonoidHom.{u, v} 𝕜ˣ Aˣ) : (a : 𝕜ˣ) → Aˣ)
          (Units.mk0 (HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p).leadingCoeff lead_ne)) :
      A)
p_a_eq :
  (aeval a : (a : 𝕜[X]) → A) (HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p) =
    HSub.hSub (α := A) (β := A) ((↑ₐ : (a : 𝕜) → A) k : A) ((aeval a : (a : 𝕜[X]) → A) p : A)
hk : ∃ k_1 ∈ σ a, eval k_1 (HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p) = 0
⊢ Membership.mem (γ := Set 𝕜) ((fun (x : 𝕜) ↦ eval x p) '' σ a) k
have rcases : ∀ (r : 𝕜) (r_mem : r ∈ σ a) (r_ev : eval r (HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p) = 0),
  Membership.mem (γ := Set 𝕜) ((fun (x : 𝕜) ↦ eval x p) '' σ a) k
Tactic: rcases hk with ⟨r, r_mem, r_ev⟩
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Spectrum (hypothesis)
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hnon : (σ a).Nonempty
⊢ spectrum.{u, v} 𝕜 (A := A) ((aeval a : (a : 𝕜[X]) → A) p : A) = (fun (k : 𝕜) ↦ eval k p) '' σ a
have a₁ : Nontrivial A
Tactic: nontriviality A
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Spectrum (hypothesis)
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hnon : (σ a).Nonempty
h : Nontrivial A
⊢ spectrum.{u, v} 𝕜 (A := A) ((aeval a : (a : 𝕜[X]) → A) p : A) = (fun (k : 𝕜) ↦ eval k p) '' σ a
have h : p.degree ≤ 0
Tactic: refine Or.elim (le_or_gt (degree p) 0) (fun h => ?_) (map_polynomial_aeval_of_degree_pos a p)
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Spectrum (goal)
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hnon : (σ a).Nonempty
h_1 : Nontrivial A
h : p.degree ≤ 0
⊢ spectrum.{u, v} 𝕜 (A := A) ((aeval a : (a : 𝕜[X]) → A) p : A) = (fun (k : 𝕜) ↦ eval k p) '' σ a
have rw : spectrum.{u, v} 𝕜 (A := A) ((aeval a : (a : 𝕜[X]) → A) ((C : (a : 𝕜) → 𝕜[X]) (p.coeff 0) : 𝕜[X]) : A) =
  (fun (k : 𝕜) ↦ eval k ((C : (a : 𝕜) → 𝕜[X]) (p.coeff 0))) '' σ a
Tactic: rw [eq_C_of_degree_le_zero h]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Spectrum (goal)
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
⊢ 0 < (HPow.hPow (α := 𝕜[X]) X n).degree
have rwa : LT.lt (α := WithBot ℕ) 0 (↑n : WithBot ℕ)
Tactic: rwa [degree_X_pow, Nat.cast_pos]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Spectrum (goal)
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
⊢ (σ a).Nonempty
have obtain : ∀ (p : 𝕜[X]) (h_mon : p.Monic) (h_eval_p : eval₂ ↑ₐ a p = 0), (σ a).Nonempty
Tactic: obtain ⟨p, ⟨h_mon, h_eval_p⟩⟩ := isIntegral_of_noetherian (IsNoetherian.iff_fg.2 I) a
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Spectrum (hypothesis)
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)
have h_eval_p₁ : Eq.{v + 1} (α := A) ((aeval a : (a : 𝕜[X]) → A) p : A) (0 : A)
Tactic: rw [← aeval_def] at h_eval_p
Cleared hypotheses: h_eval_p
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Spectrum (goal)
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) ((aeval a : (a : 𝕜[X]) → A) p : A)
have rw : ¬IsUnit.{v} (M := A) 0
Tactic: rw [h_eval_p]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Spectrum (hypothesis)
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
⊢ (σ a).Nonempty
have nu : ¬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
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Spectrum (hypothesis)
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)
⊢ (σ a).Nonempty
have 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)
Tactic: rw [(IsAlgClosed.splits p).eq_prod_roots_of_monic h_mon] at nu
Cleared hypotheses: nu
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Spectrum (goal)
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)
⊢ (σ a).Nonempty
have obtain : ∀ (k : 𝕜) (hk : k ∈ σ a), eval k p = 0 → (σ a).Nonempty
Tactic: obtain ⟨k, hk, _⟩ := exists_mem_of_not_isUnit_aeval_prod nu
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Spectrum (hypothesis)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
p : A
hp : IsIdempotentElem p
⊢ spectrum 𝕜 p ⊆ {0, 1}
have a : Nontrivial A
Tactic: nontriviality A
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Spectrum (goal)
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
⊢ spectrum 𝕜 p ⊆ {0, 1}
have 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}
Tactic: apply Set.image_subset_iff.mp (spectrum.subset_polynomial_aeval p (X ^ 2 - X)) |>.trans
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Spectrum (goal)
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}
have 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
Tactic: refine fun a ha => eq_zero_or_one_of_sq_eq_self ?_
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
⊢ LE.le (α := Ideal R) (pNilradical R p) (nilradical R)
have pos : ∀ (hp : 1 < p), LE.le (α := Ideal R) (pNilradical R p) (nilradical R)
Tactic: by_cases hp : 1 < p
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
pos : ∀ (hp : 1 < p), LE.le (α := Ideal R) (pNilradical R p) (nilradical R)
⊢ LE.le (α := Ideal R) (pNilradical R p) (nilradical R)
have neg : ∀ (hp : ¬1 < p), LE.le (α := Ideal R) (pNilradical R p) (nilradical R)
Tactic: by_cases hp : 1 < p
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : 1 < p
⊢ LE.le (α := Ideal R) (pNilradical R p) (nilradical R)
have pos : LE.le (α := Ideal R) (if 1 < p then nilradical R else ⊥) (nilradical R)
Tactic: rw [pNilradical, if_pos hp]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
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)
⊢ LE.le (α := Ideal R) (pNilradical R p) (nilradical R)
have pos₁ : LE.le (α := Ideal R) (nilradical R) (nilradical R)
Tactic: rw [pNilradical, if_pos hp]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : ¬1 < p
⊢ LE.le (α := Ideal R) (pNilradical R p) (nilradical R)
have neg : LE.le (α := Ideal R) (if 1 < p then nilradical R else ⊥) (nilradical R)
Tactic: simp_rw [pNilradical, if_neg hp, bot_le]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
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)
⊢ LE.le (α := Ideal R) (pNilradical R p) (nilradical R)
have neg₁ : LE.le (α := Ideal R) ⊥ (nilradical R)
Tactic: simp_rw [pNilradical, if_neg hp, bot_le]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : 1 < p
⊢ Eq (α := Ideal R) (pNilradical R p) (nilradical R)
have rw : Eq (α := Ideal R) (if 1 < p then nilradical R else ⊥) (nilradical R)
Tactic: rw [pNilradical, if_pos hp]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
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)
⊢ Eq (α := Ideal R) (pNilradical R p) (nilradical R)
have rw₁ : Eq (α := Ideal R) (nilradical R) (nilradical R)
Tactic: rw [pNilradical, if_pos hp]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : ¬1 < p
⊢ Eq (α := Ideal R) (pNilradical R p) ⊥
have rw : Eq (α := Ideal R) (if 1 < p then nilradical R else ⊥) ⊥
Tactic: rw [pNilradical, if_neg hp]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : ¬1 < p
rw : Eq (α := Ideal R) (if 1 < p then nilradical R else ⊥) ⊥
⊢ Eq (α := Ideal R) (pNilradical R p) ⊥
have rw₁ : Eq.{u_1 + 1} (α := Ideal R) ⊥ ⊥
Tactic: rw [pNilradical, if_neg hp]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
x : R
⊢ Membership.mem (γ := Ideal R) (pNilradical R p) x ↔ ∃ (n : ℕ), x ^ p ^ n = 0
have pos : ∀ (hp : 1 < p), Membership.mem (γ := Ideal R) (pNilradical R p) x ↔ ∃ (n : ℕ), x ^ p ^ n = 0
Tactic: by_cases hp : 1 < p
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
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
⊢ Membership.mem (γ := Ideal R) (pNilradical R p) x ↔ ∃ (n : ℕ), x ^ p ^ n = 0
have neg : ∀ (hp : ¬1 < p), Membership.mem (γ := Ideal R) (pNilradical R p) x ↔ ∃ (n : ℕ), x ^ p ^ n = 0
Tactic: by_cases hp : 1 < p
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
x : R
hp : 1 < p
⊢ Membership.mem (γ := Ideal R) (pNilradical R p) x ↔ ∃ (n : ℕ), x ^ p ^ n = 0
have pos : Membership.mem (γ := Ideal R) (nilradical R) x ↔ ∃ (n : ℕ), x ^ p ^ n = 0
Tactic: rw [pNilradical_eq_nilradical hp]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
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
have pos : Membership.mem (γ := Ideal R) (nilradical R) x → ∀ (n : ℕ) (h : Membership.mem (γ := Ideal R) 0 (x ^ n)), x ^ p ^ n = 0
Tactic: refine ⟨fun ⟨n, h⟩ ↦ ⟨n, ?_⟩, fun ⟨n, h⟩ ↦ ⟨p ^ n, h⟩⟩
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
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)
⊢ x ^ p ^ n = 0
have pos : x ^ (p ^ n - n + n) = 0
Tactic: rw [← Nat.sub_add_cancel ((n.lt_pow_self hp).le), pow_add, h, mul_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
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
⊢ x ^ p ^ n = 0
have pos₁ : x ^ (p ^ n - n) * x ^ n = 0
Tactic: rw [← Nat.sub_add_cancel ((n.lt_pow_self hp).le), pow_add, h, mul_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
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
⊢ x ^ p ^ n = 0
have pos₂ : x ^ (p ^ n - n) * 0 = 0
Tactic: rw [← Nat.sub_add_cancel ((n.lt_pow_self hp).le), pow_add, h, mul_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
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
⊢ x ^ p ^ n = 0
have pos₃ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [← Nat.sub_add_cancel ((n.lt_pow_self hp).le), pow_add, h, mul_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
x : R
hp : ¬1 < p
⊢ Membership.mem (γ := Ideal R) (pNilradical R p) x ↔ ∃ (n : ℕ), x ^ p ^ n = 0
have neg : x = 0 ↔ ∃ (n : ℕ), x ^ p ^ n = 0
Tactic: rw [pNilradical_eq_bot hp, Ideal.mem_bot]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
x : R
hp : ¬1 < p
h : x = 0
⊢ x ^ HPow.hPow (β := ℕ) p 0 = 0
have rw : HPow.hPow (β := ℕ) x 1 = 0
Tactic: rw [pow_zero, pow_one, h]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
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
⊢ x ^ HPow.hPow (β := ℕ) p 0 = 0
have rw₂ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [pow_zero, pow_one, h]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
x : R
hp : ¬1 < p
⊢ x = 0 ↔ ∃ (n : ℕ), x ^ p ^ n = 0
have neg : (∃ (n : ℕ), x ^ p ^ n = 0) → ∀ (n : ℕ) (h : x ^ p ^ n = 0), x = 0
Tactic: refine ⟨fun h ↦ ⟨0, by rw [pow_zero, pow_one, h]⟩, fun ⟨n, h⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
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
⊢ x = 0
have neg : ∀ (hp : p = 0), x = 0
Tactic: rcases Nat.le_one_iff_eq_zero_or_eq_one.1 (not_lt.1 hp) with hp | hp
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
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
⊢ x = 0
have neg₁ : ∀ (hp : p = 1), x = 0
Tactic: rcases Nat.le_one_iff_eq_zero_or_eq_one.1 (not_lt.1 hp) with hp | hp
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
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
⊢ x = 0
have pos : ∀ (hn : n = 0), x = 0
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
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
⊢ x = 0
have neg : ∀ (hn : ¬n = 0), x = 0
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
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
⊢ x = 0
have pos : ∀ (h : x ^ HPow.hPow (β := ℕ) p 0 = 0) (hp : p = 0) (hn : n = 0), x = 0
Tactic: rwa [hn, pow_zero, pow_one] at h
Cleared hypotheses: h, hp, hn
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
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
⊢ x = 0
have pos₁ : ∀ (h : HPow.hPow (β := ℕ) x 1 = 0) (hp : p = 0) (hn : n = 0), x = 0
Tactic: rwa [hn, pow_zero, pow_one] at h
Cleared hypotheses: h, hp, hn
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
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
⊢ x = 0
have pos₂ : ∀ (h : x = 0) (hp : p = 0) (hn : n = 0), x = 0
Tactic: rwa [hn, pow_zero, pow_one] at h
Cleared hypotheses: h, hp, hn
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (hypothesis)
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
⊢ x = 0
have h₁ : Eq.{u_1 + 1} (α := R) 1 0
Tactic: rw [hp, zero_pow hn, pow_zero] at h
Cleared hypotheses: h, hp, hn
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
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
⊢ x = 0
have neg : ∀ (h : x ^ HPow.hPow (α := ℕ) 1 n = 0) (hp : p = 1), x = 0
Tactic: rwa [hp, one_pow, pow_one] at h
Cleared hypotheses: h, hp