awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : IsAlgClosed K
inst_3 : IsAlgClosed L
p : ℕ
inst_4 : CharP K p
inst_5 : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
inl : ∀ (hp : Nat.Prime p), Nonempty (K ≃+* L)
inr : ∀ (hp : p = 0), Nonempty (K ≃+* L)
⊢ Nonempty (K ≃+* L)

Tactic:
rcases CharP.char_is_prime_or_zero K p with (hp | hp)

Premises used: CharP.char_is_prime_or_zero
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : IsAlgClosed K
inst_3 : IsAlgClosed L
p : ℕ
inst_4 : CharP K p
inst_5 : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
hp : Nat.Prime p
⊢ Fact (Nat.Prime p)

Tactic:
haveI : Fact p.Prime := ⟨hp⟩
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : IsAlgClosed K
inst_3 : IsAlgClosed L
p : ℕ
inst_4 : CharP K p
inst_5 : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
hp : Nat.Prime p
this : Fact (Nat.Prime p)
⊢ Nonempty (K ≃+* L)

Tactic:
ringEquiv_of_Cardinal_eq_of_charP p hK hKL

Premises used: _private.0.IsAlgClosed.ringEquiv_of_Cardinal_eq_of_charP
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : IsAlgClosed K
inst_3 : IsAlgClosed L
p : ℕ
inst_4 : CharP K p
inst_5 : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
hp : Nat.Prime p
this : Fact (Nat.Prime p)
⊢ Nonempty (K ≃+* L)

Tactic:
exact ringEquiv_of_Cardinal_eq_of_charP p hK hKL

Premises used: _private.0.IsAlgClosed.ringEquiv_of_Cardinal_eq_of_charP
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : IsAlgClosed K
inst_3 : IsAlgClosed L
p : ℕ
inst_4 : CharP K p
inst_5 : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
hp : p = 0
⊢ CharP K 0

Tactic:
simp only [hp] at *
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
K : Type u
L : Type v
inst_1 : Field K
inst_2 : Field L
inst_3 : IsAlgClosed K
inst_4 : IsAlgClosed L
p : ℕ
inst_5 : CharP K p
inst_6 : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
hp : p = 0
inst : CharP K 0
⊢ CharP L 0

Tactic:
simp only [hp] at *
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
K : Type u
L : Type v
inst_1 : Field K
inst_2 : Field L
inst_3 : IsAlgClosed K
inst_4 : IsAlgClosed L
p : ℕ
inst_5 : CharP K p
inst_6 : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
hp : p = 0
inst : CharP K 0
inst₁ : CharP L 0
⊢ True

Tactic:
simp only [hp] at *
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : IsAlgClosed K
inst_3 : IsAlgClosed L
p : ℕ
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
inst_4 : CharP K 0
inst_5 : CharP L 0
hp : True
this_1 : CharZero K := ⋯
this : CharZero L := ⋯
⊢ Nonempty (K ≃+* L)

Tactic:
ringEquiv_of_equiv_of_charZero hK hKL

Premises used: IsAlgClosed.ringEquiv_of_equiv_of_charZero
-- Module: Mathlib.FieldTheory.IsAlgClosed.Classification
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : IsAlgClosed K
inst_3 : IsAlgClosed L
p : ℕ
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
inst_4 : CharP K 0
inst_5 : CharP L 0
hp : True
this_1 : CharZero K := ⋯
this : CharZero L := ⋯
⊢ Nonempty (K ≃+* L)

Tactic:
exact ringEquiv_of_equiv_of_charZero hK hKL

Premises used: IsAlgClosed.ringEquiv_of_equiv_of_charZero
-- Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : IsDomain R
p : R[X]
a : A
h :
  ¬IsUnit.{v} (M := A)
      ((aeval a : (a : R[X]) → A)
          (Multiset.prod
            (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
              p.roots)) :
        A)
⊢ ¬IsUnit.{v} (M := A)
      (List.prod
        (List.map (α := R[X]) (⇑(aeval a) : (a : R[X]) → A)
          (Multiset.toList
            (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
              p.roots))))

