awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.AlgebraicClosure
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
⊢ Eq (α := IntermediateField (↥(algebraicClosure F E)) E) (algebraicClosure (↥(algebraicClosure F E)) E) ⊥

Tactic:
bot_unique fun x hx ↦ mem_bot.2
    ⟨⟨x, isIntegral_trans x (mem_algebraicClosure_iff'.1 hx)⟩, rfl⟩

Premises used: Iff.mpr, isIntegral_trans, Subtype.mk, mem_algebraicClosure_iff', Exists.intro, Iff.mp, bot_unique, IntermediateField.mem_bot, rfl
-- Module: Mathlib.FieldTheory.AlgebraicClosure
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
⊢ Eq (α := IntermediateField F E) (normalClosure F (↥(algebraicClosure F E)) E) (algebraicClosure F E)

Tactic:
le_antisymm (normalClosure_le_iff.2 fun i ↦
    haveI : Algebra.IsAlgebraic F i.fieldRange := (AlgEquiv.ofInjectiveField i).isAlgebraic
    le_algebraicClosure F E _) (le_normalClosure _)

Premises used: normalClosure_le_iff, Iff.mpr, le_algebraicClosure, AlgHom.fieldRange, le_antisymm, IntermediateField.le_normalClosure
-- Module: Mathlib.FieldTheory.AlgebraicClosure
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsAlgClosed E
⊢ Eq (α := IntermediateField F E) (algebraicClosure F E) ⊥ ↔ IsAlgClosed F

Tactic:
⟨fun h ↦ IsAlgClosed.of_exists_root _ fun p hmon hirr ↦ ?_,
    fun _ ↦ IntermediateField.eq_bot_of_isAlgClosed_of_isAlgebraic _⟩

Premises used: IntermediateField.eq_bot_of_isAlgClosed_of_isAlgebraic, algebraicClosure, Iff.intro, IsAlgClosed.of_exists_root
-- Module: Mathlib.FieldTheory.AlgebraicClosure
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsAlgClosed E
refine :
  ∀ (h : Eq (α := IntermediateField F E) (algebraicClosure F E) ⊥) (p : F[X]) (hmon : p.Monic) (hirr : Irreducible p),
    ∃ (x : F), eval x p = 0
⊢ Eq (α := IntermediateField F E) (algebraicClosure F E) ⊥ ↔ IsAlgClosed F

Tactic:
refine ⟨fun h ↦ IsAlgClosed.of_exists_root _ fun p hmon hirr ↦ ?_,
    fun _ ↦ IntermediateField.eq_bot_of_isAlgClosed_of_isAlgebraic _⟩
-- Module: Mathlib.FieldTheory.AlgebraicClosure
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsAlgClosed E
h : Eq (α := IntermediateField F E) (algebraicClosure F E) ⊥
p : F[X]
hmon : p.Monic
hirr : Irreducible p
obtain : ∀ (x : E) (hx : Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E) (0 : E)), ∃ (x : F), eval x p = 0
⊢ ∃ (x : F), eval x p = 0

Tactic:
obtain ⟨x, hx⟩ := IsAlgClosed.exists_aeval_eq_zero E p (degree_pos_of_irreducible hirr).ne'

Premises used: LT.lt.ne', Polynomial.degree_pos_of_irreducible, IsAlgClosed.exists_aeval_eq_zero
-- Module: Mathlib.FieldTheory.AlgebraicClosure
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsAlgClosed E
h : Eq (α := IntermediateField F E) (algebraicClosure F E) ⊥
p : F[X]
hmon : p.Monic
hirr : Irreducible p
x : E
hx : Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E) (0 : E)
obtain :
  ∀ (x : F)
    (hx :
      Eq.{u_2 + 1} (α := E)
        (((aeval ((AlgHom.toRingHom (Algebra.ofId F E) : (a : F) → E) x) : F[X] →ₐ[F] E) : (a : F[X]) → E) p : E)
        (0 : E)),
    ∃ (x : F), eval x p = 0
⊢ ∃ (x : F), eval x p = 0

Tactic:
obtain ⟨x, rfl⟩ := h ▸ mem_algebraicClosure_iff'.2 (minpoly.ne_zero_iff.1 <|
    ne_zero_of_dvd_ne_zero hmon.ne_zero (minpoly.dvd _ x hx))

