-- Mathlib/ModelTheory/Algebra/Field/IsAlgClosed.lean
theorem isAlgClosed_of_model_ACF (p : ℕ) (K : Type*)
    [Field K] [CompatibleRing K] [h : (Theory.ACF p).Model K] :
    IsAlgClosed K

Proof state:
p : ℕ
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
h : K ⊨ Theory.ACF p
⊢ IsAlgClosed K

Tactic:
refine IsAlgClosed.of_exists_root _ ?_

Result:
p : ℕ
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
h : K ⊨ Theory.ACF p
⊢ ∀ (p : K[X]), p.Monic → Irreducible p → ∃ x, eval x p = 0

Proof state:
p✝ : ℕ
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
h✝ : K ⊨ Theory.ACF p✝
p : K[X]
hpm : p.Monic
hpi : Irreducible p
h : ∀ (φ : Language.ring.Sentence), ∀ x ∈ {n | 0 < n}, genericMonicPolyHasRoot x = φ → K ⊨ φ
⊢ ∃ x, eval x p = 0

Tactic:
have := h _ p.natDegree (natDegree_pos_iff_degree_pos.2
  (degree_pos_of_irreducible hpi)) rfl

Result:
p✝ : ℕ
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
h✝ : K ⊨ Theory.ACF p✝
p : K[X]
hpm : p.Monic
hpi : Irreducible p
h : ∀ (φ : Language.ring.Sentence), ∀ x ∈ {n | 0 < n}, genericMonicPolyHasRoot x = φ → K ⊨ φ
this : K ⊨ genericMonicPolyHasRoot p.natDegree
⊢ ∃ x, eval x p = 0

Proof state:
p✝ : ℕ
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
h✝ : K ⊨ Theory.ACF p✝
p : K[X]
hpm : p.Monic
hpi : Irreducible p
h : K ⊨ genericMonicPolyHasRoot '' {n | 0 < n}
⊢ ∃ x, eval x p = 0

Tactic:
simp only [Theory.model_iff, Set.mem_image, Set.mem_singleton_iff,
  exists_prop, forall_exists_index, and_imp] at h

Result:
p✝ : ℕ
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
h✝ : K ⊨ Theory.ACF p✝
p : K[X]
hpm : p.Monic
hpi : Irreducible p
h : ∀ (φ : Language.ring.Sentence), ∀ x ∈ {n | 0 < n}, genericMonicPolyHasRoot x = φ → K ⊨ φ
⊢ ∃ x, eval x p = 0

Proof state:
p✝ : ℕ
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
h : K ⊨ Theory.ACF p✝
p : K[X]
hpm : p.Monic
hpi : Irreducible p
⊢ genericMonicPolyHasRoot '' {n | 0 < n} ⊆ Theory.ACF p✝

Tactic:
simp [Theory.ACF]

Result:
no goals

Proof state:
p✝ : ℕ
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
h✝ : K ⊨ Theory.ACF p✝
p : K[X]
hpm : p.Monic
hpi : Irreducible p
h : ∀ (φ : Language.ring.Sentence), ∀ x ∈ {n | 0 < n}, genericMonicPolyHasRoot x = φ → K ⊨ φ
this : ∀ (p_1 : { p_1 // p_1.Monic ∧ p_1.natDegree = p.natDegree }), ∃ x, eval x ↑p_1 = 0
⊢ ∃ x, eval x p = 0

Tactic:
exact this ⟨_, hpm, rfl⟩

Result:
no goals

Proof state:
p✝ : ℕ
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
h : K ⊨ Theory.ACF p✝
p : K[X]
hpm : p.Monic
hpi : Irreducible p
⊢ ∃ x, eval x p = 0

Tactic:
have h : K ⊨ genericMonicPolyHasRoot '' {n | 0 < n} :=
  Theory.Model.mono h (by simp [Theory.ACF])

Result:
p✝ : ℕ
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
h✝ : K ⊨ Theory.ACF p✝
p : K[X]
hpm : p.Monic
hpi : Irreducible p
h : K ⊨ genericMonicPolyHasRoot '' {n | 0 < n}
⊢ ∃ x, eval x p = 0

Proof state:
p✝ : ℕ
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
h✝ : K ⊨ Theory.ACF p✝
p : K[X]
hpm : p.Monic
hpi : Irreducible p
h : ∀ (φ : Language.ring.Sentence), ∀ x ∈ {n | 0 < n}, genericMonicPolyHasRoot x = φ → K ⊨ φ
this : K ⊨ genericMonicPolyHasRoot p.natDegree
⊢ ∃ x, eval x p = 0

Tactic:
rw [realize_genericMonicPolyHasRoot] at this

Result:
p✝ : ℕ
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
h✝ : K ⊨ Theory.ACF p✝
p : K[X]
hpm : p.Monic
hpi : Irreducible p
h : ∀ (φ : Language.ring.Sentence), ∀ x ∈ {n | 0 < n}, genericMonicPolyHasRoot x = φ → K ⊨ φ
this : ∀ (p_1 : { p_1 // p_1.Monic ∧ p_1.natDegree = p.natDegree }), ∃ x, eval x ↑p_1 = 0
⊢ ∃ x, eval x p = 0

Proof state:
p : ℕ
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
h : K ⊨ Theory.ACF p
⊢ ∀ (p : K[X]), p.Monic → Irreducible p → ∃ x, eval x p = 0

Tactic:
intro p hpm hpi

Result:
p✝ : ℕ
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
h : K ⊨ Theory.ACF p✝
p : K[X]
hpm : p.Monic
hpi : Irreducible p
⊢ ∃ x, eval x p = 0