awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_1 : (↑T0 : Set Language.ring.Sentence) ⊨ᵇ φ
ψ : Language.ring.Sentence
h : ψ ∈ Theory.field ∪ genericMonicPolyHasRoot '' {n : ℕ | 0 < n}
⊢ Nonempty { s : Finset Nat.Primes // ∀ q ∉ s, Theory.ACF (↑q : ℕ) ⊨ᵇ ψ }

Tactic:
⟨⟨∅, ?_⟩⟩

Premises used: Nonempty.intro, Subtype.mk, EmptyCollection.emptyCollection
-- 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_1 : (↑T0 : Set Language.ring.Sentence) ⊨ᵇ φ
ψ : Language.ring.Sentence
h : ψ ∈ Theory.field ∪ genericMonicPolyHasRoot '' {n : ℕ | 0 < n}
a : ∀ q ∉ ∅, Theory.ACF (↑q : ℕ) ⊨ᵇ ψ
⊢ Nonempty { s : Finset Nat.Primes // ∀ q ∉ s, Theory.ACF (↑q : ℕ) ⊨ᵇ ψ }

Tactic:
refine ⟨⟨∅, ?_⟩⟩
-- 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_1 : (↑T0 : Set Language.ring.Sentence) ⊨ᵇ φ
ψ : Language.ring.Sentence
h : ψ ∈ Theory.field ∪ genericMonicPolyHasRoot '' {n : ℕ | 0 < n}
q : Nat.Primes
a : q ∉ ∅ → Theory.ACF (↑q : ℕ) ⊨ᵇ ψ
⊢ q ∉ ∅ → Theory.ACF (↑q : ℕ) ⊨ᵇ ψ

Tactic:
_
-- 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_1 : (↑T0 : Set Language.ring.Sentence) ⊨ᵇ φ
ψ : Language.ring.Sentence
h : ψ ∈ Theory.field ∪ genericMonicPolyHasRoot '' {n : ℕ | 0 < n}
q : Nat.Primes
h_2 : q ∉ ∅
rw :
  ψ ∈
    Theory.field ∪ genericMonicPolyHasRoot '' {n : ℕ | 0 < n} ∪
      if (↑q : ℕ) = 0 then (fun (q : ℕ) ↦ ∼(eqZero q)) '' {q : ℕ | Nat.Prime q}
      else if Nat.Prime (↑q : ℕ) then {eqZero (↑q : ℕ)} else {⊥}
⊢ ψ ∈ Theory.ACF (↑q : ℕ)

Tactic:
rw [Theory.ACF, Theory.fieldOfChar, Set.union_right_comm]

Premises used: FirstOrder.Language.Theory.ACF, FirstOrder.Language.Theory.fieldOfChar, Set.union_right_comm
-- 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_1 : (↑T0 : Set Language.ring.Sentence) ⊨ᵇ φ
ψ : Language.ring.Sentence
h : ψ ∈ Theory.field ∪ genericMonicPolyHasRoot '' {n : ℕ | 0 < n}
q : Nat.Primes
h_2 : q ∉ ∅
⊢ ψ ∈
    Theory.field ∪ genericMonicPolyHasRoot '' {n : ℕ | 0 < n} ∪
      if (↑q : ℕ) = 0 then (fun (q : ℕ) ↦ ∼(eqZero q)) '' {q : ℕ | Nat.Prime q}
      else if Nat.Prime (↑q : ℕ) then {eqZero (↑q : ℕ)} else {⊥}

Tactic:
Set.mem_union_left _ h

Premises used: Set.mem_union_left
-- 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_1 : (↑T0 : Set Language.ring.Sentence) ⊨ᵇ φ
ψ : Language.ring.Sentence
h : ψ ∈ Theory.field ∪ genericMonicPolyHasRoot '' {n : ℕ | 0 < n}
q : Nat.Primes
h_2 : q ∉ ∅
⊢ ψ ∈
    Theory.field ∪ genericMonicPolyHasRoot '' {n : ℕ | 0 < n} ∪
      if (↑q : ℕ) = 0 then (fun (q : ℕ) ↦ ∼(eqZero q)) '' {q : ℕ | Nat.Prime q}
      else if Nat.Prime (↑q : ℕ) then {eqZero (↑q : ℕ)} else {⊥}

Tactic:
exact Set.mem_union_left _ h

Premises used: Set.mem_union_left
-- 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_1 : (↑T0 : Set Language.ring.Sentence) ⊨ᵇ φ
ψ : Language.ring.Sentence
h : ψ ∈ Theory.field ∪ genericMonicPolyHasRoot '' {n : ℕ | 0 < n}
q : Nat.Primes
h_2 : q ∉ ∅
⊢ Theory.ACF (↑q : ℕ) ⊨ᵇ ψ

Tactic:
exact Theory.models_sentence_of_mem
        (by rw [Theory.ACF, Theory.fieldOfChar, Set.union_right_comm];
            exact Set.mem_union_left _ h)

Premises used: FirstOrder.Language.Theory.models_sentence_of_mem
-- 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) ⊨ᵇ φ
p : ℕ
hp : Membership.mem (γ := Set ℕ) {q : ℕ | Nat.Prime q} p
⊢ Nonempty { s : Finset Nat.Primes // ∀ q ∉ s, Theory.ACF (↑q : ℕ) ⊨ᵇ ∼(eqZero p) }

Tactic:
⟨⟨{⟨p, hp⟩}, ?_⟩⟩

Premises used: Nonempty.intro, Subtype.mk, Singleton.singleton
-- 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) ⊨ᵇ φ
p : ℕ
hp : Membership.mem (γ := Set ℕ) {q : ℕ | Nat.Prime q} p
a : ∀ q ∉ {Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) p hp}, Theory.ACF (↑q : ℕ) ⊨ᵇ ∼(eqZero p)
⊢ Nonempty { s : Finset Nat.Primes // ∀ q ∉ s, Theory.ACF (↑q : ℕ) ⊨ᵇ ∼(eqZero p) }

Tactic:
refine ⟨⟨{⟨p, hp⟩}, ?_⟩⟩
-- 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) ⊨ᵇ φ
p : ℕ
hp : Membership.mem (γ := Set ℕ) {q : ℕ | Nat.Prime q} p
q : ℕ
property : Nat.Prime q
hq : Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property ∉ {Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) p hp}
K : Type
struc : Language.ring.Structure K
is_model : K ⊨ Theory.ACF (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property) : ℕ)
nonempty' : Nonempty K
v :
  Empty →
    (↑(Theory.ModelType.mk (T := Theory.ACF (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property) : ℕ)) K) : Type)
