awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.AxGrothendieck
Goal:
ι : Type u_1
α : Type u_2
inst : Finite α
inst_1 : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
inr : Set.Infinite (α := Nat.Primes) {p : Nat.Primes | Theory.ACF (↑p : ℕ) ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons}
⊢ Theory.ACF 0 ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons

Tactic:
rw [ACF_zero_realize_iff_infinite_ACF_prime_realize]

Premises used: FirstOrder.Field.ACF_zero_realize_iff_infinite_ACF_prime_realize
-- Module: Mathlib.FieldTheory.AxGrothendieck
Goal:
ι : Type u_1
α : Type u_2
inst : Finite α
inst_1 : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
⊢ Set.Infinite (α := Nat.Primes) Set.univ

Tactic:
Set.infinite_univ (α := Nat.Primes)

Premises used: Set.infinite_univ
-- Module: Mathlib.FieldTheory.AxGrothendieck
Goal:
ι : Type u_1
α : Type u_2
inst : Finite α
inst_1 : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
h : Eq (α := Set Nat.Primes) {p : Nat.Primes | Theory.ACF (↑p : ℕ) ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons} Set.univ
⊢ Set.Infinite (α := Nat.Primes) {p : Nat.Primes | Theory.ACF (↑p : ℕ) ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons}

Tactic:
convert! Set.infinite_univ (α := Nat.Primes)

Premises used: Set.infinite_univ
-- Module: Mathlib.FieldTheory.AxGrothendieck
Goal:
ι : Type u_1
α : Type u_2
inst : Finite α
inst_1 : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
h :
  ∀ (x : Nat.Primes),
    Membership.mem (γ := Set Nat.Primes) {p : Nat.Primes | Theory.ACF (↑p : ℕ) ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons} x
⊢ Eq (α := Set Nat.Primes) {p : Nat.Primes | Theory.ACF (↑p : ℕ) ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons} Set.univ

Tactic:
rw [Set.eq_univ_iff_forall]

Premises used: Set.eq_univ_iff_forall
-- Module: Mathlib.FieldTheory.AxGrothendieck
Goal:
ι : Type u_1
α : Type u_2
inst : Finite α
inst_1 : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
p : ℕ
hp : Nat.Prime p
⊢ Membership.mem (γ := Set Nat.Primes) {p : Nat.Primes | Theory.ACF (↑p : ℕ) ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons}
    (Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) p hp)

Tactic:
ACF_models_genericPolyMapSurjOnOfInjOn_of_prime hp φ mons

Premises used: FirstOrder.ACF_models_genericPolyMapSurjOnOfInjOn_of_prime, Set.Mem, setOf, FirstOrder.Language.Theory.ModelsBoundedFormula
-- Module: Mathlib.FieldTheory.AxGrothendieck
Goal:
ι : Type u_1
α : Type u_2
inst : Finite α
inst_1 : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
p : ℕ
hp : Nat.Prime p
⊢ Membership.mem (γ := Set Nat.Primes) {p : Nat.Primes | Theory.ACF (↑p : ℕ) ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons}
    (Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) p hp)

Tactic:
exact ACF_models_genericPolyMapSurjOnOfInjOn_of_prime hp φ mons

Premises used: FirstOrder.ACF_models_genericPolyMapSurjOnOfInjOn_of_prime
-- Module: Mathlib.FieldTheory.AxGrothendieck
Goal:
K : Type u_1
ι : Type u_2
inst : Field K
inst_1 : IsAlgClosed K
inst_2 : Finite ι
inst_3 : CompatibleRing K
c : Set K
S : Set (ι → K)
hS : c.Definable ring S
ps : ι → MvPolynomial ι K
this : Fintype ι := Fintype.ofFinite ι
p : ℕ := ringChar K
rw :
  ∀ (hS : ∃ (A0 : Finset K), (↑A0 : Set K) ⊆ c ∧ (↑A0 : Set K).Definable ring S) (ps : ι → MvPolynomial ι K),
    Set.MapsTo (fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (ps i)) S S →
      Set.InjOn (β := (i : ι) → K) (fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (ps i)) S →
        Set.SurjOn (fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (ps i)) S S
