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

Proof state:
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), p.Monic → Irreducible p → p.Separable → ∃ x, eval x p = 0
p : k[X]
hsep : p.Separable
q : k[X]
hq : Irreducible q
hdvd : q ∣ p
hlc : IsUnit q.leadingCoeff⁻¹
hsep' : (q * C q.leadingCoeff⁻¹).Separable
⊢ q.degree = 1

Tactic:
have hirr' := hq

Result:
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), p.Monic → Irreducible p → p.Separable → ∃ x, eval x p = 0
p : k[X]
hsep : p.Separable
q : k[X]
hq : Irreducible q
hdvd : q ∣ p
hlc : IsUnit q.leadingCoeff⁻¹
hsep' : (q * C q.leadingCoeff⁻¹).Separable
hirr' : Irreducible q
⊢ q.degree = 1

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

Tactic:
simp only [map_id] at hdvd

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

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

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

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

Proof state:
case intro
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), p.Monic → Irreducible p → p.Separable → ∃ x, eval x p = 0
p : k[X]
hsep : p.Separable
q : k[X]
hq : Irreducible q
hdvd : q ∣ p
hlc : IsUnit q.leadingCoeff⁻¹
hsep' : (q * C q.leadingCoeff⁻¹).Separable
hirr' : 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 hirr' hx

Result:
no goals

Proof state:
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), p.Monic → Irreducible p → p.Separable → ∃ x, eval x p = 0
p : k[X]
hsep : p.Separable
q : k[X]
hq : Irreducible q
hdvd : q ∣ p
hlc : IsUnit q.leadingCoeff⁻¹
⊢ q.degree = 1

Tactic:
have hsep' : Separable (q * C (leadingCoeff q)⁻¹) :=
  Separable.mul (Separable.of_dvd hsep hdvd) ((separable_C _).2 hlc)
  (by simpa only [← isCoprime_mul_unit_right_right (isUnit_C.2 hlc) q 1, one_mul]
    using isCoprime_one_right (x := q))

Result:
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), p.Monic → Irreducible p → p.Separable → ∃ x, eval x p = 0
p : k[X]
hsep : p.Separable
q : k[X]
hq : Irreducible q
hdvd : q ∣ p
hlc : IsUnit q.leadingCoeff⁻¹
hsep' : (q * C q.leadingCoeff⁻¹).Separable
⊢ q.degree = 1

Proof state:
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), p.Monic → Irreducible p → p.Separable → ∃ x, eval x p = 0
p : k[X]
hsep : p.Separable
q : k[X]
hq : Irreducible q
hdvd : q ∣ p
hlc : IsUnit q.leadingCoeff⁻¹
hsep' : (q * C q.leadingCoeff⁻¹).Separable
hirr' : Irreducible (q * C q.leadingCoeff⁻¹)
⊢ q.degree = 1

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

Result:
case intro
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), p.Monic → Irreducible p → p.Separable → ∃ x, eval x p = 0
p : k[X]
hsep : p.Separable
q : k[X]
hq : Irreducible q
hdvd : q ∣ p
hlc : IsUnit q.leadingCoeff⁻¹
hsep' : (q * C q.leadingCoeff⁻¹).Separable
hirr' : 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 → p.Separable → ∃ x, eval x p = 0
p : k[X]
hsep : p.Separable
⊢ ∀ {g : k[X]}, Irreducible g → g ∣ map (RingHom.id k) p → g.degree = 1

Tactic:
intro q hq hdvd

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

Proof state:
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), p.Monic → Irreducible p → p.Separable → ∃ x, eval x p = 0
p : k[X]
hsep : p.Separable
q : k[X]
hq : Irreducible q
hdvd : q ∣ p
hlc : IsUnit q.leadingCoeff⁻¹
hsep' : (q * C q.leadingCoeff⁻¹).Separable
hirr' : Irreducible q
⊢ q.degree = 1

Tactic:
rw [← irreducible_mul_isUnit (isUnit_C.2 hlc)] at hirr'

Result:
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), p.Monic → Irreducible p → p.Separable → ∃ x, eval x p = 0
p : k[X]
hsep : p.Separable
q : k[X]
hq : Irreducible q
hdvd : q ∣ p
hlc : IsUnit q.leadingCoeff⁻¹
hsep' : (q * C q.leadingCoeff⁻¹).Separable
hirr' : Irreducible (q * C q.leadingCoeff⁻¹)
⊢ q.degree = 1

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

Tactic:
have hlc : IsUnit (leadingCoeff q)⁻¹ := IsUnit.inv <| Ne.isUnit <|
  leadingCoeff_ne_zero.2 <| Irreducible.ne_zero hq

Result:
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), p.Monic → Irreducible p → p.Separable → ∃ x, eval x p = 0
p : k[X]
hsep : p.Separable
q : k[X]
hq : Irreducible q
hdvd : q ∣ p
hlc : IsUnit q.leadingCoeff⁻¹
⊢ q.degree = 1

Proof state:
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), p.Monic → Irreducible p → p.Separable → ∃ x, eval x p = 0
p : k[X]
hsep : p.Separable
q : k[X]
hq : Irreducible q
hdvd : q ∣ p
hlc : IsUnit q.leadingCoeff⁻¹
⊢ IsCoprime q (C q.leadingCoeff⁻¹)

Tactic:
simpa only [← isCoprime_mul_unit_right_right (isUnit_C.2 hlc) q 1, one_mul]
using isCoprime_one_right (x := q)

Result:
no goals