-- 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.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
⊢ (∼(eqZero p)).Realize v✝ xs✝

Tactic:
let _ := fieldOfModelACF q 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
⊢ (∼(eqZero p)).Realize v✝ xs✝

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} ∨ ∃ x ∈ {q | Nat.Prime q}, ∼(eqZero x) = ψ
⊢ { s // ∀ q ∉ s, Theory.ACF ↑q ⊨ᵇ ψ }

Tactic:
apply Classical.choice

Result:
case a
φ : 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} ∨ ∃ x ∈ {q | Nat.Prime q}, ∼(eqZero x) = ψ
⊢ Nonempty { s // ∀ q ∉ s, Theory.ACF ↑q ⊨ᵇ ψ }

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 : Nat.Primes
hp : p ∈ (↑s)ᶜ
⊢ p ∈ fun p => ∀ (M : (Theory.ACF ↑p).ModelType) (v : Empty → ↑M) (xs : Fin 0 → ↑M), BoundedFormula.Realize φ v xs

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

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
ψ : Language.ring.Sentence
hψ : ψ ∈ T0
hpψ : ∀ (x : Language.ring.Sentence) (x_1 : x ∈ T0), p ∉ ↑(f x ⋯)
⊢ Theory.ACF ↑p ⊨ᵇ ψ

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

Result:
no goals

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
⊢ (∼(eqZero p)).Realize v✝ xs✝

Tactic:
have := modelField_of_modelACF q 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
⊢ (∼(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
⊢ (∼(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]

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
⊢ ¬CharP K 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 ↑φ ⋯)
⊢ {p | ¬Theory.ACF ↑p ⊨ᵇ φ}.Finite

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ψ)

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 ⊨ᵇ ψ
⊢ {p | ¬Theory.ACF ↑p ⊨ᵇ φ}.Finite

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
ψ : Language.ring.Sentence
hψ : ψ ∈ T0
hpψ : p ∉ s
⊢ Theory.ACF ↑p ⊨ᵇ ψ

Tactic:
simp only [s, Finset.mem_biUnion, Finset.mem_attach, true_and,
  Subtype.exists, not_exists] at 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ψ : ∀ (x : Language.ring.Sentence) (x_1 : x ∈ T0), p ∉ ↑(f x ⋯)
⊢ Theory.ACF ↑p ⊨ᵇ ψ

Proof state:
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h : ↑T0 ⊨ᵇ φ
⊢ (ψ : Language.ring.Sentence) → ψ ∈ Theory.ACF 0 → { s // ∀ q ∉ s, Theory.ACF ↑q ⊨ᵇ ψ }

Tactic:
intro ψ hψ

Result:
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h : ↑T0 ⊨ᵇ φ
ψ : Language.ring.Sentence
hψ : ψ ∈ Theory.ACF 0
⊢ { s // ∀ q ∉ s, Theory.ACF ↑q ⊨ᵇ ψ }