xs :
  Fin 0 →
    (↑(Theory.ModelType.mk (T := Theory.ACF (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property) : ℕ)) K) : Type)
⊢ q ≠ p

Tactic:
simpa [← Nat.Primes.coe_nat_inj] using hq

Premises used: Nat.Primes.coe_nat_inj
-- 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) ⊨ᵇ φ
p : ℕ
hp : Membership.mem (γ := Set ℕ) {q : ℕ | Nat.Prime q} p
q : ℕ
property : Nat.Prime q
hq : Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property ∉ {Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) p hp}
K : Type
struc : Language.ring.Structure K
is_model : K ⊨ Theory.ACF (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property) : ℕ)
nonempty' : Nonempty K
v :
  Empty →
    (↑(Theory.ModelType.mk (T := Theory.ACF (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property) : ℕ)) K) : Type)
xs :
  Fin 0 →
    (↑(Theory.ModelType.mk (T := Theory.ACF (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property) : ℕ)) K) : Type)
⊢ q ≠ p

Tactic:
have hqp : q ≠ p := by simpa [← Nat.Primes.coe_nat_inj] using hq
-- 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) ⊨ᵇ φ
p : ℕ
hp : Membership.mem (γ := Set ℕ) {q : ℕ | Nat.Prime q} p
q : ℕ
property : Nat.Prime q
hq : Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property ∉ {Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) p hp}
K : Type
struc : Language.ring.Structure K
is_model : K ⊨ Theory.ACF (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property) : ℕ)
nonempty' : Nonempty K
v :
  Empty →
    (↑(Theory.ModelType.mk (T := Theory.ACF (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property) : ℕ)) K) : Type)
