awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x y z : E
hy : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) y
hz : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) z
hy' : IsSolvable.{u_1} (Gal (minpoly F y))
hz' : IsSolvable.{u_1} (Gal (minpoly F z))
⊢ Membership.mem (γ := IntermediateField F E) F⟮y, z⟯ z
have a : Membership.mem (γ := Set E) {y, z} z
Tactic: apply subset_adjoin
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x y z : E
hy : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) y
hz : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) z
hy' : IsSolvable.{u_1} (Gal (minpoly F y))
hz' : IsSolvable.{u_1} (Gal (minpoly F z))
⊢ IsSolvable.{u_1} (Gal (minpoly F (y * z)))
have apply : Membership.mem (γ := IntermediateField F E) F⟮y, z⟯ y
Tactic: apply induction_step hy hz (mul_mem hy hz) hy' hz' (mul_mem ..)
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x y z : E
hy : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) y
hz : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) z
hy' : IsSolvable.{u_1} (Gal (minpoly F y))
hz' : IsSolvable.{u_1} (Gal (minpoly F z))
apply : Membership.mem (γ := IntermediateField F E) F⟮y, z⟯ y
⊢ IsSolvable.{u_1} (Gal (minpoly F (y * z)))
have apply₁ : Membership.mem (γ := IntermediateField F E) F⟮y, z⟯ z
Tactic: apply induction_step hy hz (mul_mem hy hz) hy' hz' (mul_mem ..)
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
⊢ IsSolvable.{u_1} (Gal (minpoly F x))
have mem : ∀ (y : F), IsSolvable.{u_1} (Gal (minpoly.{u_1, u_2} F (B := E) ((algebraMap F E : (a : F) → E) y : E)))
Tactic: induction hx using solvableByRad.induction with
  | mem y => rw [minpoly.eq_X_sub_C E]; infer_instance
  | add y z hy hz hy' hz' =>
    apply induction_step hy hz (add_mem hy hz) hy' hz' (add_mem ..) <;> apply subset_adjoin <;> simp
  | mul y z hy hz hy' hz' =>
    apply induction_step hy hz (mul_mem hy hz) hy' hz' (mul_mem ..) <;> apply subset_adjoin <;> simp
  | rad n y hn hy hy' => exact induction_rad (solvableByRad.rad_mem hn hy) hn hy'
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
mem : ∀ (y : F), IsSolvable.{u_1} (Gal (minpoly.{u_1, u_2} F (B := E) ((algebraMap F E : (a : F) → E) y : E)))
⊢ IsSolvable.{u_1} (Gal (minpoly F x))
have add : ∀ (y z : E) (hy : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) y)
  (hz : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) z) (hy' : IsSolvable.{u_1} (Gal (minpoly F y)))
  (hz' : IsSolvable.{u_1} (Gal (minpoly F z))), IsSolvable.{u_1} (Gal (minpoly F (y + z)))
Tactic: induction hx using solvableByRad.induction with
  | mem y => rw [minpoly.eq_X_sub_C E]; infer_instance
  | add y z hy hz hy' hz' =>
    apply induction_step hy hz (add_mem hy hz) hy' hz' (add_mem ..) <;> apply subset_adjoin <;> simp
  | mul y z hy hz hy' hz' =>
    apply induction_step hy hz (mul_mem hy hz) hy' hz' (mul_mem ..) <;> apply subset_adjoin <;> simp
  | rad n y hn hy hy' => exact induction_rad (solvableByRad.rad_mem hn hy) hn hy'
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
mem : ∀ (y : F), IsSolvable.{u_1} (Gal (minpoly.{u_1, u_2} F (B := E) ((algebraMap F E : (a : F) → E) y : E)))
add :
  ∀ (y z : E) (hy : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) y)
    (hz : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) z)
    (hy' : IsSolvable.{u_1} (Gal (minpoly F y))) (hz' : IsSolvable.{u_1} (Gal (minpoly F z))),
    IsSolvable.{u_1} (Gal (minpoly F (y + z)))
