-- Lean 4 proof step from Mathlib.FieldTheory.AxGrothendieck (goal)
Goal:
ι : Type u_1
K : Type u_2
R : Type u_3
inst : Field K
inst_1 : Finite K
inst_2 : CommRing R
inst_3 : Finite ι
inst_4 : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
S : Set (ι → R)
hm : Set.MapsTo (fun (v : ι → R) (i : ι) ↦ (eval v : (a : MvPolynomial ι R) → R) (ps i)) S S
hinj : Set.InjOn (β := (i : ι) → R) (fun (v : ι → R) (i : ι) ↦ (eval v : (a : MvPolynomial ι R) → R) (ps i)) S
is_int : ∀ (x : R), IsIntegral K x
intro intro₁ :
  ∀ ⦃v : (i : ι) → R⦄ (hvS : v ∈ S),
    Membership.mem (γ := Set ((i : ι) → R))
      ((fun (v : ι → R) (i : ι) ↦ (eval v : (a : MvPolynomial ι R) → R) (ps i)) '' S) v
intro₂ :
  ∀ ⦃v : (i : ι) → R⦄ (hvS : v ∈ S) (val : Fintype ι),
    Membership.mem (γ := Set ((i : ι) → R))
      ((fun (v : ι → R) (i : ι) ↦ (eval v : (a : MvPolynomial ι R) → R) (ps i)) '' S) v
intro₃ :
  ∀ ⦃v : (i : ι) → R⦄ (hvS : v ∈ S) (val : Fintype ι),
    Membership.mem (γ := Set ((i : ι) → R))
      ((fun (v : ι → R) (i : ι) ↦ (eval v : (a : MvPolynomial ι R) → R) (ps i)) '' S) v
intro₄ :
  ∀ ⦃v : (i : ι) → R⦄ (hvS : v ∈ S) (val : Fintype ι),
    let s :=
      (Finset.biUnion univ fun (i : ι) ↦ image (fun (x : ι →₀ ℕ) ↦ coeff x (ps i)) (ps i).support) ∪ image v univ;
    ∀ (hv : ∀ (i : ι), Membership.mem (γ := Subalgebra K R) (Algebra.adjoin K (↑s : Set R)) (v i)),
      Membership.mem (γ := Set ((i : ι) → R))
        ((fun (v : ι → R) (i : ι) ↦ (eval v : (a : MvPolynomial ι R) → R) (ps i)) '' S) v
intro₅ :
  ∀ ⦃v : (i : ι) → R⦄ (hvS : v ∈ S) (val : Fintype ι),
    let s :=
      (Finset.biUnion univ fun (i : ι) ↦ image (fun (x : ι →₀ ℕ) ↦ coeff x (ps i)) (ps i).support) ∪ image v univ;
    ∀ (hv : ∀ (i : ι), Membership.mem (γ := Subalgebra K R) (Algebra.adjoin K (↑s : Set R)) (v i))
      (hs₁ :
        ∀ (i : ι),
          ∀ k ∈ (ps i).support, Membership.mem (γ := Subalgebra K R) (Algebra.adjoin K (↑s : Set R)) (coeff k (ps i))),
      Membership.mem (γ := Set ((i : ι) → R))
        ((fun (v : ι → R) (i : ι) ↦ (eval v : (a : MvPolynomial ι R) → R) (ps i)) '' S) v
intro₆ :
  ∀ ⦃v : (i : ι) → R⦄ (hvS : v ∈ S) (val : Fintype ι),
    let s :=
      (Finset.biUnion univ fun (i : ι) ↦ image (fun (x : ι →₀ ℕ) ↦ coeff x (ps i)) (ps i).support) ∪ image v univ;
    ∀ (hv : ∀ (i : ι), Membership.mem (γ := Subalgebra K R) (Algebra.adjoin K (↑s : Set R)) (v i))
      (hs₁ :
        ∀ (i : ι),
          ∀ k ∈ (ps i).support, Membership.mem (γ := Subalgebra K R) (Algebra.adjoin K (↑s : Set R)) (coeff k (ps i)))
      (this : IsNoetherian.{u_2, u_3} K ↥(Algebra.adjoin K (↑s : Set R))),
      Membership.mem (γ := Set ((i : ι) → R))
        ((fun (v : ι → R) (i : ι) ↦ (eval v : (a : MvPolynomial ι R) → R) (ps i)) '' S) v