xs :
  Fin 0 →
    (↑(Theory.ModelType.mk (T := Theory.ACF (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property) : ℕ)) K) : Type)
hqp : q ≠ p
x : Field K := fieldOfModelACF q K
⊢ K ⊨ Theory.field

Tactic:
have := modelField_of_modelACF q K
-- 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) ⊨ᵇ φ
p : ℕ
hp : Membership.mem (γ := Set ℕ) {q : ℕ | Nat.Prime q} p
q : ℕ
property : Nat.Prime q
hq : Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property ∉ {Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) p hp}
K : Type
struc : Language.ring.Structure K
is_model : K ⊨ Theory.ACF (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property) : ℕ)
nonempty' : Nonempty K
v :
  Empty →
    (↑(Theory.ModelType.mk (T := Theory.ACF (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property) : ℕ)) K) : Type)
xs :
  Fin 0 →
    (↑(Theory.ModelType.mk (T := Theory.ACF (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property) : ℕ)) K) : Type)
hqp : q ≠ p
x : Field K := fieldOfModelACF q K
this : K ⊨ Theory.field
x_1 : CompatibleRing K := compatibleRingOfModelField K
⊢ CharP K q

Tactic:
have := charP_of_model_fieldOfChar q K
-- 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) ⊨ᵇ φ
p : ℕ
hp : Membership.mem (γ := Set ℕ) {q : ℕ | Nat.Prime q} p
q : ℕ
property : Nat.Prime q
hq : Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property ∉ {Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) p hp}
K : Type
struc : Language.ring.Structure K
is_model : K ⊨ Theory.ACF (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property) : ℕ)
nonempty' : Nonempty K
v :
  Empty →
    (↑(Theory.ModelType.mk (T := Theory.ACF (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property) : ℕ)) K) : Type)
xs :
  Fin 0 →
    (↑(Theory.ModelType.mk (T := Theory.ACF (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property) : ℕ)) K) : Type)
hqp : q ≠ p
x : Field K := fieldOfModelACF q K
this_1 : K ⊨ Theory.field
x_1 : CompatibleRing K := compatibleRingOfModelField K
this : CharP K q
a : ¬CharP K p
⊢ (∼(eqZero p)).Realize v xs

Tactic:
simp only [eqZero, Term.equal, BoundedFormula.realize_not, BoundedFormula.realize_bdEqual,
        Term.realize_relabel, Sum.elim_comp_inl, realize_termOfFreeCommRing, map_natCast,
        realize_zero, ← CharP.charP_iff_prime_eq_zero hp]

Premises used: FirstOrder.Ring.realize_termOfFreeCommRing, Sum.elim_comp_inl, FirstOrder.Language.BoundedFormula.realize_not, FirstOrder.Language.Term.realize_relabel, FirstOrder.Language.Term.equal, FirstOrder.Field.eqZero, map_natCast, FirstOrder.Ring.realize_zero, FirstOrder.Language.BoundedFormula.realize_bdEqual, CharP.charP_iff_prime_eq_zero
-- 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) ⊨ᵇ φ
p : ℕ
hp : Membership.mem (γ := Set ℕ) {q : ℕ | Nat.Prime q} p
q : ℕ
property : Nat.Prime q
hq : Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property ∉ {Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) p hp}
K : Type
struc : Language.ring.Structure K
is_model : K ⊨ Theory.ACF (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property) : ℕ)
nonempty' : Nonempty K
v :
  Empty →
    (↑(Theory.ModelType.mk (T := Theory.ACF (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property) : ℕ)) K) : Type)
xs :
  Fin 0 →
    (↑(Theory.ModelType.mk (T := Theory.ACF (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property) : ℕ)) K) : Type)
hqp : q ≠ p
x : Field K := fieldOfModelACF q K
this_1 : K ⊨ Theory.field
x_1 : CompatibleRing K := compatibleRingOfModelField K
this : CharP K q
h_1 : CharP K p
⊢ False

Tactic:
hqp <| CharP.eq K this inferInstance

