-- 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 ι
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)
⊢ v ∈ (fun v i => (eval v) (ps i)) '' S

Tactic:
let S' : Set (ι → Algebra.adjoin K (s : Set R)) :=
  (fun v => Subtype.val ∘ v) ⁻¹' S

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
⊢ 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
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

Tactic:
rcases hres_surj ⟨fun i => ⟨v i, hv i⟩, hvS⟩ with ⟨⟨w, hwS'⟩, hw⟩

Result:
case intro.intro.mk
ι : 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
w : ι → ↥(Algebra.adjoin K ↑s)
hwS' : w ∈ S'
hw : res ⟨w, hwS'⟩ = ⟨fun i => ⟨v i, ⋯⟩, hvS⟩
⊢ 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
⊢ Set.SurjOn (fun v i => (eval v) (ps i)) S S

Tactic:
intro v hvS

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
v : ι → R
hvS : v ∈ S
⊢ v ∈ (fun v i => (eval v) (ps i)) '' S

Proof state:
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)

Tactic:
simp only [Subtype.ext_iff, funext_iff] at hxy

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'
i : ι
hxy : ∀ (x_1 : ι), ↑(↑(res x) x_1) = ↑(↑(res y) x_1)
⊢ ↑(↑x i) = ↑(↑y i)