-- Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean
theorem nonempty_of_isAlgClosed_of_finiteDimensional [IsAlgClosed 𝕜] [Nontrivial A]
    [I : FiniteDimensional 𝕜 A] (a : A) : (σ a).Nonempty

Proof state:
case intro.intro.intro.intro
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : p.Monic
h_eval_p : eval₂ ↑ₐ a p = 0
nu : ¬IsUnit ((aeval a) (Multiset.map (fun a => X - C a) p.roots).prod)
k : 𝕜
hk : k ∈ σ a
right✝ : eval k p = 0
⊢ (σ a).Nonempty

Tactic:
exact ⟨k, hk⟩

Result:
no goals

Proof state:
case intro.intro
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : p.Monic
h_eval_p : eval₂ ↑ₐ a p = 0
⊢ (σ a).Nonempty

Tactic:
have nu : ¬IsUnit (aeval a p) := by rw [← aeval_def] at h_eval_p; rw [h_eval_p]; simp

Result:
case intro.intro
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : p.Monic
h_eval_p : eval₂ ↑ₐ a p = 0
nu : ¬IsUnit ((aeval a) p)
⊢ (σ a).Nonempty

Proof state:
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : p.Monic
h_eval_p : (aeval a) p = 0
⊢ ¬IsUnit ((aeval a) p)

Tactic:
rw [h_eval_p]

Result:
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : p.Monic
h_eval_p : (aeval a) p = 0
⊢ ¬IsUnit 0

Proof state:
case intro.intro
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : p.Monic
h_eval_p : eval₂ ↑ₐ a p = 0
nu : ¬IsUnit ((aeval a) p)
⊢ (σ a).Nonempty

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

Result:
case intro.intro
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : p.Monic
h_eval_p : eval₂ ↑ₐ a p = 0
nu : ¬IsUnit ((aeval a) (Multiset.map (fun a => X - C a) p.roots).prod)
⊢ (σ a).Nonempty

Proof state:
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : p.Monic
h_eval_p : eval₂ ↑ₐ a p = 0
⊢ ¬IsUnit ((aeval a) p)

Tactic:
rw [← aeval_def] at h_eval_p

Result:
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : p.Monic
h_eval_p : (aeval a) p = 0
⊢ ¬IsUnit ((aeval a) p)

Proof state:
case intro.intro
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : p.Monic
h_eval_p : eval₂ ↑ₐ a p = 0
nu : ¬IsUnit ((aeval a) (Multiset.map (fun a => X - C a) p.roots).prod)
⊢ (σ a).Nonempty

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

Result:
case intro.intro.intro.intro
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : p.Monic
h_eval_p : eval₂ ↑ₐ a p = 0
nu : ¬IsUnit ((aeval a) (Multiset.map (fun a => X - C a) p.roots).prod)
k : 𝕜
hk : k ∈ σ a
right✝ : eval k p = 0
⊢ (σ a).Nonempty

Proof state:
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
⊢ (σ a).Nonempty

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

Result:
case intro.intro
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : p.Monic
h_eval_p : eval₂ ↑ₐ a p = 0
⊢ (σ a).Nonempty

Proof state:
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : p.Monic
h_eval_p : (aeval a) p = 0
⊢ ¬IsUnit 0

Tactic:
simp

Result:
no goals