Premises used: inferInstance, CharP.eq
-- 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) ⊨ᵇ φ
p : ℕ
hp : Membership.mem (γ := Set ℕ) {q : ℕ | Nat.Prime q} p
q : ℕ
property : Nat.Prime q
hq : Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property ∉ {Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) p hp}
K : Type
struc : Language.ring.Structure K
is_model : K ⊨ Theory.ACF (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property) : ℕ)
nonempty' : Nonempty K
v :
  Empty →
    (↑(Theory.ModelType.mk (T := Theory.ACF (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property) : ℕ)) K) : Type)
xs :
  Fin 0 →
    (↑(Theory.ModelType.mk (T := Theory.ACF (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property) : ℕ)) K) : Type)
hqp : q ≠ p
x : Field K := fieldOfModelACF q K
this_1 : K ⊨ Theory.field
x_1 : CompatibleRing K := compatibleRingOfModelField K
this : CharP K q
h_1 : CharP K p
⊢ False

Tactic:
exact hqp <| CharP.eq K this inferInstance

Premises used: inferInstance, CharP.eq
-- 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) ⊨ᵇ φ
have :
  ∀
    (f :
      (ψ : Language.ring.Sentence) → ψ ∈ Theory.ACF 0 → { s : Finset Nat.Primes // ∀ q ∉ s, Theory.ACF (↑q : ℕ) ⊨ᵇ ψ }),
    Set.Finite (α := Nat.Primes) {p : Nat.Primes | ¬Theory.ACF (↑p : ℕ) ⊨ᵇ φ}
⊢ Set.Finite (α := Nat.Primes) {p : Nat.Primes | ¬Theory.ACF (↑p : ℕ) ⊨ᵇ φ}

Tactic:
have f : ∀ ψ ∈ Theory.ACF 0,
      { s : Finset Nat.Primes // ∀ q : Nat.Primes, q ∉ s → Theory.ACF q ⊨ᵇ ψ } := by
    intro ψ hψ
    rw [Theory.ACF, Theory.fieldOfChar, Set.union_right_comm, Set.mem_union, if_pos rfl,
      Set.mem_image] at hψ
    apply Classical.choice
    rcases hψ with h | ⟨p, hp, rfl⟩
    · refine ⟨⟨∅, ?_⟩⟩
      intro q _
      exact Theory.models_sentence_of_mem
        (by rw [Theory.ACF, Theory.fieldOfChar, Set.union_right_comm];
            exact Set.mem_union_left _ h)
    · refine ⟨⟨{⟨p, hp⟩}, ?_⟩⟩
      rintro ⟨q, _⟩ hq ⟨K⟩ _ _
      have hqp : q ≠ p := by simpa [← Nat.Primes.coe_nat_inj] using hq
      let _ := fieldOfModelACF q K
      have := modelField_of_modelACF q K
      let _ := compatibleRingOfModelField K
      have := charP_of_model_fieldOfChar q K
      simp only [eqZero, Term.equal, BoundedFormula.realize_not, BoundedFormula.realize_bdEqual,
        Term.realize_relabel, Sum.elim_comp_inl, realize_termOfFreeCommRing, map_natCast,
        realize_zero, ← CharP.charP_iff_prime_eq_zero hp]
      intro _
      exact hqp <| CharP.eq K this inferInstance
-- 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) ⊨ᵇ φ
f : (ψ : Language.ring.Sentence) → ψ ∈ Theory.ACF 0 → { s : Finset Nat.Primes // ∀ q ∉ s, Theory.ACF (↑q : ℕ) ⊨ᵇ ψ }
s : Finset Nat.Primes := T0.attach.biUnion fun (φ : ↥T0) ↦ (↑(f (↑φ : Language.ring.Sentence) ⋯) : Finset Nat.Primes)
p : Nat.Primes
ψ : Language.ring.Sentence
hψ : ψ ∈ T0
hpψ : p ∉ s
⊢ ∀ (x : Language.ring.Sentence) (x_1 : x ∈ T0), p ∉ (↑(f x ⋯) : Finset Nat.Primes)

Tactic:
simp only [s, Finset.mem_biUnion, Finset.mem_attach, true_and,
      Subtype.exists, not_exists] at hpψ

Premises used: Finset.mem_attach, Subtype.exists, not_exists, Finset.mem_biUnion, true_and
-- 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) ⊨ᵇ φ
f : (ψ : Language.ring.Sentence) → ψ ∈ Theory.ACF 0 → { s : Finset Nat.Primes // ∀ q ∉ s, Theory.ACF (↑q : ℕ) ⊨ᵇ ψ }
s : Finset Nat.Primes := T0.attach.biUnion fun (φ : ↥T0) ↦ (↑(f (↑φ : Language.ring.Sentence) ⋯) : Finset Nat.Primes)
p : Nat.Primes
ψ : Language.ring.Sentence
hψ : ψ ∈ T0
hpψ : ∀ (x : Language.ring.Sentence) (x_1 : x ∈ T0), p ∉ (↑(f x ⋯) : Finset Nat.Primes)
⊢ Theory.ACF (↑p : ℕ) ⊨ᵇ ψ

Tactic:
(f ψ (hT0 hψ)).2 p (hpψ _ hψ)

Premises used: Subtype.property
-- 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) ⊨ᵇ φ
f : (ψ : Language.ring.Sentence) → ψ ∈ Theory.ACF 0 → { s : Finset Nat.Primes // ∀ q ∉ s, Theory.ACF (↑q : ℕ) ⊨ᵇ ψ }
s : Finset Nat.Primes := T0.attach.biUnion fun (φ : ↥T0) ↦ (↑(f (↑φ : Language.ring.Sentence) ⋯) : Finset Nat.Primes)
p : Nat.Primes
ψ : Language.ring.Sentence
hψ : ψ ∈ T0
hpψ : ∀ (x : Language.ring.Sentence) (x_1 : x ∈ T0), p ∉ (↑(f x ⋯) : Finset Nat.Primes)
⊢ Theory.ACF (↑p : ℕ) ⊨ᵇ ψ

Tactic:
exact (f ψ (hT0 hψ)).2 p (hpψ _ hψ)

Premises used: Subtype.property
-- 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) ⊨ᵇ φ
f : (ψ : Language.ring.Sentence) → ψ ∈ Theory.ACF 0 → { s : Finset Nat.Primes // ∀ q ∉ s, Theory.ACF (↑q : ℕ) ⊨ᵇ ψ }
s : Finset Nat.Primes := T0.attach.biUnion fun (φ : ↥T0) ↦ (↑(f (↑φ : Language.ring.Sentence) ⋯) : Finset Nat.Primes)
⊢ ∀ (p : Nat.Primes), ∀ ψ ∈ T0, p ∉ s → Theory.ACF (↑p : ℕ) ⊨ᵇ ψ

Tactic:
have hs : ∀ (p : Nat.Primes) ψ, ψ ∈ T0 → p ∉ s → Theory.ACF p ⊨ᵇ ψ := by
    intro p ψ hψ hpψ
    simp only [s, Finset.mem_biUnion, Finset.mem_attach, true_and,
      Subtype.exists, not_exists] at hpψ
    exact (f ψ (hT0 hψ)).2 p (hpψ _ 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) ⊨ᵇ φ
f : (ψ : Language.ring.Sentence) → ψ ∈ Theory.ACF 0 → { s : Finset Nat.Primes // ∀ q ∉ s, Theory.ACF (↑q : ℕ) ⊨ᵇ ψ }
s : Finset Nat.Primes := T0.attach.biUnion fun (φ : ↥T0) ↦ (↑(f (↑φ : Language.ring.Sentence) ⋯) : Finset Nat.Primes)
hs : ∀ (p : Nat.Primes), ∀ ψ ∈ T0, p ∉ s → Theory.ACF (↑p : ℕ) ⊨ᵇ ψ
⊢ Set.Finite (α := Nat.Primes) {p : Nat.Primes | ¬Theory.ACF (↑p : ℕ) ⊨ᵇ φ}

Tactic:
Set.Finite.subset (Finset.finite_toSet s) (Set.compl_subset_comm.2 ?_)

Premises used: Iff.mpr, Set.compl_subset_comm, Set.Finite.subset, Finset.finite_toSet
-- 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) ⊨ᵇ φ
f : (ψ : Language.ring.Sentence) → ψ ∈ Theory.ACF 0 → { s : Finset Nat.Primes // ∀ q ∉ s, Theory.ACF (↑q : ℕ) ⊨ᵇ ψ }
s : Finset Nat.Primes := T0.attach.biUnion fun (φ : ↥T0) ↦ (↑(f (↑φ : Language.ring.Sentence) ⋯) : Finset Nat.Primes)
hs : ∀ (p : Nat.Primes), ∀ ψ ∈ T0, p ∉ s → Theory.ACF (↑p : ℕ) ⊨ᵇ ψ
refine :
  (↑s : Set Nat.Primes)ᶜ ⊆ fun (p : Nat.Primes) ↦
    ∀ (M : (Theory.ACF (↑p : ℕ)).ModelType) (v : Empty → (↑M : Type)) (xs : Fin 0 → (↑M : Type)),
      BoundedFormula.Realize φ v xs
⊢ Set.Finite (α := Nat.Primes) {p : Nat.Primes | ¬Theory.ACF (↑p : ℕ) ⊨ᵇ φ}

Tactic:
refine Set.Finite.subset (Finset.finite_toSet s) (Set.compl_subset_comm.2 ?_)

Premises used: Iff.mpr, Set.compl_subset_comm, Set.Finite.subset, Finset.finite_toSet
-- 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) ⊨ᵇ φ
f : (ψ : Language.ring.Sentence) → ψ ∈ Theory.ACF 0 → { s : Finset Nat.Primes // ∀ q ∉ s, Theory.ACF (↑q : ℕ) ⊨ᵇ ψ }
s : Finset Nat.Primes := T0.attach.biUnion fun (φ : ↥T0) ↦ (↑(f (↑φ : Language.ring.Sentence) ⋯) : Finset Nat.Primes)
hs : ∀ (p : Nat.Primes), ∀ ψ ∈ T0, p ∉ s → Theory.ACF (↑p : ℕ) ⊨ᵇ ψ
p : Nat.Primes
hp : p ∈ (↑s : Set Nat.Primes)ᶜ
⊢ Membership.mem (γ := Set Nat.Primes)
    (fun (p : Nat.Primes) ↦
      ∀ (M : (Theory.ACF (↑p : ℕ)).ModelType) (v : Empty → (↑M : Type)) (xs : Fin 0 → (↑M : Type)),
        BoundedFormula.Realize φ v xs)
    p

Tactic:
Theory.models_of_models_theory (fun ψ hψ => hs p ψ hψ hp) h

Premises used: Set.Mem, FirstOrder.Language.Theory.ModelsBoundedFormula, FirstOrder.Language.Theory.models_of_models_theory
-- 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) ⊨ᵇ φ
f : (ψ : Language.ring.Sentence) → ψ ∈ Theory.ACF 0 → { s : Finset Nat.Primes // ∀ q ∉ s, Theory.ACF (↑q : ℕ) ⊨ᵇ ψ }
s : Finset Nat.Primes := T0.attach.biUnion fun (φ : ↥T0) ↦ (↑(f (↑φ : Language.ring.Sentence) ⋯) : Finset Nat.Primes)
hs : ∀ (p : Nat.Primes), ∀ ψ ∈ T0, p ∉ s → Theory.ACF (↑p : ℕ) ⊨ᵇ ψ
p : Nat.Primes
hp : p ∈ (↑s : Set Nat.Primes)ᶜ
⊢ Membership.mem (γ := Set Nat.Primes)
    (fun (p : Nat.Primes) ↦
      ∀ (M : (Theory.ACF (↑p : ℕ)).ModelType) (v : Empty → (↑M : Type)) (xs : Fin 0 → (↑M : Type)),
        BoundedFormula.Realize φ v xs)
    p

Tactic:
exact Theory.models_of_models_theory (fun ψ hψ => hs p ψ hψ hp) h

Premises used: FirstOrder.Language.Theory.models_of_models_theory
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
φ : Language.ring.Sentence
⊢ Theory.ACF 0 ⊨ᵇ φ ↔ Set.Infinite (α := Nat.Primes) {p : Nat.Primes | Theory.ACF (↑p : ℕ) ⊨ᵇ φ}

Tactic:
⟨fun h => Set.infinite_of_finite_compl
      (finite_ACF_prime_not_realize_of_ACF_zero_realize φ h),
    not_imp_not.1 ?_⟩

Premises used: FirstOrder.Field.finite_ACF_prime_not_realize_of_ACF_zero_realize, Set.infinite_of_finite_compl, Iff.intro, Iff.mp, not_imp_not
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
φ : Language.ring.Sentence
refine : ¬Theory.ACF 0 ⊨ᵇ φ → ¬Set.Infinite (α := Nat.Primes) {p : Nat.Primes | Theory.ACF (↑p : ℕ) ⊨ᵇ φ}
⊢ Theory.ACF 0 ⊨ᵇ φ ↔ Set.Infinite (α := Nat.Primes) {p : Nat.Primes | Theory.ACF (↑p : ℕ) ⊨ᵇ φ}

Tactic:
refine ⟨fun h => Set.infinite_of_finite_compl
      (finite_ACF_prime_not_realize_of_ACF_zero_realize φ h),
    not_imp_not.1 ?_⟩
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
φ : Language.ring.Sentence
⊢ ¬Theory.ACF 0 ⊨ᵇ φ → ¬Set.Infinite (α := Nat.Primes) {p : Nat.Primes | Theory.ACF (↑p : ℕ) ⊨ᵇ φ}

Tactic:
simpa [(ACF_isComplete (Or.inr rfl)).models_not_iff,
      fun p : Nat.Primes => (ACF_isComplete (Or.inl p.2)).models_not_iff] using
    finite_ACF_prime_not_realize_of_ACF_zero_realize φ.not

Premises used: FirstOrder.Field.finite_ACF_prime_not_realize_of_ACF_zero_realize, FirstOrder.Language.Theory.IsComplete.models_not_iff, FirstOrder.Language.Formula.not, Or.inl, Or.inr, rfl, FirstOrder.Field.ACF_isComplete, Subtype.property
-- Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Goal:
φ : Language.ring.Sentence
⊢ Theory.ACF 0 ⊨ᵇ φ ↔ Set.Finite (α := Nat.Primes) {p : Nat.Primes | Theory.ACF (↑p : ℕ) ⊨ᵇ φ}ᶜ

Tactic:
⟨fun h => finite_ACF_prime_not_realize_of_ACF_zero_realize φ h,
    fun h => ACF_zero_realize_iff_infinite_ACF_prime_realize.2
      (Set.infinite_of_finite_compl h)⟩

Premises used: Iff.mpr, FirstOrder.Field.finite_ACF_prime_not_realize_of_ACF_zero_realize, FirstOrder.Field.ACF_zero_realize_iff_infinite_ACF_prime_realize, Set.infinite_of_finite_compl, Iff.intro
-- Module: Mathlib.ModelTheory.Algebra.Ring.Basic
Goal:
α : Type u_2
⊢ Eq.{u_2 + 1} (α := ring.Term α) 0 (Constants.term zeroFunc)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.ModelTheory.Algebra.Ring.Basic
Goal:
α : Type u_2
⊢ Eq.{u_2 + 1} (α := ring.Term α) 1 (Constants.term oneFunc)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.ModelTheory.Algebra.Ring.Basic
Goal:
α : Type u_2
t₁ t₂ : ring.Term α
⊢ t₁ + t₂ = addFunc.apply₂ t₁ t₂

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.ModelTheory.Algebra.Ring.Basic
Goal:
α : Type u_2
t₁ t₂ : ring.Term α
⊢ t₁ * t₂ = mulFunc.apply₂ t₁ t₂

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.ModelTheory.Algebra.Ring.Basic
Goal:
α : Type u_2
t : ring.Term α
⊢ -t = negFunc.apply₁ t

Tactic:
rfl

Premises used: rfl