-- Mathlib/ModelTheory/Algebra/Field/IsAlgClosed.lean
theorem finite_ACF_prime_not_realize_of_ACF_zero_realize
    (φ : Language.ring.Sentence) (h : Theory.ACF 0 ⊨ᵇ φ) :
    Set.Finite { p : Nat.Primes | ¬ Theory.ACF p ⊨ᵇ φ }

Proof state:
case a.inl
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h✝ : ↑T0 ⊨ᵇ φ
ψ : Language.ring.Sentence
h : ψ ∈ Theory.field ∪ genericMonicPolyHasRoot '' {n | 0 < n}
⊢ ∀ q ∉ ∅, Theory.ACF ↑q ⊨ᵇ ψ

Tactic:
intro q _

Result:
case a.inl
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h✝ : ↑T0 ⊨ᵇ φ
ψ : Language.ring.Sentence
h : ψ ∈ Theory.field ∪ genericMonicPolyHasRoot '' {n | 0 < n}
q : Nat.Primes
a✝ : q ∉ ∅
⊢ Theory.ACF ↑q ⊨ᵇ ψ

Proof state:
case a.inr.intro.intro.mk.mk
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h : ↑T0 ⊨ᵇ φ
p : ℕ
hp : p ∈ {q | Nat.Prime q}
q : ℕ
property✝ : Nat.Prime q
hq : ⟨q, property✝⟩ ∉ {⟨p, hp⟩}
K : Type
struc✝ : Language.ring.Structure K
is_model✝ : K ⊨ Theory.ACF ↑⟨q, property✝⟩
nonempty'✝ : Nonempty K
v✝ : Empty → ↑(Theory.ModelType.mk K)
xs✝ : Fin 0 → ↑(Theory.ModelType.mk K)
hqp : q ≠ p
x✝¹ : Field K := fieldOfModelACF q K
this✝ : K ⊨ Theory.field
x✝ : CompatibleRing K := compatibleRingOfModelField K
this : CharP K q
⊢ ¬CharP K p

Tactic:
intro _

Result:
case a.inr.intro.intro.mk.mk
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h : ↑T0 ⊨ᵇ φ
p : ℕ
hp : p ∈ {q | Nat.Prime q}
q : ℕ
property✝ : Nat.Prime q
hq : ⟨q, property✝⟩ ∉ {⟨p, hp⟩}
K : Type
struc✝ : Language.ring.Structure K
is_model✝ : K ⊨ Theory.ACF ↑⟨q, property✝⟩
nonempty'✝ : Nonempty K
v✝ : Empty → ↑(Theory.ModelType.mk K)
xs✝ : Fin 0 → ↑(Theory.ModelType.mk K)
hqp : q ≠ p
x✝¹ : Field K := fieldOfModelACF q K
this✝ : K ⊨ Theory.field
x✝ : CompatibleRing K := compatibleRingOfModelField K
this : CharP K q
a✝ : CharP K p
⊢ False

