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
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)
⊢ ¬(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

Premises used: Polynomial.aeval_mul, spectrum.mem_iff, Polynomial.aeval_C, Commute.isUnit_mul_iff, Commute.map, Polynomial.aeval, Commute.all
-- 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
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)
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))
⊢ 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])

Tactic:
rw [mem_iff, ← p_a_eq, hprod, aeval_mul,
    ((Commute.all _ _).map (aeval a : 𝕜[X] →ₐ[𝕜] A)).isUnit_mul_iff, aeval_C] at hk

Premises used: Polynomial.aeval_mul, spectrum.mem_iff, Polynomial.aeval_C, Commute.isUnit_mul_iff, Commute.map, Polynomial.aeval, Commute.all
-- 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
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)
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])
⊢ HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p ≠ 0

Tactic:
rw [mem_iff, ← p_a_eq, hprod, aeval_mul,
    ((Commute.all _ _).map (aeval a : 𝕜[X] →ₐ[𝕜] A)).isUnit_mul_iff, aeval_C] at hk

Premises used: Polynomial.aeval_mul, spectrum.mem_iff, Polynomial.aeval_C, Commute.isUnit_mul_iff, Commute.map, Polynomial.aeval, Commute.all
-- 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
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)
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
⊢ (HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p).leadingCoeff ≠ 0

Tactic:
rw [mem_iff, ← p_a_eq, hprod, aeval_mul,
    ((Commute.all _ _).map (aeval a : 𝕜[X] →ₐ[𝕜] A)).isUnit_mul_iff, aeval_C] at hk

Premises used: Polynomial.aeval_mul, spectrum.mem_iff, Polynomial.aeval_C, Commute.isUnit_mul_iff, Commute.map, Polynomial.aeval, Commute.all
-- 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
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)
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
⊢ 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)

Tactic:
rw [mem_iff, ← p_a_eq, hprod, aeval_mul,
    ((Commute.all _ _).map (aeval a : 𝕜[X] →ₐ[𝕜] A)).isUnit_mul_iff, aeval_C] at hk

Premises used: Polynomial.aeval_mul, spectrum.mem_iff, Polynomial.aeval_C, Commute.isUnit_mul_iff, Commute.map, Polynomial.aeval, Commute.all
-- 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
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)
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)
⊢ (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:
rw [mem_iff, ← p_a_eq, hprod, aeval_mul,
    ((Commute.all _ _).map (aeval a : 𝕜[X] →ₐ[𝕜] A)).isUnit_mul_iff, aeval_C] at hk

Premises used: Polynomial.aeval_mul, spectrum.mem_iff, Polynomial.aeval_C, Commute.isUnit_mul_iff, Commute.map, Polynomial.aeval, Commute.all
-- 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
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)
⊢ ∃ 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)
-- 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
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
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
⊢ Membership.mem (γ := Set 𝕜) ((fun (x : 𝕜) ↦ eval x p) '' σ a) k

Tactic:
rcases hk with ⟨r, r_mem, r_ev⟩
-- 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
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)
r : 𝕜
r_mem : r ∈ σ a
r_ev : eval r (HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p) = 0
⊢ k = (fun (x : 𝕜) ↦ eval x p) r

Tactic:
simpa [eval_sub, eval_C, sub_eq_zero] using r_ev

Premises used: Polynomial.eval_C, sub_eq_zero, Polynomial.eval_sub
-- 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
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)
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:
exact ⟨r, r_mem, symm (by simpa [eval_sub, eval_C, sub_eq_zero] using r_ev)⟩
-- 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
p : 𝕜[X]
hnon : (σ a).Nonempty
⊢ Nontrivial A

Tactic:
nontriviality A
-- 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
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

Tactic:
Or.elim (le_or_gt (degree p) 0) (fun h => ?_) (map_polynomial_aeval_of_degree_pos a p)

Premises used: Polynomial.degree, le_or_gt, spectrum.map_polynomial_aeval_of_degree_pos, Or.elim, OfNat.ofNat
-- 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
p : 𝕜[X]
hnon : (σ a).Nonempty
h : Nontrivial A
⊢ p.degree ≤ 0

Tactic:
refine Or.elim (le_or_gt (degree p) 0) (fun h => ?_) (map_polynomial_aeval_of_degree_pos a p)

Premises used: Polynomial.degree, le_or_gt, spectrum.map_polynomial_aeval_of_degree_pos, Or.elim, OfNat.ofNat
-- 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
p : 𝕜[X]
hnon : (σ a).Nonempty
h_1 : Nontrivial A
h : p.degree ≤ 0
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
⊢ spectrum.{u, v} 𝕜 (A := A) ((aeval a : (a : 𝕜[X]) → A) p : A) = (fun (k : 𝕜) ↦ eval k p) '' σ a

Tactic:
rw [eq_C_of_degree_le_zero h]

Premises used: Polynomial.eq_C_of_degree_le_zero
-- 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
p : 𝕜[X]
hnon : (σ a).Nonempty
h_1 : Nontrivial A
h : p.degree ≤ 0
⊢ 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:
simp only [eval_C, aeval_C, scalar_eq, Set.Nonempty.image_const hnon]

Premises used: Polynomial.eval_C, Set.Nonempty.image_const, Polynomial.aeval_C, spectrum.scalar_eq
-- Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
n : ℕ
⊢ (fun (x : 𝕜) ↦ x ^ n) '' σ a ⊆ σ (a ^ n)

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

Premises used: Polynomial.aeval_X_pow, Polynomial.eval_X_pow, spectrum.subset_polynomial_aeval, HPow.hPow, Polynomial.X