⊢ IsSolvable.{u_1} (Gal (minpoly F x))
have mul : ∀ (y z : E) (hy : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) y)
  (hz : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) z) (hy' : IsSolvable.{u_1} (Gal (minpoly F y)))
  (hz' : IsSolvable.{u_1} (Gal (minpoly F z))), IsSolvable.{u_1} (Gal (minpoly F (y * z)))
Tactic: induction hx using solvableByRad.induction with
  | mem y => rw [minpoly.eq_X_sub_C E]; infer_instance
  | add y z hy hz hy' hz' =>
    apply induction_step hy hz (add_mem hy hz) hy' hz' (add_mem ..) <;> apply subset_adjoin <;> simp
  | mul y z hy hz hy' hz' =>
    apply induction_step hy hz (mul_mem hy hz) hy' hz' (mul_mem ..) <;> apply subset_adjoin <;> simp
  | rad n y hn hy hy' => exact induction_rad (solvableByRad.rad_mem hn hy) hn hy'
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
mem : ∀ (y : F), IsSolvable.{u_1} (Gal (minpoly.{u_1, u_2} F (B := E) ((algebraMap F E : (a : F) → E) y : E)))
add :
  ∀ (y z : E) (hy : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) y)
    (hz : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) z)
    (hy' : IsSolvable.{u_1} (Gal (minpoly F y))) (hz' : IsSolvable.{u_1} (Gal (minpoly F z))),
    IsSolvable.{u_1} (Gal (minpoly F (y + z)))
mul :
  ∀ (y z : E) (hy : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) y)
    (hz : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) z)
    (hy' : IsSolvable.{u_1} (Gal (minpoly F y))) (hz' : IsSolvable.{u_1} (Gal (minpoly F z))),
    IsSolvable.{u_1} (Gal (minpoly F (y * z)))
⊢ IsSolvable.{u_1} (Gal (minpoly F x))
have rad : ∀ (n : ℕ) (y : E) (hn : n ≠ 0) (hy : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) (y ^ n))
  (hy' : IsSolvable.{u_1} (Gal (minpoly F (y ^ n)))), IsSolvable.{u_1} (Gal (minpoly F y))
Tactic: induction hx using solvableByRad.induction with
  | mem y => rw [minpoly.eq_X_sub_C E]; infer_instance
  | add y z hy hz hy' hz' =>
    apply induction_step hy hz (add_mem hy hz) hy' hz' (add_mem ..) <;> apply subset_adjoin <;> simp
  | mul y z hy hz hy' hz' =>
    apply induction_step hy hz (mul_mem hy hz) hy' hz' (mul_mem ..) <;> apply subset_adjoin <;> simp
  | rad n y hn hy hy' => exact induction_rad (solvableByRad.rad_mem hn hy) hn hy'
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
q : F[X]
q_irred : Irreducible q
q_aeval : Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) q : E) (0 : E)
⊢ IsSolvable.{u_1} (HMul.hMul (β := F[X]) q ((C : (a : F) → F[X]) q.leadingCoeff⁻¹ : F[X])).Gal
have rw : IsSolvable.{u_1} (Gal (minpoly F x))
Tactic: rw [minpoly.eq_of_irreducible q_irred q_aeval]
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (hypothesis)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
q : F[X]
q_irred : Irreducible q
q_aeval : Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) q : E) (0 : E)
⊢ IsSolvable.{u_1} q.Gal
have this : IsSolvable.{u_1} (HMul.hMul (β := F[X]) q ((C : (a : F) → F[X]) q.leadingCoeff⁻¹ : F[X])).Gal
Tactic: have : IsSolvable (q * C q.leadingCoeff⁻¹).Gal := by
    rw [minpoly.eq_of_irreducible q_irred q_aeval]
    exact isSolvable_gal_minpoly hx
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
q : F[X]
q_irred : Irreducible q
q_aeval : Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) q : E) (0 : E)
this : IsSolvable.{u_1} (HMul.hMul (β := F[X]) q ((C : (a : F) → F[X]) q.leadingCoeff⁻¹ : F[X])).Gal
⊢ IsSolvable.{u_1} q.Gal
have refine : HMul.hMul (β := F[X]) q ((C : (a : F) → F[X]) q.leadingCoeff⁻¹ : F[X]) ≠ 0
Tactic: refine solvable_of_surjective (Gal.restrictDvd_surjective ⟨C q.leadingCoeff⁻¹, rfl⟩ ?_)
-- Lean 4 proof step from Mathlib.FieldTheory.AlgebraicClosure (goal)
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
i : E →ₐ[F] K
x : E
⊢ Membership.mem (α := K) (γ := IntermediateField F K) (algebraicClosure F K) ((i : (a : E) → K) x : K) ↔
    Membership.mem (γ := IntermediateField F E) (algebraicClosure F E) x
