[GOAL]
ι : 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
hinj : Injective fun v i => ↑(MvPolynomial.eval v) (ps i)
⊢ Surjective fun v i => ↑(MvPolynomial.eval v) (ps i)
[PROOFSTEP]
have is_int : ∀ x : R, IsIntegral K x := fun x => isAlgebraic_iff_isIntegral.1 (alg x)
[GOAL]
ι : 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
hinj : Injective fun v i => ↑(MvPolynomial.eval v) (ps i)
is_int : ∀ (x : R), IsIntegral K x
⊢ Surjective fun v i => ↑(MvPolynomial.eval v) (ps i)
[PROOFSTEP]
classical
intro v
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⟩))
letI := isNoetherian_adjoin_finset s fun x _ => is_int x
letI := Module.IsNoetherian.finite K (Algebra.adjoin K (s : Set R))
letI : Finite (Algebra.adjoin K (s : Set R)) :=
  FiniteDimensional.finite_of_finite K
    (Algebra.adjoin K (s : Set R))
      -- The restriction of the polynomial map, `ps`, to the subalgebra generated by `s`
let res : (ι → Algebra.adjoin K (s : Set R)) → ι → Algebra.adjoin K (s : Set R) := fun x i =>
  ⟨eval (fun j : ι => (x j : R)) (ps i), eval_mem (hs₁ _) fun i => (x i).2⟩
have hres_inj : Injective res := by
  intro x y hxy
  ext i
  simp only [Subtype.ext_iff, funext_iff] at hxy 
  exact congr_fun (hinj (funext hxy)) i
have hres_surj : Surjective res := Finite.injective_iff_surjective.1 hres_inj
cases' hres_surj fun i => ⟨v i, hv i⟩ with w hw
use fun i => w i
simpa only [Subtype.ext_iff, funext_iff] using hw
[GOAL]
ι : 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
hinj : Injective fun v i => ↑(MvPolynomial.eval v) (ps i)
is_int : ∀ (x : R), IsIntegral K x
⊢ Surjective fun v i => ↑(MvPolynomial.eval v) (ps i)
[PROOFSTEP]
intro v
[GOAL]
ι : 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
hinj : Injective fun v i => ↑(MvPolynomial.eval v) (ps i)
is_int : ∀ (x : R), IsIntegral K x
v : (i : ι) → (fun x => R) (ps i)
⊢ ∃ a, (fun v i => ↑(MvPolynomial.eval v) (ps i)) a = v
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
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
hinj : Injective fun v i => ↑(MvPolynomial.eval v) (ps i)
is_int : ∀ (x : R), IsIntegral K x
v : (i : ι) → (fun x => R) (ps i)
val✝ : Fintype ι
⊢ ∃ a, (fun v i => ↑(MvPolynomial.eval v) (ps i)) a = v
[PROOFSTEP]
let s : Finset R :=
  (Finset.biUnion (univ : Finset ι) fun i => (ps i).support.image fun x => coeff x (ps i)) ∪ (univ : Finset ι).image v
[GOAL]
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
hinj : Injective fun v i => ↑(MvPolynomial.eval v) (ps i)
is_int : ∀ (x : R), IsIntegral K x
v : (i : ι) → (fun x => R) (ps i)
val✝ : Fintype ι
s : Finset R :=
  (Finset.biUnion univ fun i => image (fun x => coeff x (ps i)) (MvPolynomial.support (ps i))) ∪ image v univ
⊢ ∃ a, (fun v i => ↑(MvPolynomial.eval v) (ps i)) a = v
[PROOFSTEP]
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⟩))
[GOAL]
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
hinj : Injective fun v i => ↑(MvPolynomial.eval v) (ps i)
is_int : ∀ (x : R), IsIntegral K x
v : (i : ι) → (fun x => R) (ps i)
val✝ : Fintype ι
s : Finset R :=
  (Finset.biUnion univ fun i => image (fun x => coeff x (ps i)) (MvPolynomial.support (ps i))) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