Tactic:
rw [← Multiset.prod_toList, map_list_prod] at h

Premises used: Multiset.prod_toList, map_list_prod
-- Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : IsDomain R
p : R[X]
a : A
h :
  ¬IsUnit.{v} (M := A)
      (List.prod
        (List.map (α := R[X]) (⇑(aeval a) : (a : R[X]) → A)
          (Multiset.toList
            (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
              p.roots))))
⊢ ¬∀ (m : A),
      Membership.mem (γ := List A)
          (List.map (α := R[X]) (⇑(aeval a) : (a : R[X]) → A)
            (Multiset.toList
              (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
                p.roots)))
          m →
        IsUnit m

Tactic:
replace h := mt List.prod_isUnit h
-- Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : IsDomain R
p : R[X]
a : A
h :
  ¬∀ (m : A),
      Membership.mem (γ := List A)
          (List.map (α := R[X]) (⇑(aeval a) : (a : R[X]) → A)
            (Multiset.toList
              (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
                p.roots)))
          m →
        IsUnit m
⊢ ∃ a_1 ∈ p.roots, ¬IsUnit (HSub.hSub (β := A) a ((↑ₐ : (a : R) → A) a_1 : A))

Tactic:
simp only [not_forall, exists_prop, aeval_C, Multiset.mem_toList, List.mem_map, aeval_X,
    exists_exists_and_eq_and, Multiset.mem_map, map_sub] at h

Premises used: map_sub, Multiset.mem_map, exists_prop, exists_exists_and_eq_and, Polynomial.aeval_C, Multiset.mem_toList, List.mem_map, Classical.not_forall, Polynomial.aeval_X
-- Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : IsDomain R
p : R[X]
a : A
h : ∃ a_1 ∈ p.roots, ¬IsUnit (HSub.hSub (β := A) a ((↑ₐ : (a : R) → A) a_1 : A))
rcases :
  ∀ (r : R) (r_mem : r ∈ p.roots) (r_nu : ¬IsUnit (HSub.hSub (β := A) a ((↑ₐ : (a : R) → A) r : A))),
    ∃ k ∈ σ a, eval k p = 0
⊢ ∃ k ∈ σ a, eval k p = 0

Tactic:
rcases h with ⟨r, r_mem, r_nu⟩
-- Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : IsDomain R
p : R[X]
a : A
r : R
r_mem : r ∈ p.roots
r_nu : ¬IsUnit (HSub.hSub (β := A) a ((↑ₐ : (a : R) → A) r : A))
rwa : ¬IsUnit (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) r : A) a)
rwa₁ rwa₂ rwa₃ rwa₄ : ¬IsUnit (HSub.hSub (β := A) a ((↑ₐ : (a : R) → A) r : A))
⊢ r ∈ σ a

Tactic:
rwa [mem_iff, ← IsUnit.sub_iff]

Premises used: IsUnit.sub_iff, spectrum.mem_iff
-- Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : IsDomain R
p : R[X]
a : A
r : R
r_mem : r ∈ p.roots
r_nu : ¬IsUnit (HSub.hSub (β := A) a ((↑ₐ : (a : R) → A) r : A))
⊢ ∃ k ∈ σ a, eval k p = 0

Tactic:
exact ⟨r, by rwa [mem_iff, ← IsUnit.sub_iff], (mem_roots'.1 r_mem).2⟩
-- Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : 𝕜[X] := HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) (eval k p) : 𝕜[X]) p
⊢ q.IsRoot k

Tactic:
simp only [q, eval_C, eval_sub, sub_self, IsRoot.def]

Premises used: Polynomial.eval_C, sub_self, Polynomial.IsRoot.def, Polynomial.eval_sub
-- Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : 𝕜[X] := HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) (eval k p) : 𝕜[X]) p
⊢ q.IsRoot k

Tactic:
have hroot : IsRoot q k := by simp only [q, eval_C, eval_sub, sub_self, IsRoot.def]
-- Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : 𝕜[X] := HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) (eval k p) : 𝕜[X]) p
hroot : q.IsRoot k
⊢ HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) X *
      -(q / HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X])) =
    q