intro₇ intro₈ intro₉ :
  ∀ ⦃v : (i : ι) → R⦄ (hvS : v ∈ S) (val : Fintype ι),
    let s :=
      (Finset.biUnion univ fun (i : ι) ↦ image (fun (x : ι →₀ ℕ) ↦ coeff x (ps i)) (ps i).support) ∪ image v univ;
    ∀ (hv : ∀ (i : ι), Membership.mem (γ := Subalgebra K R) (Algebra.adjoin K (↑s : Set R)) (v i))
      (hs₁ :
        ∀ (i : ι),
          ∀ k ∈ (ps i).support, Membership.mem (γ := Subalgebra K R) (Algebra.adjoin K (↑s : Set R)) (coeff k (ps i)))
      (this : IsNoetherian.{u_2, u_3} K ↥(Algebra.adjoin K (↑s : Set R)))
      (this : Finite.{u_3 + 1} ↥(Algebra.adjoin K (↑s : Set R))),
      Membership.mem (γ := Set ((i : ι) → R))
        ((fun (v : ι → R) (i : ι) ↦ (eval v : (a : MvPolynomial ι R) → R) (ps i)) '' S) v
intro₁₀ :
  ∀ ⦃v : (i : ι) → R⦄ (hvS : v ∈ S) (val : Fintype ι),
    let s :=
      (Finset.biUnion univ fun (i : ι) ↦ image (fun (x : ι →₀ ℕ) ↦ coeff x (ps i)) (ps i).support) ∪ image v univ;
    ∀ (hv : ∀ (i : ι), Membership.mem (γ := Subalgebra K R) (Algebra.adjoin K (↑s : Set R)) (v i))
      (hs₁ :
        ∀ (i : ι),
          ∀ k ∈ (ps i).support, Membership.mem (γ := Subalgebra K R) (Algebra.adjoin K (↑s : Set R)) (coeff k (ps i)))
      (this : IsNoetherian.{u_2, u_3} K ↥(Algebra.adjoin K (↑s : Set R)))
      (this : Finite.{u_3 + 1} ↥(Algebra.adjoin K (↑s : Set R))),
      let S' : Set (ι → ↥(Algebra.adjoin K (↑s : Set R))) :=
        (fun (v : ι → ↥(Algebra.adjoin K (↑s : Set R))) ↦
            Subtype.val (p := fun (x : R) ↦ Membership.mem (γ := Subalgebra K R) (Algebra.adjoin K (↑s : Set R)) x) ∘
              v) ⁻¹'
          S;
      let res : (↑S' : Type (max u_1 u_3)) → (↑S' : Type (max u_1 u_3)) := fun (x : (↑S' : Type (max u_1 u_3))) ↦
        Subtype.mk (p := fun (x : ι → ↥(Algebra.adjoin K (↑s : Set R))) ↦ x ∈ S')
          (fun (i : ι) ↦
            Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subalgebra K R) (Algebra.adjoin K (↑s : Set R)) x)
              ((eval fun (j : ι) ↦ (↑((↑x : ι → ↥(Algebra.adjoin K (↑s : Set R))) j) : R) : (a : MvPolynomial ι R) → R)
                (ps i))
              ⋯)
          ⋯;
      ∀ (hres_surj : Function.Surjective res),
        Membership.mem (γ := Set ((i : ι) → R))
          ((fun (v : ι → R) (i : ι) ↦ (eval v : (a : MvPolynomial ι R) → R) (ps i)) '' S) v
intro₁₁ :
  ∀ ⦃v : (i : ι) → R⦄ (hvS : v ∈ S) (val : Fintype ι),
    let s :=
      (Finset.biUnion univ fun (i : ι) ↦ image (fun (x : ι →₀ ℕ) ↦ coeff x (ps i)) (ps i).support) ∪ image v univ;
    ∀ (hv : ∀ (i : ι), Membership.mem (γ := Subalgebra K R) (Algebra.adjoin K (↑s : Set R)) (v i))
      (hs₁ :
        ∀ (i : ι),
          ∀ k ∈ (ps i).support, Membership.mem (γ := Subalgebra K R) (Algebra.adjoin K (↑s : Set R)) (coeff k (ps i)))
      (this : IsNoetherian.{u_2, u_3} K ↥(Algebra.adjoin K (↑s : Set R)))
      (this : Finite.{u_3 + 1} ↥(Algebra.adjoin K (↑s : Set R))),
      let S' : Set (ι → ↥(Algebra.adjoin K (↑s : Set R))) :=
        (fun (v : ι → ↥(Algebra.adjoin K (↑s : Set R))) ↦
            Subtype.val (p := fun (x : R) ↦ Membership.mem (γ := Subalgebra K R) (Algebra.adjoin K (↑s : Set R)) x) ∘
              v) ⁻¹'
          S;
      let res : (↑S' : Type (max u_1 u_3)) → (↑S' : Type (max u_1 u_3)) := fun (x : (↑S' : Type (max u_1 u_3))) ↦
        Subtype.mk (p := fun (x : ι → ↥(Algebra.adjoin K (↑s : Set R))) ↦ x ∈ S')
          (fun (i : ι) ↦
            Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subalgebra K R) (Algebra.adjoin K (↑s : Set R)) x)
              ((eval fun (j : ι) ↦ (↑((↑x : ι → ↥(Algebra.adjoin K (↑s : Set R))) j) : R) : (a : MvPolynomial ι R) → R)
                (ps i))
              ⋯)
          ⋯;
      ∀ (hres_surj : Function.Surjective res) (w : ι → ↥(Algebra.adjoin K (↑s : Set R))) (hwS' : w ∈ S')
        (hw :
          res (Subtype.mk (p := fun (x : ι → ↥(Algebra.adjoin K (↑s : Set R))) ↦ x ∈ S') w hwS') =
            Subtype.mk (p := fun (x : ι → ↥(Algebra.adjoin K (↑s : Set R))) ↦ x ∈ S')
              (fun (i : ι) ↦
                Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subalgebra K R) (Algebra.adjoin K (↑s : Set R)) x)
                  (v i) ⋯)
              hvS),
        Membership.mem (γ := Set ((i : ι) → R))
          ((fun (v : ι → R) (i : ι) ↦ (eval v : (a : MvPolynomial ι R) → R) (ps i)) '' S) v
⊢ Set.SurjOn (fun (v : ι → R) (i : ι) ↦ (eval v : (a : MvPolynomial ι R) → R) (ps i)) S S
have intro₁₂ : ∀ ⦃v : (i : ι) → R⦄ (hvS : v ∈ S) (val : Fintype ι),
  let s := (Finset.biUnion univ fun (i : ι) ↦ image (fun (x : ι →₀ ℕ) ↦ coeff x (ps i)) (ps i).support) ∪ image v univ;
  ∀ (hv : ∀ (i : ι), Membership.mem (γ := Subalgebra K R) (Algebra.adjoin K (↑s : Set R)) (v i))
    (hs₁ :
      ∀ (i : ι),
        ∀ k ∈ (ps i).support, Membership.mem (γ := Subalgebra K R) (Algebra.adjoin K (↑s : Set R)) (coeff k (ps i)))
    (this : IsNoetherian.{u_2, u_3} K ↥(Algebra.adjoin K (↑s : Set R)))
    (this : Finite.{u_3 + 1} ↥(Algebra.adjoin K (↑s : Set R))),
    let S' : Set (ι → ↥(Algebra.adjoin K (↑s : Set R))) :=
      (fun (v : ι → ↥(Algebra.adjoin K (↑s : Set R))) ↦
          Subtype.val (p := fun (x : R) ↦ Membership.mem (γ := Subalgebra K R) (Algebra.adjoin K (↑s : Set R)) x) ∘
            v) ⁻¹'
        S;
    let res : (↑S' : Type (max u_1 u_3)) → (↑S' : Type (max u_1 u_3)) := fun (x : (↑S' : Type (max u_1 u_3))) ↦
      Subtype.mk (p := fun (x : ι → ↥(Algebra.adjoin K (↑s : Set R))) ↦ x ∈ S')
        (fun (i : ι) ↦
          Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subalgebra K R) (Algebra.adjoin K (↑s : Set R)) x)
            ((eval fun (j : ι) ↦ (↑((↑x : ι → ↥(Algebra.adjoin K (↑s : Set R))) j) : R) : (a : MvPolynomial ι R) → R)
              (ps i))
            sorry)
        sorry;
    ∀ (hres_surj : Function.Surjective res) (w : ι → ↥(Algebra.adjoin K (↑s : Set R))) (hwS' : w ∈ S')
      (hw :
        res (Subtype.mk (p := fun (x : ι → ↥(Algebra.adjoin K (↑s : Set R))) ↦ x ∈ S') w hwS') =
          Subtype.mk (p := fun (x : ι → ↥(Algebra.adjoin K (↑s : Set R))) ↦ x ∈ S')
            (fun (i : ι) ↦
              Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subalgebra K R) (Algebra.adjoin K (↑s : Set R)) x)
                (v i) sorry)
            hvS),
      ((fun (v : ι → R) (i : ι) ↦ ((eval v : (a : MvPolynomial ι R) → R) (ps i) : R)) fun (i : ι) ↦ (↑(w i) : R)) = v
Tactic: classical
  intro v hvS
  cases nonempty_fintype ι
  /- `s` is the set of all coefficients of the polynomial, as well as all of
    the coordinates of `v`, the point I am trying to find the preimage of. -/
  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 : Finite (Algebra.adjoin K (s : Set R)) := Module.finite_of_finite K
  -- The restriction of the polynomial map, `ps`, to the subalgebra generated by `s`
  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