-- Mathlib/FieldTheory/IsAlgClosed/Basic.lean
theorem of_exists_root (H : ∀ p : k[X], p.Monic → Irreducible p → ∃ x, p.eval x = 0) :
    IsAlgClosed k

Proof state:
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), p.Monic → Irreducible p → ∃ x, eval x p = 0
p q : k[X]
hq : Irreducible q
a✝ : q ∣ map (RingHom.id k) p
⊢ q.degree = 1

Tactic:
have : Irreducible (q * C (leadingCoeff q)⁻¹) := by
  classical
  rw [← coe_normUnit_of_ne_zero hq.ne_zero]
  exact (associated_normalize _).irreducible hq

Result:
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), p.Monic → Irreducible p → ∃ x, eval x p = 0
p q : k[X]
hq : Irreducible q
a✝ : q ∣ map (RingHom.id k) p
this : Irreducible (q * C q.leadingCoeff⁻¹)
⊢ q.degree = 1

Proof state:
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), p.Monic → Irreducible p → ∃ x, eval x p = 0
p q : k[X]
hq : Irreducible q
a✝ : q ∣ map (RingHom.id k) p
this : Irreducible (q * C q.leadingCoeff⁻¹)
⊢ q.degree = 1

Tactic:
obtain ⟨x, hx⟩ := H (q * C (leadingCoeff q)⁻¹) (monic_mul_leadingCoeff_inv hq.ne_zero) this

Result:
case intro
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), p.Monic → Irreducible p → ∃ x, eval x p = 0
p q : k[X]
hq : Irreducible q
a✝ : q ∣ map (RingHom.id k) p
this : Irreducible (q * C q.leadingCoeff⁻¹)
x : k
hx : eval x (q * C q.leadingCoeff⁻¹) = 0
⊢ q.degree = 1

Proof state:
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), p.Monic → Irreducible p → ∃ x, eval x p = 0
p q : k[X]
hq : Irreducible q
a✝ : q ∣ map (RingHom.id k) p
⊢ Irreducible (q * C q.leadingCoeff⁻¹)

Tactic:
classical
rw [← coe_normUnit_of_ne_zero hq.ne_zero]
exact (associated_normalize _).irreducible hq

Result:
no goals

Proof state:
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), p.Monic → Irreducible p → ∃ x, eval x p = 0
p q : k[X]
hq : Irreducible q
a✝ : q ∣ map (RingHom.id k) p
⊢ Irreducible (q * ↑(normUnit q))

Tactic:
exact (associated_normalize _).irreducible hq

Result:
no goals

Proof state:
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), p.Monic → Irreducible p → ∃ x, eval x p = 0
p q : k[X]
hq : Irreducible q
a✝ : q ∣ map (RingHom.id k) p
⊢ Irreducible (q * C q.leadingCoeff⁻¹)

Tactic:
rw [← coe_normUnit_of_ne_zero hq.ne_zero]

Result:
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), p.Monic → Irreducible p → ∃ x, eval x p = 0
p q : k[X]
hq : Irreducible q
a✝ : q ∣ map (RingHom.id k) p
⊢ Irreducible (q * ↑(normUnit q))

Proof state:
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), p.Monic → Irreducible p → ∃ x, eval x p = 0
p : k[X]
⊢ ∀ {g : k[X]}, Irreducible g → g ∣ map (RingHom.id k) p → g.degree = 1

Tactic:
intro q hq _

Result:
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), p.Monic → Irreducible p → ∃ x, eval x p = 0
p q : k[X]
hq : Irreducible q
a✝ : q ∣ map (RingHom.id k) p
⊢ q.degree = 1

Proof state:
case intro
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), p.Monic → Irreducible p → ∃ x, eval x p = 0
p q : k[X]
hq : Irreducible q
a✝ : q ∣ map (RingHom.id k) p
this : Irreducible (q * C q.leadingCoeff⁻¹)
x : k
hx : eval x (q * C q.leadingCoeff⁻¹) = 0
⊢ q.degree = 1

Tactic:
exact degree_mul_leadingCoeff_inv q hq.ne_zero ▸ degree_eq_one_of_irreducible_of_root this hx

Result:
no goals

Proof state:
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), p.Monic → Irreducible p → ∃ x, eval x p = 0
⊢ IsAlgClosed k

Tactic:
refine ⟨fun p ↦ Or.inr ?_⟩

Result:
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), p.Monic → Irreducible p → ∃ x, eval x p = 0
p : k[X]
⊢ ∀ {g : k[X]}, Irreducible g → g ∣ map (RingHom.id k) p → g.degree = 1