-- Mathlib/FieldTheory/AxGrothendieck.lean
theorem ax_grothendieck_of_locally_finite {ι K R : Type*} [Field K] [Finite K] [CommRing R]
    [Finite ι] [Algebra K R] [alg : Algebra.IsAlgebraic K R] (ps : ι → MvPolynomial ι R)
    (S : Set (ι → R))
    (hm : S.MapsTo (fun v i => eval v (ps i)) S)
    (hinj : S.InjOn (fun v i => eval v (ps i))) :
    S.SurjOn (fun v i => eval v (ps i)) S

Proof state:
case intro
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
S : Set (ι → R)
hm : Set.MapsTo (fun v i => (eval v) (ps i)) S S
hinj : Set.InjOn (fun v i => (eval v) (ps i)) S
is_int : ∀ (x : R), IsIntegral K x
v : ι → R
hvS : v ∈ S
val✝ : Fintype ι
⊢ v ∈ (fun v i => (eval v) (ps i)) '' S

Tactic:
let s : Finset R :=
  (Finset.biUnion (univ : Finset ι) fun i => (ps i).support.image fun x => coeff x (ps i)) ∪
    (univ : Finset ι).image v

Result:
case intro
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
S : Set (ι → R)
hm : Set.MapsTo (fun v i => (eval v) (ps i)) S S
hinj : Set.InjOn (fun v i => (eval v) (ps i)) S
is_int : ∀ (x : R), IsIntegral K x
v : ι → R
hvS : v ∈ S
val✝ : Fintype ι
s : Finset R := (univ.biUnion fun i => image (fun x => coeff x (ps i)) (ps i).support) ∪ image v univ
⊢ v ∈ (fun v i => (eval v) (ps i)) '' S

Proof state:
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
S : Set (ι → R)
hm : Set.MapsTo (fun v i => (eval v) (ps i)) S S
hinj : Set.InjOn (fun v i => (eval v) (ps i)) S
is_int : ∀ (x : R), IsIntegral K x
v : ι → R
hvS : v ∈ S
val✝ : Fintype ι
s : Finset R := (univ.biUnion fun i => image (fun x => coeff x (ps i)) (ps i).support) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι), ∀ k ∈ (ps i).support, coeff k (ps i) ∈ Algebra.adjoin K ↑s
this✝¹ : IsNoetherian K ↥(Algebra.adjoin K ↑s)
this✝ : Module.Finite K ↥(Algebra.adjoin K ↑s)
this : Finite ↥(Algebra.adjoin K ↑s)
S' : Set (ι → ↥(Algebra.adjoin K ↑s)) := (fun v => Subtype.val ∘ v) ⁻¹' S
res : ↑S' → ↑S' := fun x => ⟨fun i => ⟨(eval fun j => ↑(↑x j)) (ps i), ⋯⟩, ⋯⟩
x y : ↑S'
hxy : res x = res y
⊢ x = y

Tactic:
ext i

Result:
case a.h.a
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
S : Set (ι → R)
hm : Set.MapsTo (fun v i => (eval v) (ps i)) S S
hinj : Set.InjOn (fun v i => (eval v) (ps i)) S
is_int : ∀ (x : R), IsIntegral K x
v : ι → R
hvS : v ∈ S
val✝ : Fintype ι
s : Finset R := (univ.biUnion fun i => image (fun x => coeff x (ps i)) (ps i).support) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι), ∀ k ∈ (ps i).support, coeff k (ps i) ∈ Algebra.adjoin K ↑s
this✝¹ : IsNoetherian K ↥(Algebra.adjoin K ↑s)
this✝ : Module.Finite K ↥(Algebra.adjoin K ↑s)
this : Finite ↥(Algebra.adjoin K ↑s)
S' : Set (ι → ↥(Algebra.adjoin K ↑s)) := (fun v => Subtype.val ∘ v) ⁻¹' S
res : ↑S' → ↑S' := fun x => ⟨fun i => ⟨(eval fun j => ↑(↑x j)) (ps i), ⋯⟩, ⋯⟩
x y : ↑S'
hxy : res x = res y
i : ι
⊢ ↑(↑x i) = ↑(↑y i)

Proof state:
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
S : Set (ι → R)
hm : Set.MapsTo (fun v i => (eval v) (ps i)) S S
hinj : Set.InjOn (fun v i => (eval v) (ps i)) S
⊢ Set.SurjOn (fun v i => (eval v) (ps i)) S S

Tactic:
have is_int : ∀ x : R, IsIntegral K x := fun x => isAlgebraic_iff_isIntegral.1
  (alg.isAlgebraic x)