Premises used: rfl
-- Module: Mathlib.FieldTheory.AlgebraicClosure
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsAlgClosed E
h : Eq (α := IntermediateField F E) (algebraicClosure F E) ⊥
p : F[X]
hmon : p.Monic
hirr : Irreducible p
x : F
hx :
  Eq.{u_2 + 1} (α := E)
    (((aeval ((AlgHom.toRingHom (Algebra.ofId F E) : (a : F) → E) x) : F[X] →ₐ[F] E) : (a : F[X]) → E) p : E) (0 : E)
⊢ eval x p = 0

Tactic:
simpa [Algebra.ofId_apply] using hx

Premises used: Algebra.ofId_apply
-- Module: Mathlib.FieldTheory.AlgebraicClosure
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsAlgClosed E
h : Eq (α := IntermediateField F E) (algebraicClosure F E) ⊥
p : F[X]
hmon : p.Monic
hirr : Irreducible p
x : F
hx :
  Eq.{u_2 + 1} (α := E)
    (((aeval ((AlgHom.toRingHom (Algebra.ofId F E) : (a : F) → E) x) : F[X] →ₐ[F] E) : (a : F[X]) → E) p : E) (0 : E)
⊢ ∃ (x : F), eval x p = 0

Tactic:
exact ⟨x, by simpa [Algebra.ofId_apply] using hx⟩
-- Module: Mathlib.FieldTheory.AlgebraicClosure
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
⊢ Algebra.IsAlgebraic.{u_1, u_2} F ↥(adjoin F S) ↔ ∀ x ∈ S, IsAlgebraic F x

Tactic:
((le_algebraicClosure_iff F E _).symm.trans (adjoin_le_iff.trans <| forall_congr' <|
    fun _ => Iff.imp Iff.rfl mem_algebraicClosure_iff))

Premises used: IntermediateField.adjoin_le_iff, Iff.rfl, mem_algebraicClosure_iff, Iff.imp, forall_congr', Iff.trans, le_algebraicClosure_iff, Iff.symm
-- Module: Mathlib.FieldTheory.AlgebraicClosure
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : IsAlgClosed E
⊢ IsAlgClosure.{u_1, u_2} F ↥(algebraicClosure F E)

Tactic:
⟨(IsAlgClosed.algebraicClosure_eq_bot_iff _ E).mp (algebraicClosure_eq_bot F E),
    isAlgebraic F E⟩

Premises used: IsAlgClosure.mk, algebraicClosure.algebraicClosure_eq_bot, algebraicClosure.isAlgebraic, Iff.mp, IsAlgClosed.algebraicClosure_eq_bot_iff
-- Module: Mathlib.FieldTheory.AlgebraicClosure
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
⊢ Eq (α := IntermediateField F E) (algebraicClosure F E) ⊤ ↔ Algebra.IsAlgebraic F E

Tactic:
⟨fun h ↦ ⟨fun _ ↦ mem_algebraicClosure_iff.1 (h ▸ mem_top)⟩,
    fun _ ↦ top_unique fun x _ ↦ mem_algebraicClosure_iff.2 (Algebra.IsAlgebraic.isAlgebraic x)⟩

Premises used: Iff.mpr, Algebra.IsAlgebraic.isAlgebraic, IntermediateField.mem_top, Eq.rec, mem_algebraicClosure_iff, Algebra.IsAlgebraic.mk, top_unique, Iff.intro, Iff.mp, Eq.symm
-- Module: Mathlib.FieldTheory.AlgebraicClosure
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
⊢ LE.le (α := IntermediateField F K) (algebraicClosure F K) (restrictScalars F (algebraicClosure E K))

Tactic:
fun _ h ↦ mem_algebraicClosure_iff.2 <| IsAlgebraic.tower_top E (mem_algebraicClosure_iff.1 h)

Premises used: Iff.mpr, Set.Mem, IsAlgebraic.tower_top, setOf, mem_algebraicClosure_iff, RingHom.IsIntegralElem, IsIntegral, Iff.mp
-- Module: Mathlib.FieldTheory.AlgebraicClosure
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsAlgebraic F E
⊢ Eq (α := IntermediateField F K) (algebraicClosure F K) (restrictScalars F (algebraicClosure E K))

Tactic:
(algebraicClosure.le_restrictScalars F E K).antisymm fun _ h ↦
    isIntegral_trans _ h

Premises used: isIntegral_trans, LE.le.antisymm, algebraicClosure.le_restrictScalars
-- Module: Mathlib.FieldTheory.AlgebraicClosure
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
⊢ LE.le (α := IntermediateField E K) (adjoin E (↑(algebraicClosure F K) : Set K)) (algebraicClosure E K)