⊢ ∃ a, (fun v i => ↑(MvPolynomial.eval v) (ps i)) a = v
[PROOFSTEP]
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⟩))
[GOAL]
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
hinj : Injective fun v i => ↑(MvPolynomial.eval v) (ps i)
is_int : ∀ (x : R), IsIntegral K x
v : (i : ι) → (fun x => R) (ps i)
val✝ : Fintype ι
s : Finset R :=
  (Finset.biUnion univ fun i => image (fun x => coeff x (ps i)) (MvPolynomial.support (ps i))) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι) (k : ι →₀ ℕ), k ∈ MvPolynomial.support (ps i) → coeff k (ps i) ∈ Algebra.adjoin K ↑s
⊢ ∃ a, (fun v i => ↑(MvPolynomial.eval v) (ps i)) a = v
[PROOFSTEP]
letI := isNoetherian_adjoin_finset s fun x _ => is_int x
[GOAL]
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
hinj : Injective fun v i => ↑(MvPolynomial.eval v) (ps i)
is_int : ∀ (x : R), IsIntegral K x
v : (i : ι) → (fun x => R) (ps i)
val✝ : Fintype ι
s : Finset R :=
  (Finset.biUnion univ fun i => image (fun x => coeff x (ps i)) (MvPolynomial.support (ps i))) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι) (k : ι →₀ ℕ), k ∈ MvPolynomial.support (ps i) → coeff k (ps i) ∈ Algebra.adjoin K ↑s
this : IsNoetherian K { x // x ∈ Algebra.adjoin K ↑s } := isNoetherian_adjoin_finset s fun x x_1 => is_int x
⊢ ∃ a, (fun v i => ↑(MvPolynomial.eval v) (ps i)) a = v
[PROOFSTEP]
letI := Module.IsNoetherian.finite K (Algebra.adjoin K (s : Set R))
[GOAL]
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
hinj : Injective fun v i => ↑(MvPolynomial.eval v) (ps i)
is_int : ∀ (x : R), IsIntegral K x
v : (i : ι) → (fun x => R) (ps i)
val✝ : Fintype ι
s : Finset R :=
  (Finset.biUnion univ fun i => image (fun x => coeff x (ps i)) (MvPolynomial.support (ps i))) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι) (k : ι →₀ ℕ), k ∈ MvPolynomial.support (ps i) → coeff k (ps i) ∈ Algebra.adjoin K ↑s