⊢ Set.MapsTo (fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (ps i)) S S →
    Set.InjOn (β := (i : ι) → K) (fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (ps i)) S →
      Set.SurjOn (fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (ps i)) S S

Tactic:
rw [Set.definable_iff_finitely_definable] at hS

Premises used: Set.definable_iff_finitely_definable
-- Module: Mathlib.FieldTheory.AxGrothendieck
Goal:
K : Type u_1
ι : Type u_2
inst : Field K
inst_1 : IsAlgClosed K
inst_2 : Finite ι
inst_3 : CompatibleRing K
c : Set K
S : Set (ι → K)
hS : ∃ (A0 : Finset K), (↑A0 : Set K) ⊆ c ∧ (↑A0 : Set K).Definable ring S
ps : ι → MvPolynomial ι K
this : Fintype ι := Fintype.ofFinite ι
p : ℕ := ringChar K
rcases :
  ∀ (c_1 : Finset K),
    (↑c_1 : Set K) ⊆ c →
      ∀ (hS : (↑c_1 : Set K).Definable ring S),
        Set.MapsTo (fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (ps i)) S S →
          Set.InjOn (β := (i : ι) → K) (fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (ps i)) S →
            Set.SurjOn (fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (ps i)) S S
⊢ Set.MapsTo (fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (ps i)) S S →
    Set.InjOn (β := (i : ι) → K) (fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (ps i)) S →
      Set.SurjOn (fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (ps i)) S S

Tactic:
rcases hS with ⟨c, _, hS⟩
-- Module: Mathlib.FieldTheory.AxGrothendieck
Goal:
K : Type u_1
ι : Type u_2
inst : Field K
inst_1 : IsAlgClosed K
inst_2 : Finite ι
inst_3 : CompatibleRing K
c_1 : Set K
S : Set (ι → K)
ps : ι → MvPolynomial ι K
this : Fintype ι := Fintype.ofFinite ι
p : ℕ := ringChar K
c : Finset K
left : (↑c : Set K) ⊆ c_1
hS : (↑c : Set K).Definable ring S
⊢ ∃ (φ : ring.Formula (Sum.{u_1, u_2} (↑(↑c : Set K) : Type u_1) ι)),
    S = {v : ι → K | φ.Realize (Sum.elim (Subtype.val (p := fun (x : K) ↦ x ∈ (↑c : Set K))) v)}

Tactic:
rw [Set.definable_iff_exists_formula_sum] at hS

Premises used: Set.definable_iff_exists_formula_sum
-- Module: Mathlib.FieldTheory.AxGrothendieck
Goal:
K : Type u_1
ι : Type u_2
inst : Field K
inst_1 : IsAlgClosed K
inst_2 : Finite ι
inst_3 : CompatibleRing K
c_1 : Set K
S : Set (ι → K)
ps : ι → MvPolynomial ι K
this : Fintype ι := Fintype.ofFinite ι
p : ℕ := ringChar K
c : Finset K
left : (↑c : Set K) ⊆ c_1
hS :
  ∃ (φ : ring.Formula (Sum.{u_1, u_2} (↑(↑c : Set K) : Type u_1) ι)),
    S = {v : ι → K | φ.Realize (Sum.elim (Subtype.val (p := fun (x : K) ↦ x ∈ (↑c : Set K))) v)}
rcases :
  ∀ (φ : ring.Formula (Sum.{u_1, u_2} (↑(↑c : Set K) : Type u_1) ι))
    (hφ : S = {v : ι → K | φ.Realize (Sum.elim (Subtype.val (p := fun (x : K) ↦ x ∈ (↑c : Set K))) v)}),
    Set.MapsTo (fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (ps i)) S S →
      Set.InjOn (β := (i : ι) → K) (fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (ps i)) S →
        Set.SurjOn (fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (ps i)) S S
⊢ Set.MapsTo (fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (ps i)) S S →
    Set.InjOn (β := (i : ι) → K) (fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (ps i)) S →
      Set.SurjOn (fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (ps i)) S S

