-- Mathlib/FieldTheory/AxGrothendieck.lean
theorem ACF_models_genericPolyMapSurjOnOfInjOn_of_prime_or_zero
    [Finite ι] {p : ℕ} (hp : p.Prime ∨ p = 0)
    (φ : ring.Formula (α ⊕ ι)) (mons : ι → Finset (ι →₀ ℕ)) :
    Theory.ACF p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons

Proof state:
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : Finite α
inst✝ : Finite ι
p : ℕ
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
hp : Nat.Prime p
⊢ Theory.ACF p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons

Tactic:
exact ACF_models_genericPolyMapSurjOnOfInjOn_of_prime hp φ mons

Result:
no goals

Proof state:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : Finite α
inst✝ : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
⊢ {p | Theory.ACF ↑p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons}.Infinite

Tactic:
convert Set.infinite_univ (α := Nat.Primes)

Result:
case h.e'_2
ι : Type u_1
α : Type u_2
inst✝¹ : Finite α
inst✝ : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
⊢ {p | Theory.ACF ↑p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons} = Set.univ

Proof state:
case h.e'_2
ι : Type u_1
α : Type u_2
inst✝¹ : Finite α
inst✝ : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
⊢ ∀ (x : Nat.Primes), x ∈ {p | Theory.ACF ↑p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons}

Tactic:
intro ⟨p, hp⟩

Result:
case h.e'_2
ι : Type u_1
α : Type u_2
inst✝¹ : Finite α
inst✝ : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
p : ℕ
hp : Nat.Prime p
⊢ ⟨p, hp⟩ ∈ {p | Theory.ACF ↑p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons}

Proof state:
ι : Type u_1
α : Type u_2
inst✝¹ : Finite α
inst✝ : Finite ι
p : ℕ
hp : Nat.Prime p ∨ p = 0
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
⊢ Theory.ACF p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons

Tactic:
rcases hp with hp | rfl

Result:
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : Finite α
inst✝ : Finite ι
p : ℕ
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
hp : Nat.Prime p
⊢ Theory.ACF p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons

case inr
ι : Type u_1
α : Type u_2
inst✝¹ : Finite α
inst✝ : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
⊢ Theory.ACF 0 ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons

Proof state:
case h.e'_2
ι : Type u_1
α : Type u_2
inst✝¹ : Finite α
inst✝ : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
⊢ {p | Theory.ACF ↑p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons} = Set.univ

Tactic:
rw [Set.eq_univ_iff_forall]

Result:
case h.e'_2
ι : Type u_1
α : Type u_2
inst✝¹ : Finite α
inst✝ : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
⊢ ∀ (x : Nat.Primes), x ∈ {p | Theory.ACF ↑p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons}

Proof state:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : Finite α
inst✝ : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
⊢ Theory.ACF 0 ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons

Tactic:
rw [ACF_zero_realize_iff_infinite_ACF_prime_realize]

Result:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : Finite α
inst✝ : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
⊢ {p | Theory.ACF ↑p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons}.Infinite

Proof state:
case h.e'_2
ι : Type u_1
α : Type u_2
inst✝¹ : Finite α
inst✝ : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
p : ℕ
hp : Nat.Prime p
⊢ ⟨p, hp⟩ ∈ {p | Theory.ACF ↑p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons}

Tactic:
exact ACF_models_genericPolyMapSurjOnOfInjOn_of_prime hp φ mons

Result:
no goals