have simp_rw : IsIntegral.{u_1, u_3} F (A := K) ((i : (a : E) → K) x : K) ↔ IsIntegral F x
Tactic: simp_rw [mem_algebraicClosure_iff', ← minpoly.ne_zero_iff, minpoly.algHom_eq i i.injective]
-- Lean 4 proof step from Mathlib.FieldTheory.AlgebraicClosure (goal)
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
i : E →ₐ[F] K
x : E
simp_rw : IsIntegral.{u_1, u_3} F (A := K) ((i : (a : E) → K) x : K) ↔ IsIntegral F x
⊢ Membership.mem (α := K) (γ := IntermediateField F K) (algebraicClosure F K) ((i : (a : E) → K) x : K) ↔
    Membership.mem (γ := IntermediateField F E) (algebraicClosure F E) x
have simp_rw₁ : Ne (α := F[X]) (minpoly.{u_1, u_3} F (B := K) ((i : (a : E) → K) x : K)) 0 ↔ Ne (α := F[X]) (minpoly F x) 0
Tactic: simp_rw [mem_algebraicClosure_iff', ← minpoly.ne_zero_iff, minpoly.algHom_eq i i.injective]
-- Lean 4 proof step from Mathlib.FieldTheory.AlgebraicClosure (goal)
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
i : E →ₐ[F] K
⊢ comap i (algebraicClosure F K) = algebraicClosure F E
have h : ∀ (x : E), x ∈ comap i (algebraicClosure F K) ↔ Membership.mem (γ := IntermediateField F E) (algebraicClosure F E) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.FieldTheory.AlgebraicClosure (goal)
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
h : Eq (α := IntermediateField E K) (algebraicClosure E K) ⊥
⊢ Eq (α := IntermediateField F K) (IntermediateField.map (IsScalarTower.toAlgHom F E K) (algebraicClosure F E))
    (algebraicClosure F K)
have refine : ∀ (x : K) (hx : Membership.mem (γ := IntermediateField F K) (algebraicClosure F K) x),
  Membership.mem (γ := IntermediateField F K)
    (IntermediateField.map (IsScalarTower.toAlgHom F E K) (algebraicClosure F E)) x
Tactic: refine le_antisymm (map_le_of_algHom _) (fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.FieldTheory.AlgebraicClosure (goal)
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
h : Eq (α := IntermediateField E K) (algebraicClosure E K) ⊥
x : K
hx : Membership.mem (γ := IntermediateField F K) (algebraicClosure F K) x
⊢ Membership.mem (γ := IntermediateField F K)
    (IntermediateField.map (IsScalarTower.toAlgHom F E K) (algebraicClosure F E)) x
have obtain : ∀ (y : E)
  (hx :
    Membership.mem (α := K) (γ := IntermediateField F K) (algebraicClosure F K) ((algebraMap E K : (a : E) → K) y : K)),
  Membership.mem (α := K) (γ := IntermediateField F K)
    (IntermediateField.map (IsScalarTower.toAlgHom F E K) (algebraicClosure F E)) ((algebraMap E K : (a : E) → K) y : K)
Tactic: obtain ⟨y, rfl⟩ := mem_bot.1 <| h ▸ mem_algebraicClosure_iff'.2
    (IsIntegral.tower_top <| mem_algebraicClosure_iff'.1 hx)
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.FieldTheory.AlgebraicClosure (goal)
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
have refine : ∀ (h : Eq (α := IntermediateField F E) (algebraicClosure F E) ⊥) (p : F[X]) (hmon : p.Monic) (hirr : Irreducible p),
  ∃ (x : F), eval x p = 0
Tactic: refine ⟨fun h ↦ IsAlgClosed.of_exists_root _ fun p hmon hirr ↦ ?_,
    fun _ ↦ IntermediateField.eq_bot_of_isAlgClosed_of_isAlgebraic _⟩
-- Lean 4 proof step from Mathlib.FieldTheory.AlgebraicClosure (goal)
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), eval x p = 0
have 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
Tactic: obtain ⟨x, hx⟩ := IsAlgClosed.exists_aeval_eq_zero E p (degree_pos_of_irreducible hirr).ne'
-- Lean 4 proof step from Mathlib.FieldTheory.AlgebraicClosure (goal)
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)
⊢ ∃ (x : F), eval x p = 0
have 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
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))
Cleared hypotheses: x, hx
-- 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
⊢ Set.SurjOn (fun (v : ι → R) (i : ι) ↦ (eval v : (a : MvPolynomial ι R) → R) (ps i)) S S
have is_int : ∀ (x : R), IsIntegral K x
Tactic: have is_int : ∀ x : R, IsIntegral K x := fun x => isAlgebraic_iff_isIntegral.1
    (alg.isAlgebraic x)
