-- Mathlib/FieldTheory/AxGrothendieck.lean
theorem ax_grothendieck_of_definable [CompatibleRing K] {c : Set K}
    (S : Set (ι → K)) (hS : c.Definable Language.ring S)
    (ps : ι → MvPolynomial ι K) :
    S.MapsTo (fun v i => eval v (ps i)) S →
    S.InjOn (fun v i => eval v (ps i)) →
    S.SurjOn (fun v i => eval v (ps i)) S

Proof state:
K : Type u_1
ι : Type u_2
inst✝³ : Field K
inst✝² : IsAlgClosed K
inst✝¹ : Finite ι
inst✝ : CompatibleRing K
c : Set K
S : Set (ι → K)
hS : c.Definable ring S
ps : ι → MvPolynomial ι K
this : Fintype ι := Fintype.ofFinite ι
⊢ Set.MapsTo (fun v i => (eval v) (ps i)) S S →
    Set.InjOn (fun v i => (eval v) (ps i)) S → Set.SurjOn (fun v i => (eval v) (ps i)) S S

Tactic:
let p : ℕ := ringChar K

Result:
K : Type u_1
ι : Type u_2
inst✝³ : Field K
inst✝² : IsAlgClosed K
inst✝¹ : Finite ι
inst✝ : CompatibleRing K
c : Set K
S : Set (ι → K)
hS : c.Definable ring S
ps : ι → MvPolynomial ι K
this : Fintype ι := Fintype.ofFinite ι
p : ℕ := ringChar K
⊢ Set.MapsTo (fun v i => (eval v) (ps i)) S S →
    Set.InjOn (fun v i => (eval v) (ps i)) S → Set.SurjOn (fun v i => (eval v) (ps i)) S S

Proof state:
case intro.intro.intro
K : Type u_1
ι : Type u_2
inst✝³ : Field K
inst✝² : IsAlgClosed K
inst✝¹ : Finite ι
inst✝ : CompatibleRing K
c✝ : Set K
S : Set (ι → K)
ps : ι → MvPolynomial ι K
this✝ : Fintype ι := Fintype.ofFinite ι
p : ℕ := ringChar K
this : CharP K p
c : Finset K
left✝ : ↑c ⊆ c✝
φ : ring.Formula (↑↑c ⊕ ι)
hφ : S = {v | φ.Realize (Sum.elim Subtype.val v)}
⊢ Set.MapsTo (fun v i => (eval v) (ps i)) S S →
    Set.InjOn (fun v i => (eval v) (ps i)) S → Set.SurjOn (fun v i => (eval v) (ps i)) S S

Tactic:
rw [hφ]

Result:
case intro.intro.intro
K : Type u_1
ι : Type u_2
inst✝³ : Field K
inst✝² : IsAlgClosed K
inst✝¹ : Finite ι
inst✝ : CompatibleRing K
c✝ : Set K
S : Set (ι → K)
ps : ι → MvPolynomial ι K
this✝ : Fintype ι := Fintype.ofFinite ι
p : ℕ := ringChar K
this : CharP K p
c : Finset K
left✝ : ↑c ⊆ c✝
φ : ring.Formula (↑↑c ⊕ ι)
hφ : S = {v | φ.Realize (Sum.elim Subtype.val v)}
⊢ Set.MapsTo (fun v i => (eval v) (ps i)) {v | φ.Realize (Sum.elim Subtype.val v)}
      {v | φ.Realize (Sum.elim Subtype.val v)} →
    Set.InjOn (fun v i => (eval v) (ps i)) {v | φ.Realize (Sum.elim Subtype.val v)} →
      Set.SurjOn (fun v i => (eval v) (ps i)) {v | φ.Realize (Sum.elim Subtype.val v)}
        {v | φ.Realize (Sum.elim Subtype.val v)}

Proof state:
K : Type u_1
ι : Type u_2
inst✝³ : Field K
inst✝² : IsAlgClosed K
inst✝¹ : Finite ι
inst✝ : CompatibleRing K
c : Set K
S : Set (ι → K)
hS : c.Definable ring S
ps : ι → MvPolynomial ι K
this✝ : Fintype ι := Fintype.ofFinite ι
p : ℕ := ringChar K
this : CharP K p
⊢ Set.MapsTo (fun v i => (eval v) (ps i)) S S →
    Set.InjOn (fun v i => (eval v) (ps i)) S → Set.SurjOn (fun v i => (eval v) (ps i)) S S