Tactic:
rcases hS with ⟨φ, hφ⟩
-- Module: Mathlib.FieldTheory.AxGrothendieck
Goal:
K : Type u_1
ι : Type u_2
inst : Field K
inst_1 : IsAlgClosed K
inst_2 : Finite ι
inst_3 : CompatibleRing K
c_1 : Set K
S : Set (ι → K)
ps : ι → MvPolynomial ι K
this : Fintype ι := Fintype.ofFinite ι
p : ℕ := ringChar K
c : Finset K
left : (↑c : Set K) ⊆ c_1
φ : ring.Formula (Sum.{u_1, u_2} (↑(↑c : Set K) : Type u_1) ι)
hφ : S = {v : ι → K | φ.Realize (Sum.elim (Subtype.val (p := fun (x : K) ↦ x ∈ (↑c : Set K))) v)}
rw :
  Set.MapsTo (β := (i : ι) → K) (fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (ps i))
      {v : ι → K | φ.Realize (Sum.elim (Subtype.val (p := fun (x : K) ↦ x ∈ (↑c : Set K))) v)}
      {v : ι → K | φ.Realize (Sum.elim (Subtype.val (p := fun (x : K) ↦ x ∈ (↑c : Set K))) v)} →
    Set.InjOn (β := (i : ι) → K) (fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (ps i))
        {v : ι → K | φ.Realize (Sum.elim (Subtype.val (p := fun (x : K) ↦ x ∈ (↑c : Set K))) v)} →
      Set.SurjOn (β := (i : ι) → K) (fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (ps i))
        {v : ι → K | φ.Realize (Sum.elim (Subtype.val (p := fun (x : K) ↦ x ∈ (↑c : Set K))) v)}
        {v : ι → K | φ.Realize (Sum.elim (Subtype.val (p := fun (x : K) ↦ x ∈ (↑c : Set K))) v)}
⊢ Set.MapsTo (fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (ps i)) S S →
    Set.InjOn (β := (i : ι) → K) (fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (ps i)) S →
      Set.SurjOn (fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (ps i)) S S

Tactic:
rw [hφ]
-- Module: Mathlib.FieldTheory.AxGrothendieck
Goal:
K : Type u_1
ι : Type u_2
inst : Field K
inst_1 : IsAlgClosed K
inst_2 : Finite ι
inst_3 : CompatibleRing K
c_1 : Set K
S : Set (ι → K)
ps : ι → MvPolynomial ι K
this : Fintype ι := Fintype.ofFinite ι
p : ℕ := ringChar K
c : Finset K
left : (↑c : Set K) ⊆ c_1
φ : ring.Formula (Sum.{u_1, u_2} (↑(↑c : Set K) : Type u_1) ι)
hφ : S = {v : ι → K | φ.Realize (Sum.elim (Subtype.val (p := fun (x : K) ↦ x ∈ (↑c : Set K))) v)}
⊢ Theory.ACF p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ fun (i : ι) ↦ (ps i).support

Tactic:
have := ACF_models_genericPolyMapSurjOnOfInjOn_of_prime_or_zero
    (CharP.char_is_prime_or_zero K p) φ (fun i => (ps i).support)