-- 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
⊢ Membership.mem (γ := Set ((i : ι) → R))
    ((fun (v : ι → R) (i : ι) ↦ (eval v : (a : MvPolynomial ι R) → R) (ps i)) '' S) v
have intro : ∀ (val : Fintype ι),
  Membership.mem (γ := Set ((i : ι) → R))
    ((fun (v : ι → R) (i : ι) ↦ (eval v : (a : MvPolynomial ι R) → R) (ps i)) '' S) v
Tactic: cases nonempty_fintype ι
-- 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
⊢ Membership.mem (γ := Set ((i : ι) → R))
    ((fun (v : ι → R) (i : ι) ↦ (eval v : (a : MvPolynomial ι R) → R) (ps i)) '' S) v
have hv : ∀ (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⟩))
-- 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)
⊢ Membership.mem (γ := Set ((i : ι) → R))
    ((fun (v : ι → R) (i : ι) ↦ (eval v : (a : MvPolynomial ι R) → R) (ps i)) '' S) v
have hs₁ : ∀ (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⟩))
-- 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))
⊢ Membership.mem (γ := Set ((i : ι) → R))
    ((fun (v : ι → R) (i : ι) ↦ (eval v : (a : MvPolynomial ι R) → R) (ps i)) '' S) v
have this : IsNoetherian.{u_2, u_3} K ↥(Algebra.adjoin K (↑s : Set R))
Tactic: have := isNoetherian_adjoin_finset s fun x _ => is_int x
-- 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 : 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
have this₁ : Finite.{u_3 + 1} ↥(Algebra.adjoin K (↑s : Set R))
Tactic: have : Finite (Algebra.adjoin K (s : Set R)) := Module.finite_of_finite K
-- 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))
          ⋯)
      ⋯
⊢ Function.Surjective res
have rw : Function.Injective res
Tactic: rw [← Finite.injective_iff_surjective]
-- 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))
          ⋯)
      ⋯
x y : (↑S' : Type (max u_1 u_3))
hxy : res x = res y
⊢ x = y
have a : ∀ (i : ι),
  (↑((↑x : ι → ↥(Algebra.adjoin K (↑s : Set R))) i) : R) = (↑((↑y : ι → ↥(Algebra.adjoin K (↑s : Set R))) i) : R)
Tactic: ext i