Proof state:
case a.inr.intro.intro
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h : ↑T0 ⊨ᵇ φ
p : ℕ
hp : p ∈ {q | Nat.Prime q}
⊢ Nonempty { s // ∀ q ∉ s, Theory.ACF ↑q ⊨ᵇ ∼(eqZero p) }

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

Result:
case a.inr.intro.intro
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h : ↑T0 ⊨ᵇ φ
p : ℕ
hp : p ∈ {q | Nat.Prime q}
⊢ ∀ q ∉ {⟨p, hp⟩}, Theory.ACF ↑q ⊨ᵇ ∼(eqZero p)

Proof state:
case a.inr.intro.intro.mk.mk
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h : ↑T0 ⊨ᵇ φ
p : ℕ
hp : p ∈ {q | Nat.Prime q}
q : ℕ
property✝ : Nat.Prime q
hq : ⟨q, property✝⟩ ∉ {⟨p, hp⟩}
K : Type
struc✝ : Language.ring.Structure K
is_model✝ : K ⊨ Theory.ACF ↑⟨q, property✝⟩
nonempty'✝ : Nonempty K
v✝ : Empty → ↑(Theory.ModelType.mk K)
xs✝ : Fin 0 → ↑(Theory.ModelType.mk K)
hqp : q ≠ p
x✝ : Field K := fieldOfModelACF q K
this : K ⊨ Theory.field
⊢ (∼(eqZero p)).Realize v✝ xs✝

Tactic:
let _ := compatibleRingOfModelField K

Result:
case a.inr.intro.intro.mk.mk
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h : ↑T0 ⊨ᵇ φ
p : ℕ
hp : p ∈ {q | Nat.Prime q}
q : ℕ
property✝ : Nat.Prime q
hq : ⟨q, property✝⟩ ∉ {⟨p, hp⟩}
K : Type
struc✝ : Language.ring.Structure K
is_model✝ : K ⊨ Theory.ACF ↑⟨q, property✝⟩
nonempty'✝ : Nonempty K
v✝ : Empty → ↑(Theory.ModelType.mk K)
xs✝ : Fin 0 → ↑(Theory.ModelType.mk K)
hqp : q ≠ p
x✝¹ : Field K := fieldOfModelACF q K
this : K ⊨ Theory.field
x✝ : CompatibleRing K := compatibleRingOfModelField K
⊢ (∼(eqZero p)).Realize v✝ xs✝

Proof state:
case a.inr.intro.intro.mk.mk
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h : ↑T0 ⊨ᵇ φ
p : ℕ
hp : p ∈ {q | Nat.Prime q}
q : ℕ
property✝ : Nat.Prime q
hq : ⟨q, property✝⟩ ∉ {⟨p, hp⟩}
K : Type
struc✝ : Language.ring.Structure K
is_model✝ : K ⊨ Theory.ACF ↑⟨q, property✝⟩
nonempty'✝ : Nonempty K
v✝ : Empty → ↑(Theory.ModelType.mk K)
xs✝ : Fin 0 → ↑(Theory.ModelType.mk K)
hqp : q ≠ p
x✝¹ : Field K := fieldOfModelACF q K
this✝ : K ⊨ Theory.field
x✝ : CompatibleRing K := compatibleRingOfModelField K
this : CharP K q
a✝ : CharP K p
⊢ False

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

Result:
no goals

Proof state:
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h : ↑T0 ⊨ᵇ φ
p : ℕ
hp : p ∈ {q | Nat.Prime q}
q : ℕ
property✝ : Nat.Prime q
hq : ⟨q, property✝⟩ ∉ {⟨p, hp⟩}
K : Type
struc✝ : Language.ring.Structure K
is_model✝ : K ⊨ Theory.ACF ↑⟨q, property✝⟩
nonempty'✝ : Nonempty K
v✝ : Empty → ↑(Theory.ModelType.mk K)
xs✝ : Fin 0 → ↑(Theory.ModelType.mk K)
⊢ q ≠ p

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

Result:
no goals

Proof state:
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h : ↑T0 ⊨ᵇ φ
f : (ψ : Language.ring.Sentence) → ψ ∈ Theory.ACF 0 → { s // ∀ q ∉ s, Theory.ACF ↑q ⊨ᵇ ψ }
s : Finset Nat.Primes := T0.attach.biUnion fun φ => ↑(f ↑φ ⋯)
⊢ ∀ (p : Nat.Primes), ∀ ψ ∈ T0, p ∉ s → Theory.ACF ↑p ⊨ᵇ ψ

Tactic:
intro p ψ hψ hpψ

Result:
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h : ↑T0 ⊨ᵇ φ
f : (ψ : Language.ring.Sentence) → ψ ∈ Theory.ACF 0 → { s // ∀ q ∉ s, Theory.ACF ↑q ⊨ᵇ ψ }
s : Finset Nat.Primes := T0.attach.biUnion fun φ => ↑(f ↑φ ⋯)
p : Nat.Primes
ψ : Language.ring.Sentence
hψ : ψ ∈ T0
hpψ : p ∉ s
⊢ Theory.ACF ↑p ⊨ᵇ ψ

Proof state:
case intro.intro
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h : ↑T0 ⊨ᵇ φ
f : (ψ : Language.ring.Sentence) → ψ ∈ Theory.ACF 0 → { s // ∀ q ∉ s, Theory.ACF ↑q ⊨ᵇ ψ }
s : Finset Nat.Primes := T0.attach.biUnion fun φ => ↑(f ↑φ ⋯)
hs : ∀ (p : Nat.Primes), ∀ ψ ∈ T0, p ∉ s → Theory.ACF ↑p ⊨ᵇ ψ
⊢ {p | ¬Theory.ACF ↑p ⊨ᵇ φ}.Finite

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

Result:
case intro.intro
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h : ↑T0 ⊨ᵇ φ
f : (ψ : Language.ring.Sentence) → ψ ∈ Theory.ACF 0 → { s // ∀ q ∉ s, Theory.ACF ↑q ⊨ᵇ ψ }
s : Finset Nat.Primes := T0.attach.biUnion fun φ => ↑(f ↑φ ⋯)
hs : ∀ (p : Nat.Primes), ∀ ψ ∈ T0, p ∉ s → Theory.ACF ↑p ⊨ᵇ ψ
⊢ (↑s)ᶜ ⊆ fun p => ∀ (M : (Theory.ACF ↑p).ModelType) (v : Empty → ↑M) (xs : Fin 0 → ↑M), BoundedFormula.Realize φ v xs

Proof state:
case a.inl
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h✝ : ↑T0 ⊨ᵇ φ
ψ : Language.ring.Sentence
h : ψ ∈ Theory.field ∪ genericMonicPolyHasRoot '' {n | 0 < n}
⊢ Nonempty { s // ∀ q ∉ s, Theory.ACF ↑q ⊨ᵇ ψ }

Tactic:
refine ⟨⟨∅, ?_⟩⟩

Result:
case a.inl
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h✝ : ↑T0 ⊨ᵇ φ
ψ : Language.ring.Sentence
h : ψ ∈ Theory.field ∪ genericMonicPolyHasRoot '' {n | 0 < n}
⊢ ∀ q ∉ ∅, Theory.ACF ↑q ⊨ᵇ ψ

Proof state:
φ : Language.ring.Sentence
h : ∃ T0, ↑T0 ⊆ Theory.ACF 0 ∧ ↑T0 ⊨ᵇ φ
⊢ {p | ¬Theory.ACF ↑p ⊨ᵇ φ}.Finite

Tactic:
rcases h with ⟨T0, hT0, h⟩

Result:
case intro.intro
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h : ↑T0 ⊨ᵇ φ
⊢ {p | ¬Theory.ACF ↑p ⊨ᵇ φ}.Finite

Proof state:
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h✝ : ↑T0 ⊨ᵇ φ
ψ : Language.ring.Sentence
h : ψ ∈ Theory.field ∪ genericMonicPolyHasRoot '' {n | 0 < n}
q : Nat.Primes
a✝ : 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

Result:
no goals