awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.AxGrothendieck (hypothesis)
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
v : (i : ι) → R
hvS : v ∈ S
val : Fintype ι
s : Finset R :=
  (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_1 : IsNoetherian.{u_2, u_3} K ↥(Algebra.adjoin K (↑s : Set R))
this : Finite.{u_3 + 1} ↥(Algebra.adjoin K (↑s : Set R))
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
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))
          ⋯)
      ⋯
x y : (↑S' : Type (max u_1 u_3))
hxy : res x = res y
i : ι
⊢ (↑((↑x : ι → ↥(Algebra.adjoin K (↑s : Set R))) i) : R) = (↑((↑y : ι → ↥(Algebra.adjoin K (↑s : Set R))) i) : R)
have hxy₁ : ∀ (x_1 : ι),
  (↑((↑(res x) : ι → ↥(Algebra.adjoin K (↑s : Set R))) x_1) : R) =
    (↑((↑(res y) : ι → ↥(Algebra.adjoin K (↑s : Set R))) x_1) : R)
Tactic: simp only [Subtype.ext_iff, funext_iff] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.FieldTheory.AxGrothendieck (hypothesis)
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
v : (i : ι) → R
hvS : v ∈ S
val : Fintype ι
s : Finset R :=
  (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_1 : IsNoetherian.{u_2, u_3} K ↥(Algebra.adjoin K (↑s : Set R))
this : Finite.{u_3 + 1} ↥(Algebra.adjoin K (↑s : Set R))
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
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))
          ⋯)
      ⋯
⊢ Membership.mem (γ := Set ((i : ι) → R))
    ((fun (v : ι → R) (i : ι) ↦ (eval v : (a : MvPolynomial ι R) → R) (ps i)) '' S) v
have hres_surj : Function.Surjective res
Tactic: 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
-- 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
v : (i : ι) → R
hvS : v ∈ S
val : Fintype ι
s : Finset R :=
  (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_1 : IsNoetherian.{u_2, u_3} K ↥(Algebra.adjoin K (↑s : Set R))
this : Finite.{u_3 + 1} ↥(Algebra.adjoin K (↑s : Set R))
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
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
have intro : ∀ (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),
  Membership.mem (γ := Set ((i : ι) → R))
    ((fun (v : ι → R) (i : ι) ↦ (eval v : (a : MvPolynomial ι R) → R) (ps i)) '' S) v
Tactic: rcases hres_surj ⟨fun i => ⟨v i, hv i⟩, hvS⟩ with ⟨⟨w, hwS'⟩, hw⟩
-- 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
v : (i : ι) → R
hvS : v ∈ S
val : Fintype ι
s : Finset R :=
  (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_1 : IsNoetherian.{u_2, u_3} K ↥(Algebra.adjoin K (↑s : Set R))
this : Finite.{u_3 + 1} ↥(Algebra.adjoin K (↑s : Set R))
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
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
have intro : ((fun (v : ι → R) (i : ι) ↦ ((eval v : (a : MvPolynomial ι R) → R) (ps i) : R)) fun (i : ι) ↦ (↑(w i) : R)) = v
Tactic: refine ⟨fun i => w i, hwS', ?_⟩
-- 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
⊢ Set.SurjOn (fun (v : ι → R) (i : ι) ↦ (eval v : (a : MvPolynomial ι R) → R) (ps i)) S S
have intro : ∀ ⦃v : (i : ι) → R⦄,
  v ∈ S →
    Membership.mem (γ := Set ((i : ι) → R))
      ((fun (v : ι → R) (i : ι) ↦ (eval v : (a : MvPolynomial ι R) → R) (ps i)) '' S) 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
-- 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
⊢ 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 ι),
  Membership.mem (γ := Set ((i : ι) → R))
    ((fun (v : ι → R) (i : ι) ↦ (eval v : (a : MvPolynomial ι R) → R) (ps i)) '' S) 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
-- 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
⊢ 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)),
    Membership.mem (γ := Set ((i : ι) → R))
      ((fun (v : ι → R) (i : ι) ↦ (eval v : (a : MvPolynomial ι R) → R) (ps i)) '' S) 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
