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

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

Tactic:
have : CharP (AlgebraicClosure (ZMod p)) p :=
  charP_of_injective_algebraMap
    (RingHom.injective (algebraMap (ZMod p) (AlgebraicClosure (ZMod p)))) p

Result:
ι : Type u_1
α : Type u_2
inst✝¹ : Finite α
inst✝ : Finite ι
p : ℕ
hp : Nat.Prime p
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
this✝¹ : Fact (Nat.Prime p)
this✝ : CompatibleRing (AlgebraicClosure (ZMod p)) := compatibleRingOfRing (AlgebraicClosure (ZMod p))
this : CharP (AlgebraicClosure (ZMod p)) p
⊢ Theory.ACF p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons

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

Tactic:
letI := compatibleRingOfRing (AlgebraicClosure (ZMod p))

Result:
ι : Type u_1
α : Type u_2
inst✝¹ : Finite α
inst✝ : Finite ι
p : ℕ
hp : Nat.Prime p
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
this✝ : Fact (Nat.Prime p)
this : CompatibleRing (AlgebraicClosure (ZMod p)) := compatibleRingOfRing (AlgebraicClosure (ZMod p))
⊢ Theory.ACF p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons

Proof state:
case mk
ι : Type u_1
α : Type u_2
inst✝¹ : Finite α
inst✝ : Finite ι
p : ℕ
hp : Nat.Prime p
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
this✝¹ : Fact (Nat.Prime p)
this✝ : CompatibleRing (AlgebraicClosure (ZMod p)) := compatibleRingOfRing (AlgebraicClosure (ZMod p))
this : CharP (AlgebraicClosure (ZMod p)) p
v : α → AlgebraicClosure (ZMod p)
f : ι → MvPolynomial ι (AlgebraicClosure (ZMod p))
property✝ : ∀ (i : ι), (f i).support ⊆ mons i
⊢ let f := fun v i => (eval v) (↑⟨f, property✝⟩ i);
  let S := fun x => φ.Realize (Sum.elim v x);
  Set.MapsTo f S S → Set.InjOn f S → Set.SurjOn f S S

Tactic:
exact ax_grothendieck_of_locally_finite (K := ZMod p) (ι := ι) f _

Result:
no goals

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

Tactic:
have : Fact p.Prime := ⟨hp⟩

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

Proof state:
ι : Type u_1
α : Type u_2
inst✝¹ : Finite α
inst✝ : Finite ι
p : ℕ
hp : Nat.Prime p
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
this✝¹ : Fact (Nat.Prime p)
this✝ : CompatibleRing (AlgebraicClosure (ZMod p)) := compatibleRingOfRing (AlgebraicClosure (ZMod p))
this : CharP (AlgebraicClosure (ZMod p)) p
⊢ Theory.ACF p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons

Tactic:
rw [← (ACF_isComplete (Or.inl hp)).realize_sentence_iff _
  (AlgebraicClosure (ZMod p)), realize_genericPolyMapSurjOnOfInjOn]

Result:
ι : Type u_1
α : Type u_2
inst✝¹ : Finite α
inst✝ : Finite ι
p : ℕ
hp : Nat.Prime p
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
this✝¹ : Fact (Nat.Prime p)
this✝ : CompatibleRing (AlgebraicClosure (ZMod p)) := compatibleRingOfRing (AlgebraicClosure (ZMod p))
this : CharP (AlgebraicClosure (ZMod p)) p
⊢ ∀ (v : α → AlgebraicClosure (ZMod p)) (p_1 : { p_1 // ∀ (i : ι), (p_1 i).support ⊆ mons i }),
    let f := fun v i => (eval v) (↑p_1 i);
    let S := fun x => φ.Realize (Sum.elim v x);
    Set.MapsTo f S S → Set.InjOn f S → Set.SurjOn f S S

Proof state:
ι : Type u_1
α : Type u_2
inst✝¹ : Finite α
inst✝ : Finite ι
p : ℕ
hp : Nat.Prime p
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
this✝¹ : Fact (Nat.Prime p)
this✝ : CompatibleRing (AlgebraicClosure (ZMod p)) := compatibleRingOfRing (AlgebraicClosure (ZMod p))
this : CharP (AlgebraicClosure (ZMod p)) p
⊢ ∀ (v : α → AlgebraicClosure (ZMod p)) (p_1 : { p_1 // ∀ (i : ι), (p_1 i).support ⊆ mons i }),
    let f := fun v i => (eval v) (↑p_1 i);
    let S := fun x => φ.Realize (Sum.elim v x);
    Set.MapsTo f S S → Set.InjOn f S → Set.SurjOn f S S

Tactic:
rintro v ⟨f, _⟩

Result:
case mk
ι : Type u_1
α : Type u_2
inst✝¹ : Finite α
inst✝ : Finite ι
p : ℕ
hp : Nat.Prime p
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
this✝¹ : Fact (Nat.Prime p)
this✝ : CompatibleRing (AlgebraicClosure (ZMod p)) := compatibleRingOfRing (AlgebraicClosure (ZMod p))
this : CharP (AlgebraicClosure (ZMod p)) p
v : α → AlgebraicClosure (ZMod p)
f : ι → MvPolynomial ι (AlgebraicClosure (ZMod p))
property✝ : ∀ (i : ι), (f i).support ⊆ mons i
⊢ let f := fun v i => (eval v) (↑⟨f, property✝⟩ i);
  let S := fun x => φ.Realize (Sum.elim v x);
  Set.MapsTo f S S → Set.InjOn f S → Set.SurjOn f S S

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

Tactic:
classical
have : Fact p.Prime := ⟨hp⟩
letI := compatibleRingOfRing (AlgebraicClosure (ZMod p))
have : CharP (AlgebraicClosure (ZMod p)) p :=
  charP_of_injective_algebraMap
    (RingHom.injective (algebraMap (ZMod p) (AlgebraicClosure (ZMod p)))) p
rw [← (ACF_isComplete (Or.inl hp)).realize_sentence_iff _
  (AlgebraicClosure (ZMod p)), realize_genericPolyMapSurjOnOfInjOn]
rintro v ⟨f, _⟩
exact ax_grothendieck_of_locally_finite (K := ZMod p) (ι := ι) f _

Result:
no goals