Tactic:
rw [← mul_div_eq_iff_isRoot, ← neg_mul_neg, neg_sub] at hroot

Premises used: Polynomial.mul_div_eq_iff_isRoot, neg_sub, neg_mul_neg
-- Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : 𝕜[X] := HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) (eval k p) : 𝕜[X]) p
hroot :
  HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) X *
      -(q / HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X])) =
    q
⊢ HSub.hSub (α := A) (β := A) ((↑ₐ : (a : 𝕜) → A) (eval k p) : A) ((aeval a : (a : 𝕜[X]) → A) p : A) =
    (aeval a : (a : 𝕜[X]) → A) q

Tactic:
simp only [q, aeval_C, map_sub]

Premises used: map_sub, Polynomial.aeval_C
-- Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : 𝕜[X] := HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) (eval k p) : 𝕜[X]) p
hroot :
  HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) X *
      -(q / HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X])) =
    q
⊢ HSub.hSub (α := A) (β := A) ((↑ₐ : (a : 𝕜) → A) (eval k p) : A) ((aeval a : (a : 𝕜[X]) → A) p : A) =
    (aeval a : (a : 𝕜[X]) → A) q

Tactic:
have aeval_q_eq : ↑ₐ (eval k p) - aeval a p = aeval a q := by
    simp only [q, aeval_C, map_sub]
-- Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : 𝕜[X] := HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) (eval k p) : 𝕜[X]) p
hroot :
  HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) X *
      -(q / HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X])) =
    q
aeval_q_eq :
  HSub.hSub (α := A) (β := A) ((↑ₐ : (a : 𝕜) → A) (eval k p) : A) ((aeval a : (a : 𝕜[X]) → A) p : A) =
    (aeval a : (a : 𝕜[X]) → A) q
rw :
  ¬IsUnit
      (HMul.hMul (α := A) (β := A)
        ((aeval a : (a : 𝕜[X]) → A) (HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) X) : A)
        ((aeval a : (a : 𝕜[X]) → A) (-(q / HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]))) : A))
⊢ (fun (x : 𝕜) ↦ eval x p) k ∈ spectrum.{u, v} 𝕜 (A := A) ((aeval a : (a : 𝕜[X]) → A) p : A)

Tactic:
rw [mem_iff, aeval_q_eq, ← hroot, aeval_mul]

Premises used: Polynomial.aeval_mul, spectrum.mem_iff
-- Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : 𝕜[X] := HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) (eval k p) : 𝕜[X]) p
hroot :
  HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) X *
      -(q / HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X])) =
    q
aeval_q_eq :
  HSub.hSub (α := A) (β := A) ((↑ₐ : (a : 𝕜) → A) (eval k p) : A) ((aeval a : (a : 𝕜[X]) → A) p : A) =
    (aeval a : (a : 𝕜[X]) → A) q
⊢ Commute.{v} (S := A)
    ((aeval a : (a : 𝕜[X]) → A) (HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) X) : A)
    ((aeval a : (a : 𝕜[X]) → A) (-(q / HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]))) : A)

Tactic:
have hcomm := (Commute.all (C k - X) (-(q / (X - C k)))).map (aeval a : 𝕜[X] →ₐ[𝕜] A)
-- Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : 𝕜[X] := HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) (eval k p) : 𝕜[X]) p
hroot :
  HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) X *
      -(q / HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X])) =
    q
aeval_q_eq :
  HSub.hSub (α := A) (β := A) ((↑ₐ : (a : 𝕜) → A) (eval k p) : A) ((aeval a : (a : 𝕜[X]) → A) p : A) =
    (aeval a : (a : 𝕜[X]) → A) q
hcomm :
  Commute.{v} (S := A)
    ((aeval a : (a : 𝕜[X]) → A) (HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) X) : A)
    ((aeval a : (a : 𝕜[X]) → A) (-(q / HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]))) : A)