-- Module: Mathlib.FieldTheory.AxGrothendieck
Goal:
K : Type u_1
ι : Type u_2
inst : Field K
inst_1 : IsAlgClosed K
inst_2 : Finite ι
inst_3 : CompatibleRing K
c_1 : Set K
S : Set (ι → K)
ps : ι → MvPolynomial ι K
this_1 : Fintype ι := Fintype.ofFinite ι
p : ℕ := ringChar K
c : Finset K
left : (↑c : Set K) ⊆ c_1
φ : ring.Formula (Sum.{u_1, u_2} (↑(↑c : Set K) : Type u_1) ι)
hφ : S = {v : ι → K | φ.Realize (Sum.elim (Subtype.val (p := fun (x : K) ↦ x ∈ (↑c : Set K))) v)}
this : Theory.ACF p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ fun (i : ι) ↦ (ps i).support
⊢ ∀ (v : (↑(↑c : Set K) : Type u_1) → K)
    (p : { p : ι → MvPolynomial ι K // ∀ (i : ι), (p i).support ⊆ (ps i).support }),
    have f : (ι → K) → ι → K := fun (v : ι → K) (i : ι) ↦
      (eval v : (a : MvPolynomial ι K) → K) ((↑p : ι → MvPolynomial ι K) i);
    have S : Set (ι → K) := {x : ι → K | φ.Realize (Sum.elim v x)};
    Set.MapsTo f S S → Set.InjOn f S → Set.SurjOn f S S

Tactic:
rw [← (ACF_isComplete (CharP.char_is_prime_or_zero K p)).realize_sentence_iff _ K,
    realize_genericPolyMapSurjOnOfInjOn] at this

Premises used: CharP.char_is_prime_or_zero, FirstOrder.realize_genericPolyMapSurjOnOfInjOn, FirstOrder.Language.Theory.IsComplete.realize_sentence_iff, FirstOrder.Field.ACF_isComplete
-- Module: Mathlib.FieldTheory.AxGrothendieck
Goal:
K : Type u_1
ι : Type u_2
inst : Field K
inst_1 : IsAlgClosed K
inst_2 : Finite ι
inst_3 : CompatibleRing K
c_1 : Set K
S : Set (ι → K)
ps : ι → MvPolynomial ι K
this_1 : Fintype ι := Fintype.ofFinite ι
p : ℕ := ringChar K
c : Finset K
left : (↑c : Set K) ⊆ c_1
φ : ring.Formula (Sum.{u_1, u_2} (↑(↑c : Set K) : Type u_1) ι)
hφ : S = {v : ι → K | φ.Realize (Sum.elim (Subtype.val (p := fun (x : K) ↦ x ∈ (↑c : Set K))) v)}
this :
  ∀ (v : (↑(↑c : Set K) : Type u_1) → K)
    (p : { p : ι → MvPolynomial ι K // ∀ (i : ι), (p i).support ⊆ (ps i).support }),
    have f : (ι → K) → ι → K := fun (v : ι → K) (i : ι) ↦
      (eval v : (a : MvPolynomial ι K) → K) ((↑p : ι → MvPolynomial ι K) i);
    have S : Set (ι → K) := {x : ι → K | φ.Realize (Sum.elim v x)};
    Set.MapsTo f S S → Set.InjOn f S → Set.SurjOn f S S
⊢ Set.MapsTo (β := (i : ι) → K) (fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (ps i))
      {v : ι → K | φ.Realize (Sum.elim (Subtype.val (p := fun (x : K) ↦ x ∈ (↑c : Set K))) v)}
      {v : ι → K | φ.Realize (Sum.elim (Subtype.val (p := fun (x : K) ↦ x ∈ (↑c : Set K))) v)} →
    Set.InjOn (β := (i : ι) → K) (fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (ps i))
        {v : ι → K | φ.Realize (Sum.elim (Subtype.val (p := fun (x : K) ↦ x ∈ (↑c : Set K))) v)} →
      Set.SurjOn (β := (i : ι) → K) (fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (ps i))
        {v : ι → K | φ.Realize (Sum.elim (Subtype.val (p := fun (x : K) ↦ x ∈ (↑c : Set K))) v)}
        {v : ι → K | φ.Realize (Sum.elim (Subtype.val (p := fun (x : K) ↦ x ∈ (↑c : Set K))) v)}

Tactic:
this Subtype.val ⟨ps, fun i => Set.Subset.refl _⟩

Premises used: Set.Subset.refl, MvPolynomial.support, Subtype.mk, SetLike.coe, Subtype.val
-- Module: Mathlib.FieldTheory.AxGrothendieck
Goal:
K : Type u_1
ι : Type u_2
inst : Field K
inst_1 : IsAlgClosed K
inst_2 : Finite ι
inst_3 : CompatibleRing K
c_1 : Set K
S : Set (ι → K)
ps : ι → MvPolynomial ι K
this_1 : Fintype ι := Fintype.ofFinite ι
p : ℕ := ringChar K
c : Finset K
left : (↑c : Set K) ⊆ c_1
φ : ring.Formula (Sum.{u_1, u_2} (↑(↑c : Set K) : Type u_1) ι)
hφ : S = {v : ι → K | φ.Realize (Sum.elim (Subtype.val (p := fun (x : K) ↦ x ∈ (↑c : Set K))) v)}
this :
  ∀ (v : (↑(↑c : Set K) : Type u_1) → K)
    (p : { p : ι → MvPolynomial ι K // ∀ (i : ι), (p i).support ⊆ (ps i).support }),
    have f : (ι → K) → ι → K := fun (v : ι → K) (i : ι) ↦
      (eval v : (a : MvPolynomial ι K) → K) ((↑p : ι → MvPolynomial ι K) i);
    have S : Set (ι → K) := {x : ι → K | φ.Realize (Sum.elim v x)};
    Set.MapsTo f S S → Set.InjOn f S → Set.SurjOn f S S
⊢ Set.MapsTo (β := (i : ι) → K) (fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (ps i))
      {v : ι → K | φ.Realize (Sum.elim (Subtype.val (p := fun (x : K) ↦ x ∈ (↑c : Set K))) v)}
      {v : ι → K | φ.Realize (Sum.elim (Subtype.val (p := fun (x : K) ↦ x ∈ (↑c : Set K))) v)} →
    Set.InjOn (β := (i : ι) → K) (fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (ps i))
        {v : ι → K | φ.Realize (Sum.elim (Subtype.val (p := fun (x : K) ↦ x ∈ (↑c : Set K))) v)} →
      Set.SurjOn (β := (i : ι) → K) (fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (ps i))
        {v : ι → K | φ.Realize (Sum.elim (Subtype.val (p := fun (x : K) ↦ x ∈ (↑c : Set K))) v)}
        {v : ι → K | φ.Realize (Sum.elim (Subtype.val (p := fun (x : K) ↦ x ∈ (↑c : Set K))) v)}

Tactic:
exact this Subtype.val ⟨ps, fun i => Set.Subset.refl _⟩

Premises used: Set.Subset.refl, MvPolynomial.support, Subtype.mk, SetLike.coe, Subtype.val
-- Module: Mathlib.FieldTheory.AxGrothendieck
Goal:
K : Type u_1
ι : Type u_2
inst : Field K
inst_1 : IsAlgClosed K
inst_2 : Finite ι
I : Ideal (MvPolynomial ι K)
p : ι → MvPolynomial ι K
this : CompatibleRing K := compatibleRingOfRing K
S : Set (ι → K) := zeroLocus K I
⊢ I.FG

Tactic:
IsNoetherian.noetherian I

Premises used: IsNoetherian.noetherian, Submodule.FG, Ideal.FG
-- Module: Mathlib.FieldTheory.AxGrothendieck
Goal:
K : Type u_1
ι : Type u_2
inst : Field K
inst_1 : IsAlgClosed K
inst_2 : Finite ι
I : Ideal (MvPolynomial ι K)
p : ι → MvPolynomial ι K
this : CompatibleRing K := compatibleRingOfRing K
S : Set (ι → K) := zeroLocus K I
obtain :
  ∀ (s : Finset (MvPolynomial ι K)),
    let S := zeroLocus K (Ideal.span (↑s : Set (MvPolynomial ι K)));
    Set.MapsTo (fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (p i)) S S →
      Set.InjOn (β := (i : ι) → K) (fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (p i)) S →
        Set.SurjOn (fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (p i)) S S
⊢ Set.MapsTo (fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (p i)) S S →
    Set.InjOn (β := (i : ι) → K) (fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (p i)) S →
      Set.SurjOn (fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (p i)) S S

Tactic:
obtain ⟨s, rfl⟩ : I.FG := IsNoetherian.noetherian I

Premises used: IsNoetherian.noetherian, Ideal.FG, rfl
-- Module: Mathlib.FieldTheory.AxGrothendieck
Goal:
K : Type u_1
ι : Type u_2
inst : Field K
inst_1 : IsAlgClosed K
inst_2 : Finite ι
p : ι → MvPolynomial ι K
this : CompatibleRing K := compatibleRingOfRing K
s : Finset (MvPolynomial ι K)
S : Set (ι → K) := zeroLocus K (Ideal.span (↑s : Set (MvPolynomial ι K)))
⊢ Set.MapsTo (fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (p i)) S S →
    Set.InjOn (β := (i : ι) → K) (fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (p i)) S →
      Set.SurjOn (fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (p i)) S S

Tactic:
ax_grothendieck_of_definable S (mvPolynomial_zeroLocus_definable s) p

Premises used: ax_grothendieck_of_definable, FirstOrder.Ring.mvPolynomial_zeroLocus_definable
-- Module: Mathlib.FieldTheory.AxGrothendieck
Goal:
K : Type u_1
ι : Type u_2
inst : Field K
inst_1 : IsAlgClosed K
inst_2 : Finite ι
p : ι → MvPolynomial ι K
this : CompatibleRing K := compatibleRingOfRing K
s : Finset (MvPolynomial ι K)
S : Set (ι → K) := zeroLocus K (Ideal.span (↑s : Set (MvPolynomial ι K)))
⊢ Set.MapsTo (fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (p i)) S S →
    Set.InjOn (β := (i : ι) → K) (fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (p i)) S →
      Set.SurjOn (fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (p i)) S S

Tactic:
exact ax_grothendieck_of_definable S (mvPolynomial_zeroLocus_definable s) p

Premises used: ax_grothendieck_of_definable, FirstOrder.Ring.mvPolynomial_zeroLocus_definable
-- Module: Mathlib.FieldTheory.AxGrothendieck
Goal:
K : Type u_1
ι : Type u_2
inst : Field K
inst_1 : IsAlgClosed K
inst_2 : Finite ι
p : ι → MvPolynomial ι K
⊢ (Function.Injective (β := (i : ι) → K) fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (p i)) →
    Function.Surjective (β := (i : ι) → K) fun (v : ι → K) (i : ι) ↦ (eval v : (a : MvPolynomial ι K) → K) (p i)

Tactic:
simpa using ax_grothendieck_zeroLocus 0 p

Premises used: OfNat.ofNat, ax_grothendieck_zeroLocus
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
⊢ Eq.{v + 1} (α := IntermediateField F E)
    (adjoin F (range («ι» := (Module.rank F E).ord.ToType) (⇑b : (a : (Module.rank F E).ord.ToType) → E))) ⊤

Tactic:
toSubalgebra_injective <| Subalgebra.toSubmodule_injective <| top_unique <|
    (Basis.span_eq b).ge.trans <| (Algebra.span_le_adjoin F _).trans <| algebra_adjoin_le_adjoin _ _

Premises used: Subalgebra.toSubmodule_injective, Eq.ge, Algebra.span_le_adjoin, Field.Emb.Cardinal.wellOrderedBasis, IntermediateField.toSubalgebra_injective, top_unique, LE.le.trans, Module.Basis.span_eq, IntermediateField.algebra_adjoin_le_adjoin
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
⊢ NoMaxOrder.{v} (Module.rank F E).ord.ToType

Tactic:
Cardinal.noMaxOrder Fact.out

Premises used: Cardinal.noMaxOrder, Fact.out
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
ih : (y : (Module.rank F E).ord.ToType) → y < i → (Module.rank F E).ord.ToType
s : Set E :=
  range fun (j : (↑(Iio i) : Type v)) ↦
    (b : (a : (Module.rank F E).ord.ToType) → E) (ih (↑j : (Module.rank F E).ord.ToType) ⋯)
rw :
  Ne.{v + 1} (α := Set (Module.rank F E).ord.ToType)
    {a : (Module.rank F E).ord.ToType |
      Membership.mem (α := E) (γ := IntermediateField F E) (adjoin F s)
        ((b : (a : (Module.rank F E).ord.ToType) → E) a : E)}
    Set.univ
⊢ Set.Nonempty.{v} (α := (Module.rank F E).ord.ToType)
    {k : (Module.rank F E).ord.ToType | ((b : (a : (Module.rank F E).ord.ToType) → E) k : E) ∉ adjoin F s}

Tactic:
rw [← compl_setOf, nonempty_compl]

Premises used: Set.nonempty_compl, Set.compl_setOf
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
ih : (y : (Module.rank F E).ord.ToType) → y < i → (Module.rank F E).ord.ToType
s : Set E :=
  range fun (j : (↑(Iio i) : Type v)) ↦
    (b : (a : (Module.rank F E).ord.ToType) → E) (ih (↑j : (Module.rank F E).ord.ToType) ⋯)
by_contra! :
  ∀
    (this :
      Eq.{v + 1} (α := Set (Module.rank F E).ord.ToType)
        {a : (Module.rank F E).ord.ToType |
          Membership.mem (α := E) (γ := IntermediateField F E) (adjoin F s)
            ((b : (a : (Module.rank F E).ord.ToType) → E) a : E)}
        Set.univ),
    False
⊢ Ne.{v + 1} (α := Set (Module.rank F E).ord.ToType)
    {a : (Module.rank F E).ord.ToType |
      Membership.mem (α := E) (γ := IntermediateField F E) (adjoin F s)
        ((b : (a : (Module.rank F E).ord.ToType) → E) a : E)}
    Set.univ

Tactic:
by_contra!
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
ih : (y : (Module.rank F E).ord.ToType) → y < i → (Module.rank F E).ord.ToType
s : Set E :=
  range fun (j : (↑(Iio i) : Type v)) ↦
    (b : (a : (Module.rank F E).ord.ToType) → E) (ih (↑j : (Module.rank F E).ord.ToType) ⋯)
this :
  Eq.{v + 1} (α := Set (Module.rank F E).ord.ToType)
    {a : (Module.rank F E).ord.ToType |
      Membership.mem (α := E) (γ := IntermediateField F E) (adjoin F s)
        ((b : (a : (Module.rank F E).ord.ToType) → E) a : E)}
    Set.univ
⊢ ∀ (x : (Module.rank F E).ord.ToType),
    Membership.mem (α := E) (γ := IntermediateField F E) (adjoin F s)
      ((b : (a : (Module.rank F E).ord.ToType) → E) x : E)

Tactic:
simp_rw [eq_univ_iff_forall, mem_setOf] at this

Premises used: Set.eq_univ_iff_forall, Set.mem_setOf
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
ih : (y : (Module.rank F E).ord.ToType) → y < i → (Module.rank F E).ord.ToType
s : Set E :=
  range fun (j : (↑(Iio i) : Type v)) ↦
    (b : (a : (Module.rank F E).ord.ToType) → E) (ih (↑j : (Module.rank F E).ord.ToType) ⋯)
this :
  ∀ (x : (Module.rank F E).ord.ToType),
    Membership.mem (α := E) (γ := IntermediateField F E) (adjoin F s)
      ((b : (a : (Module.rank F E).ord.ToType) → E) x : E)
⊢ LE.le (α := IntermediateField F E)
    (adjoin F (range («ι» := (Module.rank F E).ord.ToType) (⇑b : (a : (Module.rank F E).ord.ToType) → E))) (adjoin F s)

Tactic:
have := adjoin_le_iff.mpr (range_subset_iff.mpr this)
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
ih : (y : (Module.rank F E).ord.ToType) → y < i → (Module.rank F E).ord.ToType
s : Set E :=
  range fun (j : (↑(Iio i) : Type v)) ↦
    (b : (a : (Module.rank F E).ord.ToType) → E) (ih (↑j : (Module.rank F E).ord.ToType) ⋯)
this_1 :
  ∀ (x : (Module.rank F E).ord.ToType),
    Membership.mem (α := E) (γ := IntermediateField F E) (adjoin F s)
      ((b : (a : (Module.rank F E).ord.ToType) → E) x : E)
this :
  LE.le (α := IntermediateField F E)
    (adjoin F (range («ι» := (Module.rank F E).ord.ToType) (⇑b : (a : (Module.rank F E).ord.ToType) → E))) (adjoin F s)
⊢ Eq (α := IntermediateField F E) (adjoin F s) ⊤

Tactic:
rw [adjoin_basis_eq_top, ← eq_top_iff] at this

Premises used: eq_top_iff, Field.Emb.Cardinal.adjoin_basis_eq_top
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
ih : (y : (Module.rank F E).ord.ToType) → y < i → (Module.rank F E).ord.ToType
s : Set E :=
  range fun (j : (↑(Iio i) : Type v)) ↦
    (b : (a : (Module.rank F E).ord.ToType) → E) (ih (↑j : (Module.rank F E).ord.ToType) ⋯)
this_1 :
  ∀ (x : (Module.rank F E).ord.ToType),
    Membership.mem (α := E) (γ := IntermediateField F E) (adjoin F s)
      ((b : (a : (Module.rank F E).ord.ToType) → E) x : E)
this : Eq (α := IntermediateField F E) (adjoin F s) ⊤
⊢ Module.rank F ↥(adjoin F s) = Module.rank F ↥⊤

Tactic:
apply_fun Module.rank F at this

Premises used: Module.rank