awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (ι →₀ ℕ)
have : ∀ {S : Set (ι → K)} (f : (ι → K) → ι → K), Set.InjOn f S ↔ ∀ (x y : ι → K), x ∈ S → y ∈ S → f x = f y → x = y
⊢ 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₁ : ∀
  (injOnAlt :
    ∀ {S : Set (ι → K)} (f : (ι → K) → ι → K), Set.InjOn f S ↔ ∀ (x y : ι → K), x ∈ S → y ∈ S → f x = f y → x = y),
  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
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]
-- Lean 4 proof step from Mathlib.FieldTheory.AxGrothendieck (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
inst : Finite α
inst_1 : Finite ι
p : ℕ
hp : Nat.Prime p
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
⊢ Theory.ACF p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons
have this : Fact (Nat.Prime p)
Tactic: have : Fact p.Prime := ⟨hp⟩
-- Lean 4 proof step from Mathlib.FieldTheory.AxGrothendieck (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Finite α
inst_1 : Finite ι
p : ℕ
hp : Nat.Prime p
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
this_1 : Fact (Nat.Prime p)
this : CompatibleRing (AlgebraicClosure (ZMod p)) := compatibleRingOfRing (AlgebraicClosure (ZMod p))
⊢ Theory.ACF p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons
have rw : ∀ (v : α → AlgebraicClosure (ZMod p))
  (p_1 : { p_1 : ι → MvPolynomial ι (AlgebraicClosure (ZMod p)) // ∀ (i : ι), (p_1 i).support ⊆ mons i }),
  have f : (ι → AlgebraicClosure (ZMod p)) → ι → AlgebraicClosure (ZMod p) :=
    fun (v : ι → AlgebraicClosure (ZMod p)) (i : ι) ↦
    ((eval v : MvPolynomial ι (AlgebraicClosure (ZMod p)) →+* AlgebraicClosure (ZMod p)) :
        (a : MvPolynomial ι (AlgebraicClosure (ZMod p))) → AlgebraicClosure (ZMod p))
      ((↑p_1 : ι → MvPolynomial ι (AlgebraicClosure (ZMod p))) i);
  have S : Set (ι → AlgebraicClosure (ZMod p)) := {x : ι → AlgebraicClosure (ZMod p) | φ.Realize (Sum.elim v x)};
  Set.MapsTo f S S → Set.InjOn f S → Set.SurjOn f S S
Tactic: rw [← (ACF_isComplete (Or.inl hp)).realize_sentence_iff _
    (AlgebraicClosure (ZMod p)), realize_genericPolyMapSurjOnOfInjOn]
-- Lean 4 proof step from Mathlib.FieldTheory.AxGrothendieck (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Finite α
inst_1 : Finite ι
p : ℕ
hp : Nat.Prime p
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
⊢ Theory.ACF p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons
have have : ∀ (this : Fact (Nat.Prime p)), Theory.ACF p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons
Tactic: classical
  have : Fact p.Prime := ⟨hp⟩
  letI := compatibleRingOfRing (AlgebraicClosure (ZMod p))
  rw [← (ACF_isComplete (Or.inl hp)).realize_sentence_iff _
    (AlgebraicClosure (ZMod p)), realize_genericPolyMapSurjOnOfInjOn]
  rintro v ⟨f, _⟩
  exact ax_grothendieck_of_locally_finite (K := ZMod p) (ι := ι) f _
-- Lean 4 proof step from Mathlib.FieldTheory.AxGrothendieck (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Finite α
inst_1 : Finite ι
p : ℕ
hp : Nat.Prime p
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
have have₁ have₂ have₃ : ∀ (this : Fact (Nat.Prime p)), Theory.ACF p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons
⊢ Theory.ACF p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons
have have₄ : ∀ (this : Fact (Nat.Prime p)),
  let this_1 : CompatibleRing (AlgebraicClosure (ZMod p)) := compatibleRingOfRing (AlgebraicClosure (ZMod p));
  ∀ (v : α → AlgebraicClosure (ZMod p))
    (p_1 : { p_1 : ι → MvPolynomial ι (AlgebraicClosure (ZMod p)) // ∀ (i : ι), (p_1 i).support ⊆ mons i }),
    have f : (ι → AlgebraicClosure (ZMod p)) → ι → AlgebraicClosure (ZMod p) :=
      fun (v : ι → AlgebraicClosure (ZMod p)) (i : ι) ↦
      ((eval v : MvPolynomial ι (AlgebraicClosure (ZMod p)) →+* AlgebraicClosure (ZMod p)) :
          (a : MvPolynomial ι (AlgebraicClosure (ZMod p))) → AlgebraicClosure (ZMod p))
        ((↑p_1 : ι → MvPolynomial ι (AlgebraicClosure (ZMod p))) i);
    have S : Set (ι → AlgebraicClosure (ZMod p)) := {x : ι → AlgebraicClosure (ZMod p) | φ.Realize (Sum.elim v x)};
    Set.MapsTo f S S → Set.InjOn f S → Set.SurjOn f S S
Tactic: classical
  have : Fact p.Prime := ⟨hp⟩
  letI := compatibleRingOfRing (AlgebraicClosure (ZMod p))
  rw [← (ACF_isComplete (Or.inl hp)).realize_sentence_iff _
    (AlgebraicClosure (ZMod p)), realize_genericPolyMapSurjOnOfInjOn]
  rintro v ⟨f, _⟩
  exact ax_grothendieck_of_locally_finite (K := ZMod p) (ι := ι) f _
-- Lean 4 proof step from Mathlib.FieldTheory.AxGrothendieck (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Finite α
inst_1 : Finite ι
p : ℕ
hp : Nat.Prime p
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
have have₁ have₂ have₃ : ∀ (this : Fact (Nat.Prime p)), Theory.ACF p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons
have₄ :
  ∀ (this : Fact (Nat.Prime p)),
    let this_1 : CompatibleRing (AlgebraicClosure (ZMod p)) := compatibleRingOfRing (AlgebraicClosure (ZMod p));
    ∀ (v : α → AlgebraicClosure (ZMod p))
      (p_1 : { p_1 : ι → MvPolynomial ι (AlgebraicClosure (ZMod p)) // ∀ (i : ι), (p_1 i).support ⊆ mons i }),
      have f : (ι → AlgebraicClosure (ZMod p)) → ι → AlgebraicClosure (ZMod p) :=
        fun (v : ι → AlgebraicClosure (ZMod p)) (i : ι) ↦
        ((eval v : MvPolynomial ι (AlgebraicClosure (ZMod p)) →+* AlgebraicClosure (ZMod p)) :
            (a : MvPolynomial ι (AlgebraicClosure (ZMod p))) → AlgebraicClosure (ZMod p))
          ((↑p_1 : ι → MvPolynomial ι (AlgebraicClosure (ZMod p))) i);
      have S : Set (ι → AlgebraicClosure (ZMod p)) := {x : ι → AlgebraicClosure (ZMod p) | φ.Realize (Sum.elim v x)};
      Set.MapsTo f S S → Set.InjOn f S → Set.SurjOn f S S
⊢ Theory.ACF p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons
have have₅ : ∀ (this : Fact (Nat.Prime p)),
  let this_1 : CompatibleRing (AlgebraicClosure (ZMod p)) := compatibleRingOfRing (AlgebraicClosure (ZMod p));
  ∀ (v : α → AlgebraicClosure (ZMod p)) (f : ι → MvPolynomial ι (AlgebraicClosure (ZMod p)))
    (property : ∀ (i : ι), (f i).support ⊆ mons i),
    have f : (ι → AlgebraicClosure (ZMod p)) → ι → AlgebraicClosure (ZMod p) :=
      fun (v : ι → AlgebraicClosure (ZMod p)) (i : ι) ↦
      ((eval v : MvPolynomial ι (AlgebraicClosure (ZMod p)) →+* AlgebraicClosure (ZMod p)) :
          (a : MvPolynomial ι (AlgebraicClosure (ZMod p))) → AlgebraicClosure (ZMod p))
        ((↑(Subtype.mk (p := fun (p_1 : ι → MvPolynomial ι (AlgebraicClosure (ZMod p))) ↦
                ∀ (i : ι), (p_1 i).support ⊆ mons i) f property) :
            ι → MvPolynomial ι (AlgebraicClosure (ZMod p)))
          i);
    have S : Set (ι → AlgebraicClosure (ZMod p)) := {x : ι → AlgebraicClosure (ZMod p) | φ.Realize (Sum.elim v x)};
    Set.MapsTo f S S → Set.InjOn f S → Set.SurjOn f S S
Tactic: classical
  have : Fact p.Prime := ⟨hp⟩
  letI := compatibleRingOfRing (AlgebraicClosure (ZMod p))
  rw [← (ACF_isComplete (Or.inl hp)).realize_sentence_iff _
    (AlgebraicClosure (ZMod p)), realize_genericPolyMapSurjOnOfInjOn]
  rintro v ⟨f, _⟩
  exact ax_grothendieck_of_locally_finite (K := ZMod p) (ι := ι) f _
-- Lean 4 proof step from Mathlib.FieldTheory.AxGrothendieck (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Finite α
inst_1 : Finite ι
p : ℕ
hp : Nat.Prime p ∨ p = 0
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
⊢ Theory.ACF p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons
have inl : ∀ (hp : Nat.Prime p), Theory.ACF p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons
Tactic: rcases hp with hp | rfl
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.FieldTheory.AxGrothendieck (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Finite α
inst_1 : Finite ι
p : ℕ
hp : Nat.Prime p ∨ p = 0
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
inl : ∀ (hp : Nat.Prime p), Theory.ACF p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons
⊢ Theory.ACF p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons
have inr : Theory.ACF 0 ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons
Tactic: rcases hp with hp | rfl
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.FieldTheory.AxGrothendieck (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Finite α
inst_1 : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
⊢ Theory.ACF 0 ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons
have inr : Set.Infinite (α := Nat.Primes) {p : Nat.Primes | Theory.ACF (↑p : ℕ) ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons}
Tactic: rw [ACF_zero_realize_iff_infinite_ACF_prime_realize]
-- Lean 4 proof step from Mathlib.FieldTheory.AxGrothendieck (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Finite α
inst_1 : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
⊢ Set.Infinite (α := Nat.Primes) {p : Nat.Primes | Theory.ACF (↑p : ℕ) ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons}
have h : Eq (α := Set Nat.Primes) {p : Nat.Primes | Theory.ACF (↑p : ℕ) ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons} Set.univ
Tactic: convert! Set.infinite_univ (α := Nat.Primes)
-- Lean 4 proof step from Mathlib.FieldTheory.AxGrothendieck (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Finite α
inst_1 : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
⊢ Eq (α := Set Nat.Primes) {p : Nat.Primes | Theory.ACF (↑p : ℕ) ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons} Set.univ
have h : ∀ (x : Nat.Primes),
  Membership.mem (γ := Set Nat.Primes) {p : Nat.Primes | Theory.ACF (↑p : ℕ) ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons} x
Tactic: rw [Set.eq_univ_iff_forall]
-- Lean 4 proof step from Mathlib.FieldTheory.AxGrothendieck (goal)
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
⊢ 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
have 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
Tactic: rw [Set.definable_iff_finitely_definable] at hS
Cleared hypotheses: hS, ps, this, p
-- Lean 4 proof step from Mathlib.FieldTheory.AxGrothendieck (goal)
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
⊢ 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
have 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
Tactic: rcases hS with ⟨c, _, hS⟩
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.FieldTheory.AxGrothendieck (hypothesis)
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
⊢ 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
have 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)}
Tactic: rw [Set.definable_iff_exists_formula_sum] at hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.FieldTheory.AxGrothendieck (goal)
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)}
⊢ 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
have 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
Tactic: rcases hS with ⟨φ, hφ⟩
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.FieldTheory.AxGrothendieck (goal)
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)}
⊢ 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
have 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)}
Tactic: rw [hφ]
-- Lean 4 proof step from Mathlib.FieldTheory.AxGrothendieck (hypothesis)
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)}
⊢ 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)}
have this₁ : 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)
-- Lean 4 proof step from Mathlib.FieldTheory.AxGrothendieck (hypothesis)
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
⊢ 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)}
have 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
Tactic: rw [← (ACF_isComplete (CharP.char_is_prime_or_zero K p)).realize_sentence_iff _ K,
    realize_genericPolyMapSurjOnOfInjOn] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.AxGrothendieck (goal)
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
⊢ 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
have 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
Tactic: obtain ⟨s, rfl⟩ : I.FG := IsNoetherian.noetherian I
Cleared hypotheses: I, S
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
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) ⋯)
⊢ 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}
have 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
Tactic: rw [← compl_setOf, nonempty_compl]
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (hypothesis)
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
⊢ False
have 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)
Tactic: simp_rw [eq_univ_iff_forall, mem_setOf] at this
Cleared hypotheses: this