apply :
  ¬IsUnit.{v} (M := A)
      ((aeval a : (a : 𝕜[X]) → A) (HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) X) : A)
⊢ ¬IsUnit
      (HMul.hMul (α := A) (β := A)
        ((aeval a : (a : 𝕜[X]) → A) (HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) X) : A)
        ((aeval a : (a : 𝕜[X]) → A) (-(q / HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]))) : A))

Tactic:
apply mt fun h => (hcomm.isUnit_mul_iff.mp h).1

Premises used: mt, And.left, Commute.isUnit_mul_iff, Iff.mp
-- Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : 𝕜[X] := HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) (eval k p) : 𝕜[X]) p
hroot :
  HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) X *
      -(q / HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X])) =
    q
aeval_q_eq :
  HSub.hSub (α := A) (β := A) ((↑ₐ : (a : 𝕜) → A) (eval k p) : A) ((aeval a : (a : 𝕜[X]) → A) p : A) =
    (aeval a : (a : 𝕜[X]) → A) q
hcomm :
  Commute.{v} (S := A)
    ((aeval a : (a : 𝕜[X]) → A) (HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) X) : A)
    ((aeval a : (a : 𝕜[X]) → A) (-(q / HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]))) : A)
⊢ ¬IsUnit.{v} (M := A)
      ((aeval a : (a : 𝕜[X]) → A) (HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) X) : A)

Tactic:
simpa only [aeval_X, aeval_C, map_sub] using hk

Premises used: map_sub, Polynomial.aeval_C, Polynomial.aeval_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
p : 𝕜[X]
hdeg : 0 < p.degree
⊢ spectrum.{u, v} 𝕜 (A := A) ((aeval a : (a : 𝕜[X]) → A) p : A) = (fun (x : 𝕜) ↦ eval x p) '' σ a

Tactic:
Set.eq_of_subset_of_subset (fun k hk => ?_) (subset_polynomial_aeval a p)

Premises used: spectrum.subset_polynomial_aeval, Set.eq_of_subset_of_subset
-- 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
refine :
  ∀ (k : 𝕜) (hk : k ∈ spectrum.{u, v} 𝕜 (A := A) ((aeval a : (a : 𝕜[X]) → A) p : A)),
    Membership.mem (γ := Set 𝕜) ((fun (x : 𝕜) ↦ eval x p) '' σ a) k
⊢ spectrum.{u, v} 𝕜 (A := A) ((aeval a : (a : 𝕜[X]) → A) p : A) = (fun (x : 𝕜) ↦ eval x p) '' σ a

Tactic:
refine Set.eq_of_subset_of_subset (fun k hk => ?_) (subset_polynomial_aeval a p)

Premises used: spectrum.subset_polynomial_aeval, Set.eq_of_subset_of_subset
-- 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)
⊢ 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:
have hprod := (IsAlgClosed.splits (C k - p)).eq_prod_roots
-- 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])
rwa rwa₁ rwa₂ rwa₃ : 0 < p.degree
⊢ 0 < (HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p).degree

Tactic:
rwa [degree_sub_eq_right_of_degree_lt (lt_of_le_of_lt degree_C_le hdeg)]

Premises used: lt_of_le_of_lt, Polynomial.degree_sub_eq_right_of_degree_lt, Polynomial.degree_C_le
-- 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])
⊢ HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p ≠ 0

Tactic:
have h_ne : C k - p ≠ 0 := ne_zero_of_degree_gt <| by
    rwa [degree_sub_eq_right_of_degree_lt (lt_of_le_of_lt degree_C_le hdeg)]
-- 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
⊢ (HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p).leadingCoeff ≠ 0

Tactic:
have lead_ne := leadingCoeff_ne_zero.mpr h_ne
-- 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
⊢ 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:
have lead_unit := (Units.map ↑ₐ.toMonoidHom (Units.mk0 _ lead_ne)).isUnit
-- 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)
⊢ (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:
simp only [aeval_C, map_sub]

Premises used: map_sub, Polynomial.aeval_C
-- 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)
⊢ (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]