Tactic:
adjoin_le_iff.2 <| le_restrictScalars F E K

Premises used: Iff.mpr, IntermediateField.adjoin_le_iff, algebraicClosure.le_restrictScalars
-- Module: Mathlib.FieldTheory.AlgebraicClosure
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
h : Splits (Polynomial.map (algebraMap F E) p)
⊢ Splits.{u_2} (R := ↥(_root_.algebraicClosure F E)) (Polynomial.map (algebraMap F ↥(_root_.algebraicClosure F E)) p)

Tactic:
splits_of_splits h fun _ hx ↦ (isAlgebraic_of_mem_rootSet hx).isIntegral

Premises used: IsAlgebraic.isIntegral, isAlgebraic_of_mem_rootSet, IntermediateField.splits_of_splits
-- Module: Mathlib.FieldTheory.AxGrothendieck
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
⊢ ∀ (x : R), IsIntegral K x

Tactic:
have is_int : ∀ x : R, IsIntegral K x := fun x => isAlgebraic_iff_isIntegral.1
    (alg.isAlgebraic x)
-- Module: Mathlib.FieldTheory.AxGrothendieck
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
intro :
  ∀ (val : Fintype ι),
    Membership.mem (γ := Set ((i : ι) → R))
      ((fun (v : ι → R) (i : ι) ↦ (eval v : (a : MvPolynomial ι R) → R) (ps i)) '' S) v
⊢ Membership.mem (γ := Set ((i : ι) → R))
    ((fun (v : ι → R) (i : ι) ↦ (eval v : (a : MvPolynomial ι R) → R) (ps i)) '' S) v

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.FieldTheory.AxGrothendieck
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
⊢ ∀ (i : ι), Membership.mem (γ := Subalgebra K R) (Algebra.adjoin K (↑s : Set R)) (v i)

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⟩))
-- Module: Mathlib.FieldTheory.AxGrothendieck
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)
⊢ ∀ (i : ι), ∀ k ∈ (ps i).support, Membership.mem (γ := Subalgebra K R) (Algebra.adjoin K (↑s : Set R)) (coeff k (ps i))

Tactic:
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⟩))
-- Module: Mathlib.FieldTheory.AxGrothendieck
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))
⊢ IsNoetherian.{u_2, u_3} K ↥(Algebra.adjoin K (↑s : Set R))

Tactic:
have := isNoetherian_adjoin_finset s fun x _ => is_int x
-- Module: Mathlib.FieldTheory.AxGrothendieck
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 : IsNoetherian.{u_2, u_3} K ↥(Algebra.adjoin K (↑s : Set R))
⊢ Finite.{u_3 + 1} ↥(Algebra.adjoin K (↑s : Set R))

Tactic:
have : Finite (Algebra.adjoin K (s : Set R)) := Module.finite_of_finite K
-- Module: Mathlib.FieldTheory.AxGrothendieck
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))
          ⋯)
      ⋯
rw : Function.Injective res
⊢ Function.Surjective res

Tactic:
rw [← Finite.injective_iff_surjective]

Premises used: Finite.injective_iff_surjective
-- Module: Mathlib.FieldTheory.AxGrothendieck
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
a :
  ∀ (i : ι),
    (↑((↑x : ι → ↥(Algebra.adjoin K (↑s : Set R))) i) : R) = (↑((↑y : ι → ↥(Algebra.adjoin K (↑s : Set R))) i) : R)
⊢ x = y

Tactic:
ext i
-- Module: Mathlib.FieldTheory.AxGrothendieck
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_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

Premises used: funext_iff, Subtype.ext_iff
-- Module: Mathlib.FieldTheory.AxGrothendieck
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))
i : ι
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)
⊢ (↑((↑x : ι → ↥(Algebra.adjoin K (↑s : Set R))) i) : R) = (↑((↑y : ι → ↥(Algebra.adjoin K (↑s : Set R))) i) : R)

Tactic:
congr_fun (hinj x.2 y.2 (funext hxy)) i

Premises used: funext, congr_fun, Subtype.property
-- Module: Mathlib.FieldTheory.AxGrothendieck
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))
i : ι
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)
⊢ (↑((↑x : ι → ↥(Algebra.adjoin K (↑s : Set R))) i) : R) = (↑((↑y : ι → ↥(Algebra.adjoin K (↑s : Set R))) i) : R)

Tactic:
exact congr_fun (hinj x.2 y.2 (funext hxy)) i

Premises used: funext, congr_fun, Subtype.property