-- Lean 4 proof step from Mathlib.FieldTheory.AxGrothendieck (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Finite α
K : Type u_3
inst_1 : Field K
inst_2 : CompatibleRing K
inst_3 : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
tauto tauto₁ :
  ∀ {S : Set (ι → K)} (f : (ι → K) → ι → K),
    (∀ ⦃x₁ : ι → K⦄, x₁ ∈ S → ∀ ⦃x₂ : ι → K⦄, x₂ ∈ S → f x₁ = f x₂ → x₁ = x₂) ↔
      ∀ (x y : ι → K), x ∈ S → y ∈ S → f x = f y → x = y
⊢ ∀ {S : Set (ι → K)} (f : (ι → K) → ι → K),
    (∀ ⦃x₁ : ι → K⦄, x₁ ∈ S → ∀ ⦃x₂ : ι → K⦄, x₂ ∈ S → f x₁ = f x₂ → x₁ = x₂) ↔
      ∀ (x y : ι → K), x ∈ S → y ∈ S → f x = f y → x = y
have mp : ∀ {S : Set (ι → K)} (f : (ι → K) → ι → K),
  (∀ ⦃x₁ : ι → K⦄, x₁ ∈ S → ∀ ⦃x₂ : ι → K⦄, x₂ ∈ S → f x₁ = f x₂ → x₁ = x₂) →
    ∀ (x y : ι → K), x ∈ S → y ∈ S → f x = f y → x = y
Tactic: tauto
-- Lean 4 proof step from Mathlib.FieldTheory.AxGrothendieck (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Finite α
K : Type u_3
inst_1 : Field K
inst_2 : CompatibleRing K
inst_3 : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
tauto tauto₁ :
  ∀ {S : Set (ι → K)} (f : (ι → K) → ι → K),
    (∀ ⦃x₁ : ι → K⦄, x₁ ∈ S → ∀ ⦃x₂ : ι → K⦄, x₂ ∈ S → f x₁ = f x₂ → x₁ = x₂) ↔
      ∀ (x y : ι → K), x ∈ S → y ∈ S → f x = f y → x = y
mp :
  ∀ {S : Set (ι → K)} (f : (ι → K) → ι → K),
    (∀ ⦃x₁ : ι → K⦄, x₁ ∈ S → ∀ ⦃x₂ : ι → K⦄, x₂ ∈ S → f x₁ = f x₂ → x₁ = x₂) →
      ∀ (x y : ι → K), x ∈ S → y ∈ S → f x = f y → x = y
⊢ ∀ {S : Set (ι → K)} (f : (ι → K) → ι → K),
    (∀ ⦃x₁ : ι → K⦄, x₁ ∈ S → ∀ ⦃x₂ : ι → K⦄, x₂ ∈ S → f x₁ = f x₂ → x₁ = x₂) ↔
      ∀ (x y : ι → K), x ∈ S → y ∈ S → f x = f y → x = y
have mpr : ∀ {S : Set (ι → K)} (f : (ι → K) → ι → K),
  (∀ (x y : ι → K), x ∈ S → y ∈ S → f x = f y → x = y) →
    ∀ ⦃x₁ : ι → K⦄, x₁ ∈ S → ∀ ⦃x₂ : ι → K⦄, x₂ ∈ S → f x₁ = f x₂ → x₁ = x₂
Tactic: tauto
-- Lean 4 proof step from Mathlib.FieldTheory.AxGrothendieck (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
inst : Finite α
K : Type u_3
inst_1 : Field K
inst_2 : CompatibleRing K
inst_3 : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
⊢ K ⊨ genericPolyMapSurjOnOfInjOn φ mons ↔
    ∀ (v : α → K) (p : { p : ι → MvPolynomial ι K // ∀ (i : ι), (p i).support ⊆ mons i }),
      let f : (ι → K) → ι → K := fun (v : ι → K) (i : ι) ↦
        (eval v : (a : MvPolynomial ι K) → K) ((↑p : ι → MvPolynomial ι K) i);
      let S : Set (ι → K) := {x : ι → K | φ.Realize (Sum.elim v x)};
      Set.MapsTo f S S → Set.InjOn f S → Set.SurjOn f S S
have injOnAlt : ∀ {S : Set (ι → K)} (f : (ι → K) → ι → K), Set.InjOn f S ↔ ∀ (x y : ι → K), x ∈ S → y ∈ S → f x = f y → x = y
Tactic: have injOnAlt : ∀ {S : Set (ι → K)} (f : (ι → K) → (ι → K)),
      S.InjOn f ↔ ∀ x y, x ∈ S → y ∈ S → f x = f y → x = y := by
    simp [Set.InjOn]; tauto
-- Lean 4 proof step from Mathlib.FieldTheory.AxGrothendieck (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Finite α
K : Type u_3
inst_1 : Field K
inst_2 : CompatibleRing K
inst_3 : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
⊢ K ⊨ genericPolyMapSurjOnOfInjOn φ mons ↔
    ∀ (v : α → K) (p : { p : ι → MvPolynomial ι K // ∀ (i : ι), (p i).support ⊆ mons i }),
      let f : (ι → K) → ι → K := fun (v : ι → K) (i : ι) ↦
        (eval v : (a : MvPolynomial ι K) → K) ((↑p : ι → MvPolynomial ι K) i);
      let S : Set (ι → K) := {x : ι → K | φ.Realize (Sum.elim v x)};
      Set.MapsTo f S S → Set.InjOn f S → Set.SurjOn f S S
have have : ∀ {S : Set (ι → K)} (f : (ι → K) → ι → K), Set.InjOn f S ↔ ∀ (x y : ι → K), x ∈ S → y ∈ S → f x = f y → x = y
Tactic: classical
  have injOnAlt : ∀ {S : Set (ι → K)} (f : (ι → K) → (ι → K)),
      S.InjOn f ↔ ∀ x y, x ∈ S → y ∈ S → f x = f y → x = y := by
    simp [Set.InjOn]; tauto
  simp only [Sentence.Realize, Formula.Realize, genericPolyMapSurjOnOfInjOn, Formula.relabel,
    Function.comp_def, Sum.map, id_eq, Equiv.sumAssoc, Equiv.coe_fn_symm_mk, Sum.elim_inr,
    realize_iAlls, realize_imp, realize_relabel, Fin.natAdd_zero, realize_subst, realize_iInf,
    realize_bdEqual, Term.realize_relabel,
    Equiv.forall_congr_left (Equiv.curry (Fin 2) ι K), Equiv.curry_symm_apply,
    Fin.forall_fin_succ_pi, Fin.forall_fin_zero_pi, realize_iExs, realize_inf, Sum.forall_sum,
    Set.MapsTo, Set.mem_setOf_eq, injOnAlt, funext_iff, Set.SurjOn, Set.image,
    Set.subset_def, Equiv.forall_congr_left (mvPolynomialSupportLEEquiv mons)]
  simp +singlePass only [← Sum.elim_comp_inl_inr]
  -- was `simp` and very slow (https://github.com/leanprover-community/mathlib4/issues/19751)
  simp only [Function.comp_def, Sum.elim_inl, Sum.elim_inr, Fin.castAdd_zero, Fin.cast_eq_self,
    Nat.add_zero, Term.realize_var, Term.realize_relabel, realize_termOfFreeCommRing,
    lift_genericPolyMap, Nat.reduceAdd, Fin.isValue, Function.uncurry_apply_pair, Fin.cons_zero,
    Fin.cons_one, ↓reduceIte, one_ne_zero]