-- 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:
ι : 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), ⋯⟩, ⋯⟩
⊢ Function.Injective res

Tactic:
intro x y hxy

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

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

Tactic:
cases nonempty_fintype ι

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

Tactic:
have hv : ∀ i, v i ∈ Algebra.adjoin K (s : Set R) := fun j =>
  Algebra.subset_adjoin (mem_union_right _ (mem_image.2 ⟨j, mem_univ _, rfl⟩))

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

Tactic:
have := Module.IsNoetherian.finite K (Algebra.adjoin K (s : Set R))

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)
⊢ 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:
classical
intro v hvS
cases nonempty_fintype ι
let s : Finset R :=
  (Finset.biUnion (univ : Finset ι) fun i => (ps i).support.image fun x => coeff x (ps i)) ∪
    (univ : Finset ι).image v
have hv : ∀ i, v i ∈ Algebra.adjoin K (s : Set R) := fun j =>
  Algebra.subset_adjoin (mem_union_right _ (mem_image.2 ⟨j, mem_univ _, rfl⟩))
have hs₁ : ∀ (i : ι) (k : ι →₀ ℕ),
    k ∈ (ps i).support → coeff k (ps i) ∈ Algebra.adjoin K (s : Set R) :=
  fun i k hk => Algebra.subset_adjoin
    (mem_union_left _ (mem_biUnion.2 ⟨i, mem_univ _, mem_image_of_mem _ hk⟩))
have := isNoetherian_adjoin_finset s fun x _ => is_int x
have := Module.IsNoetherian.finite K (Algebra.adjoin K (s : Set R))
have : Finite (Algebra.adjoin K (s : Set R)) := Module.finite_of_finite K
let S' : Set (ι → Algebra.adjoin K (s : Set R)) :=
  (fun v => Subtype.val ∘ v) ⁻¹' S
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⟩
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
rcases hres_surj ⟨fun i => ⟨v i, hv i⟩, hvS⟩ with ⟨⟨w, hwS'⟩, hw⟩
refine ⟨fun i => w i, hwS', ?_⟩
simpa [Subtype.ext_iff, funext_iff] using hw

Result:
no goals