awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
p_1 : ℕ
K : Type u_2
inst : Field K
inst_1 : CompatibleRing K
h_1 : K ⊨ Theory.ACF p_1
p : K[X]
hpm : p.Monic
hpi : Irreducible p
h : K ⊨ genericMonicPolyHasRoot '' {n : ℕ | 0 < n}
⊢ ∀ (φ : Language.ring.Sentence) (x : ℕ),
    Membership.mem (γ := Set ℕ) {n : ℕ | 0 < n} x → genericMonicPolyHasRoot x = φ → K ⊨ φ

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

Premises used: and_imp, FirstOrder.Language.Theory.model_iff, Set.mem_image, forall_exists_index
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
p_1 : ℕ
K : Type u_2
inst : Field K
inst_1 : CompatibleRing K
h_1 : K ⊨ Theory.ACF p_1
p : K[X]
hpm : p.Monic
hpi : Irreducible p
h :
  ∀ (φ : Language.ring.Sentence) (x : ℕ),
    Membership.mem (γ := Set ℕ) {n : ℕ | 0 < n} x → genericMonicPolyHasRoot x = φ → K ⊨ φ
⊢ K ⊨ genericMonicPolyHasRoot p.natDegree

Tactic:
have := h _ p.natDegree (natDegree_pos_iff_degree_pos.2
    (degree_pos_of_irreducible hpi)) rfl
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
p_1 : ℕ
K : Type u_2
inst : Field K
inst_1 : CompatibleRing K
h_1 : K ⊨ Theory.ACF p_1
p : K[X]
hpm : p.Monic
hpi : Irreducible p
h :
  ∀ (φ : Language.ring.Sentence) (x : ℕ),
    Membership.mem (γ := Set ℕ) {n : ℕ | 0 < n} x → genericMonicPolyHasRoot x = φ → K ⊨ φ