this✝ : IsNoetherian K { x // x ∈ Algebra.adjoin K ↑s } := isNoetherian_adjoin_finset s fun x x_1 => is_int x
this : Module.Finite K { x // x ∈ Algebra.adjoin K ↑s } := Module.IsNoetherian.finite K { x // x ∈ Algebra.adjoin K ↑s }
⊢ ∃ a, (fun v i => ↑(MvPolynomial.eval v) (ps i)) a = v
[PROOFSTEP]
letI : Finite (Algebra.adjoin K (s : Set R)) :=
  FiniteDimensional.finite_of_finite K
    (Algebra.adjoin K (s : Set R))
      -- The restriction of the polynomial map, `ps`, to the subalgebra generated by `s`
[GOAL]
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
hinj : Injective fun v i => ↑(MvPolynomial.eval v) (ps i)
is_int : ∀ (x : R), IsIntegral K x
v : (i : ι) → (fun x => R) (ps i)
val✝ : Fintype ι
s : Finset R :=
  (Finset.biUnion univ fun i => image (fun x => coeff x (ps i)) (MvPolynomial.support (ps i))) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι) (k : ι →₀ ℕ), k ∈ MvPolynomial.support (ps i) → coeff k (ps i) ∈ Algebra.adjoin K ↑s
this✝¹ : IsNoetherian K { x // x ∈ Algebra.adjoin K ↑s } := isNoetherian_adjoin_finset s fun x x_1 => is_int x
this✝ : Module.Finite K { x // x ∈ Algebra.adjoin K ↑s } :=
  Module.IsNoetherian.finite K { x // x ∈ Algebra.adjoin K ↑s }
this : Finite { x // x ∈ Algebra.adjoin K ↑s } := FiniteDimensional.finite_of_finite K { x // x ∈ Algebra.adjoin K ↑s }
⊢ ∃ a, (fun v i => ↑(MvPolynomial.eval v) (ps i)) a = v
[PROOFSTEP]
let res : (ι → Algebra.adjoin K (s : Set R)) → ι → Algebra.adjoin K (s : Set R) := fun x i =>
  ⟨eval (fun j : ι => (x j : R)) (ps i), eval_mem (hs₁ _) fun i => (x i).2⟩
[GOAL]
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
hinj : Injective fun v i => ↑(MvPolynomial.eval v) (ps i)
is_int : ∀ (x : R), IsIntegral K x
v : (i : ι) → (fun x => R) (ps i)
val✝ : Fintype ι
s : Finset R :=
  (Finset.biUnion univ fun i => image (fun x => coeff x (ps i)) (MvPolynomial.support (ps i))) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι) (k : ι →₀ ℕ), k ∈ MvPolynomial.support (ps i) → coeff k (ps i) ∈ Algebra.adjoin K ↑s
this✝¹ : IsNoetherian K { x // x ∈ Algebra.adjoin K ↑s } := isNoetherian_adjoin_finset s fun x x_1 => is_int x
this✝ : Module.Finite K { x // x ∈ Algebra.adjoin K ↑s } :=
  Module.IsNoetherian.finite K { x // x ∈ Algebra.adjoin K ↑s }
this : Finite { x // x ∈ Algebra.adjoin K ↑s } := FiniteDimensional.finite_of_finite K { x // x ∈ Algebra.adjoin K ↑s }
res : (ι → { x // x ∈ Algebra.adjoin K ↑s }) → ι → { x // x ∈ Algebra.adjoin K ↑s } :=
  fun x i =>
    { val := ↑(MvPolynomial.eval fun j => ↑(x j)) (ps i),
      property := (_ : ↑(MvPolynomial.eval fun j => ↑(x j)) (ps i) ∈ Algebra.adjoin K ↑s) }
⊢ ∃ a, (fun v i => ↑(MvPolynomial.eval v) (ps i)) a = v
[PROOFSTEP]
have hres_inj : Injective res := by
  intro x y hxy
  ext i
  simp only [Subtype.ext_iff, funext_iff] at hxy 
  exact congr_fun (hinj (funext hxy)) i
[GOAL]
ι : 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
hinj : Injective fun v i => ↑(MvPolynomial.eval v) (ps i)
is_int : ∀ (x : R), IsIntegral K x
v : (i : ι) → (fun x => R) (ps i)
val✝ : Fintype ι
s : Finset R :=
  (Finset.biUnion univ fun i => image (fun x => coeff x (ps i)) (MvPolynomial.support (ps i))) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι) (k : ι →₀ ℕ), k ∈ MvPolynomial.support (ps i) → coeff k (ps i) ∈ Algebra.adjoin K ↑s
this✝¹ : IsNoetherian K { x // x ∈ Algebra.adjoin K ↑s } := isNoetherian_adjoin_finset s fun x x_1 => is_int x
this✝ : Module.Finite K { x // x ∈ Algebra.adjoin K ↑s } :=
  Module.IsNoetherian.finite K { x // x ∈ Algebra.adjoin K ↑s }
this : Finite { x // x ∈ Algebra.adjoin K ↑s } := FiniteDimensional.finite_of_finite K { x // x ∈ Algebra.adjoin K ↑s }
res : (ι → { x // x ∈ Algebra.adjoin K ↑s }) → ι → { x // x ∈ Algebra.adjoin K ↑s } :=
  fun x i =>
    { val := ↑(MvPolynomial.eval fun j => ↑(x j)) (ps i),
      property := (_ : ↑(MvPolynomial.eval fun j => ↑(x j)) (ps i) ∈ Algebra.adjoin K ↑s) }
⊢ Injective res
[PROOFSTEP]
intro x y hxy
[GOAL]
ι : 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
hinj : Injective fun v i => ↑(MvPolynomial.eval v) (ps i)
is_int : ∀ (x : R), IsIntegral K x
v : (i : ι) → (fun x => R) (ps i)
val✝ : Fintype ι
s : Finset R :=
  (Finset.biUnion univ fun i => image (fun x => coeff x (ps i)) (MvPolynomial.support (ps i))) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι) (k : ι →₀ ℕ), k ∈ MvPolynomial.support (ps i) → coeff k (ps i) ∈ Algebra.adjoin K ↑s
this✝¹ : IsNoetherian K { x // x ∈ Algebra.adjoin K ↑s } := isNoetherian_adjoin_finset s fun x x_1 => is_int x
this✝ : Module.Finite K { x // x ∈ Algebra.adjoin K ↑s } :=
  Module.IsNoetherian.finite K { x // x ∈ Algebra.adjoin K ↑s }
this : Finite { x // x ∈ Algebra.adjoin K ↑s } := FiniteDimensional.finite_of_finite K { x // x ∈ Algebra.adjoin K ↑s }
res : (ι → { x // x ∈ Algebra.adjoin K ↑s }) → ι → { x // x ∈ Algebra.adjoin K ↑s } :=
  fun x i =>
    { val := ↑(MvPolynomial.eval fun j => ↑(x j)) (ps i),
      property := (_ : ↑(MvPolynomial.eval fun j => ↑(x j)) (ps i) ∈ Algebra.adjoin K ↑s) }
x y : ι → { x // x ∈ Algebra.adjoin K ↑s }
hxy : res x = res y
⊢ x = y
[PROOFSTEP]
ext i
[GOAL]
case 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
hinj : Injective fun v i => ↑(MvPolynomial.eval v) (ps i)
is_int : ∀ (x : R), IsIntegral K x
v : (i : ι) → (fun x => R) (ps i)
val✝ : Fintype ι
s : Finset R :=
  (Finset.biUnion univ fun i => image (fun x => coeff x (ps i)) (MvPolynomial.support (ps i))) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι) (k : ι →₀ ℕ), k ∈ MvPolynomial.support (ps i) → coeff k (ps i) ∈ Algebra.adjoin K ↑s
this✝¹ : IsNoetherian K { x // x ∈ Algebra.adjoin K ↑s } := isNoetherian_adjoin_finset s fun x x_1 => is_int x
this✝ : Module.Finite K { x // x ∈ Algebra.adjoin K ↑s } :=
  Module.IsNoetherian.finite K { x // x ∈ Algebra.adjoin K ↑s }
this : Finite { x // x ∈ Algebra.adjoin K ↑s } := FiniteDimensional.finite_of_finite K { x // x ∈ Algebra.adjoin K ↑s }
res : (ι → { x // x ∈ Algebra.adjoin K ↑s }) → ι → { x // x ∈ Algebra.adjoin K ↑s } :=
  fun x i =>
    { val := ↑(MvPolynomial.eval fun j => ↑(x j)) (ps i),
      property := (_ : ↑(MvPolynomial.eval fun j => ↑(x j)) (ps i) ∈ Algebra.adjoin K ↑s) }
x y : ι → { x // x ∈ Algebra.adjoin K ↑s }
hxy : res x = res y
i : ι
⊢ ↑(x i) = ↑(y i)
[PROOFSTEP]
simp only [Subtype.ext_iff, funext_iff] at hxy 
[GOAL]
case 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
hinj : Injective fun v i => ↑(MvPolynomial.eval v) (ps i)
is_int : ∀ (x : R), IsIntegral K x
v : (i : ι) → (fun x => R) (ps i)
val✝ : Fintype ι
s : Finset R :=
  (Finset.biUnion univ fun i => image (fun x => coeff x (ps i)) (MvPolynomial.support (ps i))) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι) (k : ι →₀ ℕ), k ∈ MvPolynomial.support (ps i) → coeff k (ps i) ∈ Algebra.adjoin K ↑s
this✝¹ : IsNoetherian K { x // x ∈ Algebra.adjoin K ↑s } := isNoetherian_adjoin_finset s fun x x_1 => is_int x
this✝ : Module.Finite K { x // x ∈ Algebra.adjoin K ↑s } :=
  Module.IsNoetherian.finite K { x // x ∈ Algebra.adjoin K ↑s }
this : Finite { x // x ∈ Algebra.adjoin K ↑s } := FiniteDimensional.finite_of_finite K { x // x ∈ Algebra.adjoin K ↑s }
res : (ι → { x // x ∈ Algebra.adjoin K ↑s }) → ι → { x // x ∈ Algebra.adjoin K ↑s } :=
  fun x i =>
    { val := ↑(MvPolynomial.eval fun j => ↑(x j)) (ps i),
      property := (_ : ↑(MvPolynomial.eval fun j => ↑(x j)) (ps i) ∈ Algebra.adjoin K ↑s) }
x y : ι → { x // x ∈ Algebra.adjoin K ↑s }
i : ι
hxy : ∀ (a : ι), ↑(MvPolynomial.eval fun j => ↑(x j)) (ps a) = ↑(MvPolynomial.eval fun j => ↑(y j)) (ps a)
⊢ ↑(x i) = ↑(y i)
[PROOFSTEP]
exact congr_fun (hinj (funext hxy)) i
[GOAL]
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
hinj : Injective fun v i => ↑(MvPolynomial.eval v) (ps i)
is_int : ∀ (x : R), IsIntegral K x
v : (i : ι) → (fun x => R) (ps i)
val✝ : Fintype ι
s : Finset R :=
  (Finset.biUnion univ fun i => image (fun x => coeff x (ps i)) (MvPolynomial.support (ps i))) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι) (k : ι →₀ ℕ), k ∈ MvPolynomial.support (ps i) → coeff k (ps i) ∈ Algebra.adjoin K ↑s
this✝¹ : IsNoetherian K { x // x ∈ Algebra.adjoin K ↑s } := isNoetherian_adjoin_finset s fun x x_1 => is_int x
this✝ : Module.Finite K { x // x ∈ Algebra.adjoin K ↑s } :=
  Module.IsNoetherian.finite K { x // x ∈ Algebra.adjoin K ↑s }
this : Finite { x // x ∈ Algebra.adjoin K ↑s } := FiniteDimensional.finite_of_finite K { x // x ∈ Algebra.adjoin K ↑s }
res : (ι → { x // x ∈ Algebra.adjoin K ↑s }) → ι → { x // x ∈ Algebra.adjoin K ↑s } :=
  fun x i =>
    { val := ↑(MvPolynomial.eval fun j => ↑(x j)) (ps i),
      property := (_ : ↑(MvPolynomial.eval fun j => ↑(x j)) (ps i) ∈ Algebra.adjoin K ↑s) }
hres_inj : Injective res
⊢ ∃ a, (fun v i => ↑(MvPolynomial.eval v) (ps i)) a = v
[PROOFSTEP]
have hres_surj : Surjective res := Finite.injective_iff_surjective.1 hres_inj
[GOAL]
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
hinj : Injective fun v i => ↑(MvPolynomial.eval v) (ps i)
is_int : ∀ (x : R), IsIntegral K x
v : (i : ι) → (fun x => R) (ps i)
val✝ : Fintype ι
s : Finset R :=
  (Finset.biUnion univ fun i => image (fun x => coeff x (ps i)) (MvPolynomial.support (ps i))) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι) (k : ι →₀ ℕ), k ∈ MvPolynomial.support (ps i) → coeff k (ps i) ∈ Algebra.adjoin K ↑s
this✝¹ : IsNoetherian K { x // x ∈ Algebra.adjoin K ↑s } := isNoetherian_adjoin_finset s fun x x_1 => is_int x
this✝ : Module.Finite K { x // x ∈ Algebra.adjoin K ↑s } :=
  Module.IsNoetherian.finite K { x // x ∈ Algebra.adjoin K ↑s }
this : Finite { x // x ∈ Algebra.adjoin K ↑s } := FiniteDimensional.finite_of_finite K { x // x ∈ Algebra.adjoin K ↑s }
res : (ι → { x // x ∈ Algebra.adjoin K ↑s }) → ι → { x // x ∈ Algebra.adjoin K ↑s } :=
  fun x i =>
    { val := ↑(MvPolynomial.eval fun j => ↑(x j)) (ps i),
      property := (_ : ↑(MvPolynomial.eval fun j => ↑(x j)) (ps i) ∈ Algebra.adjoin K ↑s) }
hres_inj : Injective res
hres_surj : Surjective res
⊢ ∃ a, (fun v i => ↑(MvPolynomial.eval v) (ps i)) a = v
[PROOFSTEP]
cases' hres_surj fun i => ⟨v i, hv i⟩ with w hw
[GOAL]
case intro.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
hinj : Injective fun v i => ↑(MvPolynomial.eval v) (ps i)
is_int : ∀ (x : R), IsIntegral K x
v : (i : ι) → (fun x => R) (ps i)
val✝ : Fintype ι
s : Finset R :=
  (Finset.biUnion univ fun i => image (fun x => coeff x (ps i)) (MvPolynomial.support (ps i))) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι) (k : ι →₀ ℕ), k ∈ MvPolynomial.support (ps i) → coeff k (ps i) ∈ Algebra.adjoin K ↑s
this✝¹ : IsNoetherian K { x // x ∈ Algebra.adjoin K ↑s } := isNoetherian_adjoin_finset s fun x x_1 => is_int x
this✝ : Module.Finite K { x // x ∈ Algebra.adjoin K ↑s } :=
  Module.IsNoetherian.finite K { x // x ∈ Algebra.adjoin K ↑s }
this : Finite { x // x ∈ Algebra.adjoin K ↑s } := FiniteDimensional.finite_of_finite K { x // x ∈ Algebra.adjoin K ↑s }
res : (ι → { x // x ∈ Algebra.adjoin K ↑s }) → ι → { x // x ∈ Algebra.adjoin K ↑s } :=
  fun x i =>
    { val := ↑(MvPolynomial.eval fun j => ↑(x j)) (ps i),
      property := (_ : ↑(MvPolynomial.eval fun j => ↑(x j)) (ps i) ∈ Algebra.adjoin K ↑s) }
hres_inj : Injective res
hres_surj : Surjective res
w : ι → { x // x ∈ Algebra.adjoin K ↑s }
hw : res w = fun i => { val := v i, property := (_ : v i ∈ Algebra.adjoin K ↑s) }
⊢ ∃ a, (fun v i => ↑(MvPolynomial.eval v) (ps i)) a = v
[PROOFSTEP]
use fun i => w i
[GOAL]
case h
ι : 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
hinj : Injective fun v i => ↑(MvPolynomial.eval v) (ps i)
is_int : ∀ (x : R), IsIntegral K x
v : (i : ι) → (fun x => R) (ps i)
val✝ : Fintype ι
s : Finset R :=
  (Finset.biUnion univ fun i => image (fun x => coeff x (ps i)) (MvPolynomial.support (ps i))) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι) (k : ι →₀ ℕ), k ∈ MvPolynomial.support (ps i) → coeff k (ps i) ∈ Algebra.adjoin K ↑s
this✝¹ : IsNoetherian K { x // x ∈ Algebra.adjoin K ↑s } := isNoetherian_adjoin_finset s fun x x_1 => is_int x
this✝ : Module.Finite K { x // x ∈ Algebra.adjoin K ↑s } :=
  Module.IsNoetherian.finite K { x // x ∈ Algebra.adjoin K ↑s }
this : Finite { x // x ∈ Algebra.adjoin K ↑s } := FiniteDimensional.finite_of_finite K { x // x ∈ Algebra.adjoin K ↑s }
res : (ι → { x // x ∈ Algebra.adjoin K ↑s }) → ι → { x // x ∈ Algebra.adjoin K ↑s } :=
  fun x i =>
    { val := ↑(MvPolynomial.eval fun j => ↑(x j)) (ps i),
      property := (_ : ↑(MvPolynomial.eval fun j => ↑(x j)) (ps i) ∈ Algebra.adjoin K ↑s) }
hres_inj : Injective res
hres_surj : Surjective res
w : ι → { x // x ∈ Algebra.adjoin K ↑s }
hw : res w = fun i => { val := v i, property := (_ : v i ∈ Algebra.adjoin K ↑s) }
⊢ ((fun v i => ↑(MvPolynomial.eval v) (ps i)) fun i => ↑(w i)) = v
[PROOFSTEP]
simpa only [Subtype.ext_iff, funext_iff] using hw
