-- 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:
φ : 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 ⊨ᵇ ψ }

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

Result:
φ : 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 ⊨ᵇ ψ }

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

Tactic:
intro p hp

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 : Nat.Primes
hp : p ∈ (↑s)ᶜ
⊢ p ∈ 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}
q : Nat.Primes
a✝ : 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)

Result:
no goals

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}
⊢ ∀ q ∉ {⟨p, hp⟩}, Theory.ACF ↑q ⊨ᵇ ∼(eqZero p)

Tactic:
rintro ⟨q, _⟩ hq ⟨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)
⊢ (∼(eqZero p)).Realize v✝ xs✝

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

Tactic:
rw [Theory.models_iff_finset_models] at h

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

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

Tactic:
have := charP_of_model_fieldOfChar 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
x✝ : CompatibleRing K := compatibleRingOfModelField K
this : CharP K q
⊢ (∼(eqZero p)).Realize v✝ xs✝

Proof state:
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 ⊨ᵇ ψ }

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

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}
⊢ Nonempty { s // ∀ q ∉ s, Theory.ACF ↑q ⊨ᵇ ψ }

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

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

Tactic:
have hqp : q ≠ p := by simpa [← Nat.Primes.coe_nat_inj] using hq

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

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

Tactic:
let s : Finset Nat.Primes := T0.attach.biUnion (fun φ => f φ.1 (hT0 φ.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 ↑φ ⋯)
⊢ {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.ACF ↑q

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

Result:
φ : 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 {⊥}