Result:
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
S : Set (ι → R)
hm : Set.MapsTo (fun v i => (eval v) (ps i)) S S
hinj : Set.InjOn (fun v i => (eval v) (ps i)) S
is_int : ∀ (x : R), IsIntegral K x
⊢ Set.SurjOn (fun v i => (eval v) (ps i)) S S

Proof state:
case intro
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
S : Set (ι → R)
hm : Set.MapsTo (fun v i => (eval v) (ps i)) S S
hinj : Set.InjOn (fun v i => (eval v) (ps i)) S
is_int : ∀ (x : R), IsIntegral K x
v : ι → R
hvS : v ∈ S
val✝ : Fintype ι
s : Finset R := (univ.biUnion fun i => image (fun x => coeff x (ps i)) (ps i).support) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι), ∀ k ∈ (ps i).support, coeff k (ps i) ∈ Algebra.adjoin K ↑s
this✝¹ : IsNoetherian K ↥(Algebra.adjoin K ↑s)
this✝ : Module.Finite K ↥(Algebra.adjoin K ↑s)
this : Finite ↥(Algebra.adjoin K ↑s)
S' : Set (ι → ↥(Algebra.adjoin K ↑s)) := (fun v => Subtype.val ∘ v) ⁻¹' S
res : ↑S' → ↑S' := fun x => ⟨fun i => ⟨(eval fun j => ↑(↑x j)) (ps i), ⋯⟩, ⋯⟩
⊢ v ∈ (fun v i => (eval v) (ps i)) '' S

Tactic:
have hres_surj : Function.Surjective res := by
  rw [← Finite.injective_iff_surjective]
  intro x y hxy
  ext i
  simp only [Subtype.ext_iff, funext_iff] at hxy
  exact congr_fun (hinj x.2 y.2 (funext hxy)) i

Result:
case intro
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
S : Set (ι → R)
hm : Set.MapsTo (fun v i => (eval v) (ps i)) S S
hinj : Set.InjOn (fun v i => (eval v) (ps i)) S
is_int : ∀ (x : R), IsIntegral K x
v : ι → R
hvS : v ∈ S
val✝ : Fintype ι
s : Finset R := (univ.biUnion fun i => image (fun x => coeff x (ps i)) (ps i).support) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι), ∀ k ∈ (ps i).support, coeff k (ps i) ∈ Algebra.adjoin K ↑s
this✝¹ : IsNoetherian K ↥(Algebra.adjoin K ↑s)
this✝ : Module.Finite K ↥(Algebra.adjoin K ↑s)
this : Finite ↥(Algebra.adjoin K ↑s)
S' : Set (ι → ↥(Algebra.adjoin K ↑s)) := (fun v => Subtype.val ∘ v) ⁻¹' S
res : ↑S' → ↑S' := fun x => ⟨fun i => ⟨(eval fun j => ↑(↑x j)) (ps i), ⋯⟩, ⋯⟩
hres_surj : Function.Surjective res
⊢ v ∈ (fun v i => (eval v) (ps i)) '' S

Proof state:
case intro
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
S : Set (ι → R)
hm : Set.MapsTo (fun v i => (eval v) (ps i)) S S
hinj : Set.InjOn (fun v i => (eval v) (ps i)) S
is_int : ∀ (x : R), IsIntegral K x
v : ι → R
hvS : v ∈ S
val✝ : Fintype ι
s : Finset R := (univ.biUnion fun i => image (fun x => coeff x (ps i)) (ps i).support) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι), ∀ k ∈ (ps i).support, coeff k (ps i) ∈ Algebra.adjoin K ↑s
⊢ v ∈ (fun v i => (eval v) (ps i)) '' S

Tactic:
have := isNoetherian_adjoin_finset s fun x _ => is_int x

Result:
case intro
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
S : Set (ι → R)
hm : Set.MapsTo (fun v i => (eval v) (ps i)) S S
hinj : Set.InjOn (fun v i => (eval v) (ps i)) S
is_int : ∀ (x : R), IsIntegral K x
v : ι → R
hvS : v ∈ S
val✝ : Fintype ι
s : Finset R := (univ.biUnion fun i => image (fun x => coeff x (ps i)) (ps i).support) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι), ∀ k ∈ (ps i).support, coeff k (ps i) ∈ Algebra.adjoin K ↑s
this : IsNoetherian K ↥(Algebra.adjoin K ↑s)
⊢ v ∈ (fun v i => (eval v) (ps i)) '' S