this : K ⊨ genericMonicPolyHasRoot p.natDegree
⊢ ∀ (p_2 : { p_2 : K[X] // p_2.Monic ∧ p_2.natDegree = p.natDegree }), ∃ (x : K), eval x (↑p_2 : K[X]) = 0

Tactic:
rw [realize_genericMonicPolyHasRoot] at this

Premises used: FirstOrder.Field.realize_genericMonicPolyHasRoot
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
p_1 : ℕ
K : Type u_2
inst : Field K
inst_1 : CompatibleRing K
h_1 : K ⊨ Theory.ACF p_1
p : K[X]
hpm : p.Monic
hpi : Irreducible p
h :
  ∀ (φ : Language.ring.Sentence) (x : ℕ),
    Membership.mem (γ := Set ℕ) {n : ℕ | 0 < n} x → genericMonicPolyHasRoot x = φ → K ⊨ φ
this : ∀ (p_2 : { p_2 : K[X] // p_2.Monic ∧ p_2.natDegree = p.natDegree }), ∃ (x : K), eval x (↑p_2 : K[X]) = 0
⊢ ∃ (x : K), eval x p = 0

Tactic:
this ⟨_, hpm, rfl⟩

Premises used: Subtype.mk, And.intro, rfl
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
p_1 : ℕ
K : Type u_2
inst : Field K
inst_1 : CompatibleRing K
h_1 : K ⊨ Theory.ACF p_1
p : K[X]
hpm : p.Monic
hpi : Irreducible p
h :
  ∀ (φ : Language.ring.Sentence) (x : ℕ),
    Membership.mem (γ := Set ℕ) {n : ℕ | 0 < n} x → genericMonicPolyHasRoot x = φ → K ⊨ φ
this : ∀ (p_2 : { p_2 : K[X] // p_2.Monic ∧ p_2.natDegree = p.natDegree }), ∃ (x : K), eval x (↑p_2 : K[X]) = 0
⊢ ∃ (x : K), eval x p = 0

Tactic:
exact this ⟨_, hpm, rfl⟩

Premises used: Subtype.mk, And.intro, rfl
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
p : ℕ
hp : Nat.Prime p
⊢ Fact (Nat.Prime p)

Tactic:
have : Fact p.Prime := ⟨hp⟩
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
x : CompatibleRing (AlgebraicClosure (ZMod p)) := compatibleRingOfRing (AlgebraicClosure (ZMod p))
⊢ (Theory.ACF p).IsSatisfiable

Tactic:
⟨⟨AlgebraicClosure (ZMod p)⟩⟩

Premises used: FirstOrder.Language.Theory.IsSatisfiable, Nonempty.intro, ZMod, FirstOrder.Language.Theory.ModelType.mk, AlgebraicClosure
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
x : CompatibleRing (AlgebraicClosure (ZMod p)) := compatibleRingOfRing (AlgebraicClosure (ZMod p))
⊢ (Theory.ACF p).IsSatisfiable

Tactic:
exact ⟨⟨AlgebraicClosure (ZMod p)⟩⟩
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
p : ℕ
hp : p = 0
inr : (Theory.ACF 0).IsSatisfiable
⊢ (Theory.ACF p).IsSatisfiable

Tactic:
subst hp
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
x : CompatibleRing (AlgebraicClosure ℚ) := compatibleRingOfRing (AlgebraicClosure ℚ)
⊢ (Theory.ACF 0).IsSatisfiable

Tactic:
⟨⟨AlgebraicClosure ℚ⟩⟩

Premises used: FirstOrder.Language.Theory.IsSatisfiable, Rat, Nonempty.intro, FirstOrder.Language.Theory.ModelType.mk, AlgebraicClosure
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
x : CompatibleRing (AlgebraicClosure ℚ) := compatibleRingOfRing (AlgebraicClosure ℚ)
⊢ (Theory.ACF 0).IsSatisfiable

Tactic:
exact ⟨⟨AlgebraicClosure ℚ⟩⟩
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
p : ℕ
hp : Nat.Prime p ∨ p = 0
inl : ∀ (hp : Nat.Prime p), (Theory.ACF p).IsSatisfiable
inr : ∀ (hp : p = 0), (Theory.ACF p).IsSatisfiable
⊢ (Theory.ACF p).IsSatisfiable

Tactic:
cases hp with
  | inl hp =>
    have : Fact p.Prime := ⟨hp⟩
    let _ := compatibleRingOfRing (AlgebraicClosure (ZMod p))
    exact ⟨⟨AlgebraicClosure (ZMod p)⟩⟩
  | inr hp =>
    subst hp
    let _ := compatibleRingOfRing (AlgebraicClosure ℚ)
    exact ⟨⟨AlgebraicClosure ℚ⟩⟩
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
p : ℕ
κ : Cardinal.{u_2}
hκ : ℵ₀ < κ
M : Type u_2
struc : Language.ring.Structure M
is_model : M ⊨ Theory.ACF p
nonempty' : Nonempty M
N : Type u_2
struc_1 : Language.ring.Structure N
is_model_1 : N ⊨ Theory.ACF p
nonempty'_1 : Nonempty N
hM : #(↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) = κ
hN : #(↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2) = κ
x : Field M := fieldOfModelACF p M
⊢ M ⊨ Theory.field

Tactic:
have := modelField_of_modelACF p M
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
p : ℕ
κ : Cardinal.{u_2}
hκ : ℵ₀ < κ
M : Type u_2
struc : Language.ring.Structure M
is_model : M ⊨ Theory.ACF p
nonempty' : Nonempty M
N : Type u_2
struc_1 : Language.ring.Structure N
is_model_1 : N ⊨ Theory.ACF p
nonempty'_1 : Nonempty N
hM : #(↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) = κ
hN : #(↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2) = κ
x : Field M := fieldOfModelACF p M
this : M ⊨ Theory.field
x_1 : CompatibleRing M := compatibleRingOfModelField M
⊢ IsAlgClosed M

Tactic:
have := isAlgClosed_of_model_ACF p M
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
p : ℕ
κ : Cardinal.{u_2}
hκ : ℵ₀ < κ
M : Type u_2
struc : Language.ring.Structure M
is_model : M ⊨ Theory.ACF p
nonempty' : Nonempty M
N : Type u_2
struc_1 : Language.ring.Structure N
is_model_1 : N ⊨ Theory.ACF p
nonempty'_1 : Nonempty N
hM : #(↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) = κ
hN : #(↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2) = κ
x : Field M := fieldOfModelACF p M
this_1 : M ⊨ Theory.field
x_1 : CompatibleRing M := compatibleRingOfModelField M
this : IsAlgClosed M
⊢ CharP M p

Tactic:
have := charP_of_model_fieldOfChar p M
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
p : ℕ
κ : Cardinal.{u_2}
hκ : ℵ₀ < κ
M : Type u_2
struc : Language.ring.Structure M
is_model : M ⊨ Theory.ACF p
nonempty' : Nonempty M
N : Type u_2
struc_1 : Language.ring.Structure N
is_model_1 : N ⊨ Theory.ACF p
nonempty'_1 : Nonempty N
hM : #(↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) = κ
hN : #(↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2) = κ
x : Field M := fieldOfModelACF p M
this_1 : M ⊨ Theory.field
x_1 : CompatibleRing M := compatibleRingOfModelField M
this_2 : IsAlgClosed M
this : CharP M p
x_2 : Field N := fieldOfModelACF p N
⊢ N ⊨ Theory.field

Tactic:
have := modelField_of_modelACF p N
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
p : ℕ
κ : Cardinal.{u_2}
hκ : ℵ₀ < κ
M : Type u_2
struc : Language.ring.Structure M
is_model : M ⊨ Theory.ACF p
nonempty' : Nonempty M
N : Type u_2
struc_1 : Language.ring.Structure N
is_model_1 : N ⊨ Theory.ACF p
nonempty'_1 : Nonempty N
hM : #(↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) = κ
hN : #(↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2) = κ
x : Field M := fieldOfModelACF p M
this_1 : M ⊨ Theory.field
x_1 : CompatibleRing M := compatibleRingOfModelField M
this_2 : IsAlgClosed M
this_3 : CharP M p
x_2 : Field N := fieldOfModelACF p N
this : N ⊨ Theory.field
x_3 : CompatibleRing N := compatibleRingOfModelField N
⊢ IsAlgClosed N

Tactic:
have := isAlgClosed_of_model_ACF p N
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
p : ℕ
κ : Cardinal.{u_2}
hκ : ℵ₀ < κ
M : Type u_2
struc : Language.ring.Structure M
is_model : M ⊨ Theory.ACF p
nonempty' : Nonempty M
N : Type u_2
struc_1 : Language.ring.Structure N
is_model_1 : N ⊨ Theory.ACF p
nonempty'_1 : Nonempty N
hM : #(↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) = κ
hN : #(↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2) = κ
x : Field M := fieldOfModelACF p M
this_1 : M ⊨ Theory.field
x_1 : CompatibleRing M := compatibleRingOfModelField M
this_2 : IsAlgClosed M
this_3 : CharP M p
x_2 : Field N := fieldOfModelACF p N
this_4 : N ⊨ Theory.field
x_3 : CompatibleRing N := compatibleRingOfModelField N
this : IsAlgClosed N
⊢ CharP N p

Tactic:
have := charP_of_model_fieldOfChar p N
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
p : ℕ
κ : Cardinal.{u_2}
hκ : ℵ₀ < κ
M : Type u_2
struc : Language.ring.Structure M
is_model : M ⊨ Theory.ACF p
nonempty' : Nonempty M
N : Type u_2
struc_1 : Language.ring.Structure N
is_model_1 : N ⊨ Theory.ACF p
nonempty'_1 : Nonempty N
hM : #(↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) = κ
hN : #(↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2) = κ
x : Field M := fieldOfModelACF p M
this_1 : M ⊨ Theory.field
x_1 : CompatibleRing M := compatibleRingOfModelField M
this_2 : IsAlgClosed M
this_3 : CharP M p
x_2 : Field N := fieldOfModelACF p N
this_4 : N ⊨ Theory.field
x_3 : CompatibleRing N := compatibleRingOfModelField N
this_5 : IsAlgClosed N
this : CharP N p
val :
  (↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) ≃[Language.ring]
    (↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2)
⊢ Nonempty.{u_2 + 1}
    ((↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) ≃[Language.ring]
      (↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2))

Tactic:
constructor
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
p : ℕ
κ : Cardinal.{u_2}
hκ : ℵ₀ < κ
M : Type u_2
struc : Language.ring.Structure M
is_model : M ⊨ Theory.ACF p
nonempty' : Nonempty M
N : Type u_2
struc_1 : Language.ring.Structure N
is_model_1 : N ⊨ Theory.ACF p
nonempty'_1 : Nonempty N
hM : #(↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) = κ
hN : #(↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2) = κ
x : Field M := fieldOfModelACF p M
this_1 : M ⊨ Theory.field
x_1 : CompatibleRing M := compatibleRingOfModelField M
this_2 : IsAlgClosed M
this_3 : CharP M p
x_2 : Field N := fieldOfModelACF p N
this_4 : N ⊨ Theory.field
x_3 : CompatibleRing N := compatibleRingOfModelField N
this_5 : IsAlgClosed N
this : CharP N p
val :
  (↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) ≃+*
    (↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2)
⊢ (↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) ≃[Language.ring]
    (↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2)

Tactic:
refine languageEquivEquivRingEquiv.symm ?_

Premises used: FirstOrder.Ring.languageEquivEquivRingEquiv, Equiv.symm, DFunLike.coe
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
p : ℕ
κ : Cardinal.{u_2}
hκ : ℵ₀ < κ
M : Type u_2
struc : Language.ring.Structure M
is_model : M ⊨ Theory.ACF p
nonempty' : Nonempty M
N : Type u_2
struc_1 : Language.ring.Structure N
is_model_1 : N ⊨ Theory.ACF p
nonempty'_1 : Nonempty N
hM : #(↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) = κ
hN : #(↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2) = κ
x : Field M := fieldOfModelACF p M
this_1 : M ⊨ Theory.field
x_1 : CompatibleRing M := compatibleRingOfModelField M
this_2 : IsAlgClosed M
this_3 : CharP M p
x_2 : Field N := fieldOfModelACF p N
this_4 : N ⊨ Theory.field
x_3 : CompatibleRing N := compatibleRingOfModelField N
this_5 : IsAlgClosed N
this : CharP N p
val :
  Nonempty.{u_2 + 1}
    ((↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) ≃+*
      (↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2))
⊢ (↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) ≃+*
    (↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2)

Tactic:
apply Classical.choice

Premises used: Classical.choice
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
p : ℕ
κ : Cardinal.{u_2}
hκ : ℵ₀ < κ
M : Type u_2
struc : Language.ring.Structure M
is_model : M ⊨ Theory.ACF p
nonempty' : Nonempty M
N : Type u_2
struc_1 : Language.ring.Structure N
is_model_1 : N ⊨ Theory.ACF p
nonempty'_1 : Nonempty N
hM : #(↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) = κ
hN : #(↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2) = κ
x : Field M := fieldOfModelACF p M
this_1 : M ⊨ Theory.field
x_1 : CompatibleRing M := compatibleRingOfModelField M
this_2 : IsAlgClosed M
this_3 : CharP M p
x_2 : Field N := fieldOfModelACF p N
this_4 : N ⊨ Theory.field
x_3 : CompatibleRing N := compatibleRingOfModelField N
this_5 : IsAlgClosed N
this : CharP N p
⊢ Nonempty.{u_2 + 1}
    ((↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) ≃+*
      (↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2))

Tactic:
IsAlgClosed.ringEquiv_of_equiv_of_char_eq p ?_ ?_

Premises used: IsAlgClosed.ringEquiv_of_equiv_of_char_eq
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
p : ℕ
κ : Cardinal.{u_2}
hκ : ℵ₀ < κ
M : Type u_2
struc : Language.ring.Structure M
is_model : M ⊨ Theory.ACF p
nonempty' : Nonempty M
N : Type u_2
struc_1 : Language.ring.Structure N
is_model_1 : N ⊨ Theory.ACF p
nonempty'_1 : Nonempty N
hM : #(↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) = κ
hN : #(↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2) = κ
x : Field M := fieldOfModelACF p M
this_1 : M ⊨ Theory.field
x_1 : CompatibleRing M := compatibleRingOfModelField M
this_2 : IsAlgClosed M
this_3 : CharP M p
x_2 : Field N := fieldOfModelACF p N
this_4 : N ⊨ Theory.field
x_3 : CompatibleRing N := compatibleRingOfModelField N
this_5 : IsAlgClosed N
this : CharP N p
val : ℵ₀ < #(↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2)
val₁ :
  Nonempty.{u_2 + 1}
    ((↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) ≃
      (↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2))
⊢ Nonempty.{u_2 + 1}
    ((↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) ≃+*
      (↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2))

Tactic:
refine IsAlgClosed.ringEquiv_of_equiv_of_char_eq p ?_ ?_

Premises used: IsAlgClosed.ringEquiv_of_equiv_of_char_eq
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
p : ℕ
κ : Cardinal.{u_2}
hκ : ℵ₀ < κ
M : Type u_2
struc : Language.ring.Structure M
is_model : M ⊨ Theory.ACF p
nonempty' : Nonempty M
N : Type u_2
struc_1 : Language.ring.Structure N
is_model_1 : N ⊨ Theory.ACF p
nonempty'_1 : Nonempty N
hM : #(↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) = κ
hN : #(↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2) = κ
x : Field M := fieldOfModelACF p M
this_1 : M ⊨ Theory.field
x_1 : CompatibleRing M := compatibleRingOfModelField M
this_2 : IsAlgClosed M
this_3 : CharP M p
x_2 : Field N := fieldOfModelACF p N
this_4 : N ⊨ Theory.field
x_3 : CompatibleRing N := compatibleRingOfModelField N
this_5 : IsAlgClosed N
this : CharP N p
val : ℵ₀ < κ
⊢ ℵ₀ < #(↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2)

Tactic:
rw [hM]
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
p : ℕ
κ : Cardinal.{u_2}
hκ : ℵ₀ < κ
M : Type u_2
struc : Language.ring.Structure M
is_model : M ⊨ Theory.ACF p
nonempty' : Nonempty M
N : Type u_2
struc_1 : Language.ring.Structure N
is_model_1 : N ⊨ Theory.ACF p
nonempty'_1 : Nonempty N
hM : #(↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) = κ
hN : #(↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2) = κ
x : Field M := fieldOfModelACF p M
this_1 : M ⊨ Theory.field
x_1 : CompatibleRing M := compatibleRingOfModelField M
this_2 : IsAlgClosed M
this_3 : CharP M p
x_2 : Field N := fieldOfModelACF p N
this_4 : N ⊨ Theory.field
x_3 : CompatibleRing N := compatibleRingOfModelField N
this_5 : IsAlgClosed N
this : CharP N p
⊢ ℵ₀ < κ

Tactic:
hκ
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
p : ℕ
κ : Cardinal.{u_2}
hκ : ℵ₀ < κ
M : Type u_2
struc : Language.ring.Structure M
is_model : M ⊨ Theory.ACF p
nonempty' : Nonempty M
N : Type u_2
struc_1 : Language.ring.Structure N
is_model_1 : N ⊨ Theory.ACF p
nonempty'_1 : Nonempty N
hM : #(↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) = κ
hN : #(↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2) = κ
x : Field M := fieldOfModelACF p M
this_1 : M ⊨ Theory.field
x_1 : CompatibleRing M := compatibleRingOfModelField M
this_2 : IsAlgClosed M
this_3 : CharP M p
x_2 : Field N := fieldOfModelACF p N
this_4 : N ⊨ Theory.field
x_3 : CompatibleRing N := compatibleRingOfModelField N
this_5 : IsAlgClosed N
this : CharP N p
⊢ ℵ₀ < κ

Tactic:
exact hκ
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
p : ℕ
κ : Cardinal.{u_2}
hκ : ℵ₀ < κ
M : Type u_2
struc : Language.ring.Structure M
is_model : M ⊨ Theory.ACF p
nonempty' : Nonempty M
N : Type u_2
struc_1 : Language.ring.Structure N
is_model_1 : N ⊨ Theory.ACF p
nonempty'_1 : Nonempty N
hM : #(↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) = κ
hN : #(↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2) = κ
x : Field M := fieldOfModelACF p M
this_1 : M ⊨ Theory.field
x_1 : CompatibleRing M := compatibleRingOfModelField M
this_2 : IsAlgClosed M
this_3 : CharP M p
x_2 : Field N := fieldOfModelACF p N
this_4 : N ⊨ Theory.field
x_3 : CompatibleRing N := compatibleRingOfModelField N
this_5 : IsAlgClosed N
this : CharP N p
val :
  #(↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) =
    #(↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2)
val₁ : κ = #(↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2)
val₂ val₃ : κ = κ
⊢ Nonempty.{u_2 + 1}
    ((↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type u_2) ≃
      (↑(Theory.ModelType.mk (T := Theory.ACF p) N) : Type u_2))

Tactic:
rw [← Cardinal.eq, hM, hN]

Premises used: Cardinal.eq
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
p : ℕ
hp : Nat.Prime p ∨ p = 0
h2 : Cardinal.lift.{0, 0} Language.ring.card ≤ Cardinal.lift.{0, 0} (Order.succ ℵ₀)
hS : (Theory.ACF p).IsSatisfiable
hT : ∀ (M : (Theory.ACF p).ModelType), Infinite (↑M : Type)
⊢ (Theory.ACF p).IsComplete

Tactic:
apply Categorical.isComplete.{0, 0, 0} (Order.succ ℵ₀) _
    (ACF_categorical _ (Order.lt_succ _))
    (Order.le_succ ℵ₀)

Premises used: Order.succ, FirstOrder.Field.ACF_categorical, Cardinal.aleph0, Order.lt_succ, Order.le_succ, Cardinal.Categorical.isComplete
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
p : ℕ
hp : Nat.Prime p ∨ p = 0
h2 : 5 ≤ Order.succ ℵ₀
⊢ Cardinal.lift.{0, 0} Language.ring.card ≤ Cardinal.lift.{0, 0} (Order.succ ℵ₀)

Tactic:
simp only [card_ring, lift_id']

Premises used: Cardinal.lift_id', FirstOrder.Ring.card_ring
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
p : ℕ
hp : Nat.Prime p ∨ p = 0
⊢ 5 ≤ Order.succ ℵ₀

Tactic:
le_trans (le_of_lt (lt_aleph0_of_finite _)) (Order.le_succ _)

Premises used: le_of_lt, Cardinal.lt_aleph0_of_finite, Order.le_succ, le_trans
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
p : ℕ
hp : Nat.Prime p ∨ p = 0
⊢ 5 ≤ Order.succ ℵ₀

Tactic:
exact le_trans (le_of_lt (lt_aleph0_of_finite _)) (Order.le_succ _)

Premises used: le_of_lt, Cardinal.lt_aleph0_of_finite, Order.le_succ, le_trans
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
p : ℕ
hp : Nat.Prime p ∨ p = 0
⊢ (Theory.ACF p).IsSatisfiable

Tactic:
ACF_isSatisfiable hp

Premises used: FirstOrder.Field.ACF_isSatisfiable
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
p : ℕ
hp : Nat.Prime p ∨ p = 0
⊢ (Theory.ACF p).IsSatisfiable

Tactic:
exact ACF_isSatisfiable hp

Premises used: FirstOrder.Field.ACF_isSatisfiable
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
p : ℕ
hp : Nat.Prime p ∨ p = 0
M : Type
struc : Language.ring.Structure M
is_model : M ⊨ Theory.ACF p
nonempty' : Nonempty M
x : Field M := fieldOfModelACF p M
⊢ M ⊨ Theory.field

Tactic:
have := modelField_of_modelACF p M
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
p : ℕ
hp : Nat.Prime p ∨ p = 0
M : Type
struc : Language.ring.Structure M
is_model : M ⊨ Theory.ACF p
nonempty' : Nonempty M
x : Field M := fieldOfModelACF p M
this : M ⊨ Theory.field
x_1 : CompatibleRing M := compatibleRingOfModelField M
⊢ IsAlgClosed M

Tactic:
have := isAlgClosed_of_model_ACF p M
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
p : ℕ
hp : Nat.Prime p ∨ p = 0
M : Type
struc : Language.ring.Structure M
is_model : M ⊨ Theory.ACF p
nonempty' : Nonempty M
x : Field M := fieldOfModelACF p M
this_1 : M ⊨ Theory.field
x_1 : CompatibleRing M := compatibleRingOfModelField M
this : IsAlgClosed M
⊢ Infinite (↑(Theory.ModelType.mk (T := Theory.ACF p) M) : Type)

Tactic:
infer_instance
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
φ : Language.ring.Sentence
h : Theory.ACF 0 ⊨ᵇ φ
⊢ ∃ (T0 : Finset Language.ring.Sentence),
    (↑T0 : Set Language.ring.Sentence) ⊆ Theory.ACF 0 ∧ (↑T0 : Set Language.ring.Sentence) ⊨ᵇ φ

Tactic:
rw [Theory.models_iff_finset_models] at h

Premises used: FirstOrder.Language.Theory.models_iff_finset_models
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
φ : Language.ring.Sentence
h :
  ∃ (T0 : Finset Language.ring.Sentence),
    (↑T0 : Set Language.ring.Sentence) ⊆ Theory.ACF 0 ∧ (↑T0 : Set Language.ring.Sentence) ⊨ᵇ φ
rcases :
  ∀ (T0 : Finset Language.ring.Sentence) (hT0 : (↑T0 : Set Language.ring.Sentence) ⊆ Theory.ACF 0)
    (h : (↑T0 : Set Language.ring.Sentence) ⊨ᵇ φ),
    Set.Finite (α := Nat.Primes) {p : Nat.Primes | ¬Theory.ACF (↑p : ℕ) ⊨ᵇ φ}
⊢ Set.Finite (α := Nat.Primes) {p : Nat.Primes | ¬Theory.ACF (↑p : ℕ) ⊨ᵇ φ}

Tactic:
rcases h with ⟨T0, hT0, h⟩
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : (↑T0 : Set Language.ring.Sentence) ⊆ Theory.ACF 0
h : (↑T0 : Set Language.ring.Sentence) ⊨ᵇ φ
ψ : Language.ring.Sentence
hψ : ψ ∈ Theory.ACF 0
⊢ ψ ∈ Theory.field ∪ genericMonicPolyHasRoot '' {n : ℕ | 0 < n} ∨
    ∃ (x : ℕ), Membership.mem (γ := Set ℕ) {q : ℕ | Nat.Prime q} x ∧ ∼(eqZero x) = ψ

Tactic:
rw [Theory.ACF, Theory.fieldOfChar, Set.union_right_comm, Set.mem_union, if_pos rfl,
      Set.mem_image] at hψ

Premises used: Set.mem_union, FirstOrder.Language.Theory.ACF, Set.mem_image, if_pos, FirstOrder.Language.Theory.fieldOfChar, Set.union_right_comm, rfl
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : (↑T0 : Set Language.ring.Sentence) ⊆ Theory.ACF 0
h : (↑T0 : Set Language.ring.Sentence) ⊨ᵇ φ
ψ : Language.ring.Sentence
hψ :
  ψ ∈ Theory.field ∪ genericMonicPolyHasRoot '' {n : ℕ | 0 < n} ∨
    ∃ (x : ℕ), Membership.mem (γ := Set ℕ) {q : ℕ | Nat.Prime q} x ∧ ∼(eqZero x) = ψ
a : Nonempty { s : Finset Nat.Primes // ∀ q ∉ s, Theory.ACF (↑q : ℕ) ⊨ᵇ ψ }
⊢ { s : Finset Nat.Primes // ∀ q ∉ s, Theory.ACF (↑q : ℕ) ⊨ᵇ ψ }

Tactic:
apply Classical.choice

Premises used: Classical.choice
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : (↑T0 : Set Language.ring.Sentence) ⊆ Theory.ACF 0
h : (↑T0 : Set Language.ring.Sentence) ⊨ᵇ φ
ψ : Language.ring.Sentence
hψ :
  ψ ∈ Theory.field ∪ genericMonicPolyHasRoot '' {n : ℕ | 0 < n} ∨
    ∃ (x : ℕ), Membership.mem (γ := Set ℕ) {q : ℕ | Nat.Prime q} x ∧ ∼(eqZero x) = ψ
a :
  ∀ (h : ψ ∈ Theory.field ∪ genericMonicPolyHasRoot '' {n : ℕ | 0 < n}),
    Nonempty { s : Finset Nat.Primes // ∀ q ∉ s, Theory.ACF (↑q : ℕ) ⊨ᵇ ψ }
a₁ :
  ∀ (p : ℕ) (hp : Membership.mem (γ := Set ℕ) {q : ℕ | Nat.Prime q} p),
    Nonempty { s : Finset Nat.Primes // ∀ q ∉ s, Theory.ACF (↑q : ℕ) ⊨ᵇ ∼(eqZero p) }
⊢ Nonempty { s : Finset Nat.Primes // ∀ q ∉ s, Theory.ACF (↑q : ℕ) ⊨ᵇ ψ }

Tactic:
rcases hψ with h | ⟨p, hp, rfl⟩

Premises used: rfl