Tactic:
rw [Set.definable_iff_finitely_definable] at hS

Result:
K : Type u_1
ι : Type u_2
inst✝³ : Field K
inst✝² : IsAlgClosed K
inst✝¹ : Finite ι
inst✝ : CompatibleRing K
c : Set K
S : Set (ι → K)
hS : ∃ A0, ↑A0 ⊆ c ∧ (↑A0).Definable ring S
ps : ι → MvPolynomial ι K
this✝ : Fintype ι := Fintype.ofFinite ι
p : ℕ := ringChar K
this : CharP K p
⊢ Set.MapsTo (fun v i => (eval v) (ps i)) S S →
    Set.InjOn (fun v i => (eval v) (ps i)) S → Set.SurjOn (fun v i => (eval v) (ps i)) S S

Proof state:
case intro.intro.intro
K : Type u_1
ι : Type u_2
inst✝³ : Field K
inst✝² : IsAlgClosed K
inst✝¹ : Finite ι
inst✝ : CompatibleRing K
c✝ : Set K
S : Set (ι → K)
ps : ι → MvPolynomial ι K
this✝¹ : Fintype ι := Fintype.ofFinite ι
p : ℕ := ringChar K
this✝ : CharP K p
c : Finset K
left✝ : ↑c ⊆ c✝
φ : ring.Formula (↑↑c ⊕ ι)
hφ : S = {v | φ.Realize (Sum.elim Subtype.val v)}
this :
  ∀ (v : ↑↑c → K) (p : { p // ∀ (i : ι), (p i).support ⊆ (ps i).support }),
    let f := fun v i => (eval v) (↑p i);
    let S := fun x => φ.Realize (Sum.elim v x);
    Set.MapsTo f S S → Set.InjOn f S → Set.SurjOn f S S
⊢ Set.MapsTo (fun v i => (eval v) (ps i)) {v | φ.Realize (Sum.elim Subtype.val v)}
      {v | φ.Realize (Sum.elim Subtype.val v)} →
    Set.InjOn (fun v i => (eval v) (ps i)) {v | φ.Realize (Sum.elim Subtype.val v)} →
      Set.SurjOn (fun v i => (eval v) (ps i)) {v | φ.Realize (Sum.elim Subtype.val v)}
        {v | φ.Realize (Sum.elim Subtype.val v)}

Tactic:
exact this Subtype.val ⟨ps, fun i => Set.Subset.refl _⟩

Result:
no goals

Proof state:
case intro.intro.intro
K : Type u_1
ι : Type u_2
inst✝³ : Field K
inst✝² : IsAlgClosed K
inst✝¹ : Finite ι
inst✝ : CompatibleRing K
c✝ : Set K
S : Set (ι → K)
ps : ι → MvPolynomial ι K
this✝ : Fintype ι := Fintype.ofFinite ι
p : ℕ := ringChar K
this : CharP K p
c : Finset K
left✝ : ↑c ⊆ c✝
φ : ring.Formula (↑↑c ⊕ ι)
hφ : S = {v | φ.Realize (Sum.elim Subtype.val v)}
⊢ Set.MapsTo (fun v i => (eval v) (ps i)) {v | φ.Realize (Sum.elim Subtype.val v)}
      {v | φ.Realize (Sum.elim Subtype.val v)} →
    Set.InjOn (fun v i => (eval v) (ps i)) {v | φ.Realize (Sum.elim Subtype.val v)} →
      Set.SurjOn (fun v i => (eval v) (ps i)) {v | φ.Realize (Sum.elim Subtype.val v)}
        {v | φ.Realize (Sum.elim Subtype.val v)}

Tactic:
have := ACF_models_genericPolyMapSurjOnOfInjOn_of_prime_or_zero
  (CharP.char_is_prime_or_zero K p) φ (fun i => (ps i).support)

Result:
case intro.intro.intro
K : Type u_1
ι : Type u_2
inst✝³ : Field K
inst✝² : IsAlgClosed K
inst✝¹ : Finite ι
inst✝ : CompatibleRing K
c✝ : Set K
S : Set (ι → K)
ps : ι → MvPolynomial ι K
this✝¹ : Fintype ι := Fintype.ofFinite ι
p : ℕ := ringChar K
this✝ : CharP K p
c : Finset K
left✝ : ↑c ⊆ c✝
φ : ring.Formula (↑↑c ⊕ ι)
hφ : S = {v | φ.Realize (Sum.elim Subtype.val v)}
this : Theory.ACF p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ fun i => (ps i).support
⊢ Set.MapsTo (fun v i => (eval v) (ps i)) {v | φ.Realize (Sum.elim Subtype.val v)}
      {v | φ.Realize (Sum.elim Subtype.val v)} →
    Set.InjOn (fun v i => (eval v) (ps i)) {v | φ.Realize (Sum.elim Subtype.val v)} →
      Set.SurjOn (fun v i => (eval v) (ps i)) {v | φ.Realize (Sum.elim Subtype.val v)}
        {v | φ.Realize (Sum.elim Subtype.val v)}

Proof state:
K : Type u_1
ι : Type u_2
inst✝³ : Field K
inst✝² : IsAlgClosed K
inst✝¹ : Finite ι
inst✝ : CompatibleRing K
c : Set K
S : Set (ι → K)
hS : ∃ A0, ↑A0 ⊆ c ∧ (↑A0).Definable ring S
ps : ι → MvPolynomial ι K
this✝ : Fintype ι := Fintype.ofFinite ι
p : ℕ := ringChar K
this : CharP K p
⊢ Set.MapsTo (fun v i => (eval v) (ps i)) S S →
    Set.InjOn (fun v i => (eval v) (ps i)) S → Set.SurjOn (fun v i => (eval v) (ps i)) S S

Tactic:
rcases hS with ⟨c, _, hS⟩

Result:
case intro.intro
K : Type u_1
ι : Type u_2
inst✝³ : Field K
inst✝² : IsAlgClosed K
inst✝¹ : Finite ι
inst✝ : CompatibleRing K
c✝ : Set K
S : Set (ι → K)
ps : ι → MvPolynomial ι K
this✝ : Fintype ι := Fintype.ofFinite ι
p : ℕ := ringChar K
this : CharP K p
c : Finset K
left✝ : ↑c ⊆ c✝
hS : (↑c).Definable ring S
⊢ Set.MapsTo (fun v i => (eval v) (ps i)) S S →
    Set.InjOn (fun v i => (eval v) (ps i)) S → Set.SurjOn (fun v i => (eval v) (ps i)) S S

Proof state:
K : Type u_1
ι : Type u_2
inst✝³ : Field K
inst✝² : IsAlgClosed K
inst✝¹ : Finite ι
inst✝ : CompatibleRing K
c : Set K
S : Set (ι → K)
hS : c.Definable ring S
ps : ι → MvPolynomial ι K
this : Fintype ι := Fintype.ofFinite ι
p : ℕ := ringChar K
⊢ Set.MapsTo (fun v i => (eval v) (ps i)) S S →
    Set.InjOn (fun v i => (eval v) (ps i)) S → Set.SurjOn (fun v i => (eval v) (ps i)) S S

Tactic:
have : CharP K p := ⟨ringChar.spec K⟩

Result:
K : Type u_1
ι : Type u_2
inst✝³ : Field K
inst✝² : IsAlgClosed K
inst✝¹ : Finite ι
inst✝ : CompatibleRing K
c : Set K
S : Set (ι → K)
hS : c.Definable ring S
ps : ι → MvPolynomial ι K
this✝ : Fintype ι := Fintype.ofFinite ι
p : ℕ := ringChar K
this : CharP K p
⊢ Set.MapsTo (fun v i => (eval v) (ps i)) S S →
    Set.InjOn (fun v i => (eval v) (ps i)) S → Set.SurjOn (fun v i => (eval v) (ps i)) S S