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

Tactic:
refine ⟨fun i => w i, hwS', ?_⟩

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⟩
⊢ ((fun v i => (eval v) (ps i)) fun i => ↑(w i)) = v

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

Tactic:
let res : S' → S' := fun x => ⟨fun i =>
  ⟨eval (fun j : ι => (x.1 j : R)) (ps i), eval_mem (hs₁ _) fun i => (x.1 i).2⟩,
    hm x.2⟩

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

Proof state:
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⟩
⊢ ((fun v i => (eval v) (ps i)) fun i => ↑(w i)) = v

Tactic:
simpa [Subtype.ext_iff, funext_iff] using hw

Result:
no goals