awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
          ⋯)
      ⋯
⊢ Function.Surjective res

Tactic:
have hres_surj : Function.Surjective res := by
    rw [← Finite.injective_iff_surjective]
    intro x y hxy
    ext i
    simp only [Subtype.ext_iff, funext_iff] at hxy
    exact congr_fun (hinj x.2 y.2 (funext hxy)) i
-- 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))
          ⋯)
      ⋯
hres_surj : Function.Surjective res
intro :
  ∀ (w : ι → ↥(Algebra.adjoin K (↑s : Set R))) (hwS' : w ∈ S')
    (hw :
      res (Subtype.mk (p := fun (x : ι → ↥(Algebra.adjoin K (↑s : Set R))) ↦ x ∈ S') w hwS') =
        Subtype.mk (p := fun (x : ι → ↥(Algebra.adjoin K (↑s : Set R))) ↦ x ∈ S')
          (fun (i : ι) ↦
            Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subalgebra K R) (Algebra.adjoin K (↑s : Set R)) x) (v i)
              ⋯)
          hvS),
    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:
rcases hres_surj ⟨fun i => ⟨v i, hv i⟩, hvS⟩ with ⟨⟨w, hwS'⟩, hw⟩

Premises used: Subtype.mk
-- 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))
          ⋯)
      ⋯
hres_surj : Function.Surjective res
w : ι → ↥(Algebra.adjoin K (↑s : Set R))
hwS' : w ∈ S'
hw :
  res (Subtype.mk (p := fun (x : ι → ↥(Algebra.adjoin K (↑s : Set R))) ↦ x ∈ S') w hwS') =
    Subtype.mk (p := fun (x : ι → ↥(Algebra.adjoin K (↑s : Set R))) ↦ x ∈ S')
      (fun (i : ι) ↦
        Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subalgebra K R) (Algebra.adjoin K (↑s : Set R)) x) (v i) ⋯)
      hvS
⊢ Membership.mem (γ := Set ((i : ι) → R))
    ((fun (v : ι → R) (i : ι) ↦ (eval v : (a : MvPolynomial ι R) → R) (ps i)) '' S) v

Tactic:
⟨fun i => w i, hwS', ?_⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, Subtype.val
-- 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))
          ⋯)
      ⋯
hres_surj : Function.Surjective res
w : ι → ↥(Algebra.adjoin K (↑s : Set R))
hwS' : w ∈ S'
hw :
  res (Subtype.mk (p := fun (x : ι → ↥(Algebra.adjoin K (↑s : Set R))) ↦ x ∈ S') w hwS') =
    Subtype.mk (p := fun (x : ι → ↥(Algebra.adjoin K (↑s : Set R))) ↦ x ∈ S')
      (fun (i : ι) ↦
        Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subalgebra K R) (Algebra.adjoin K (↑s : Set R)) x) (v i) ⋯)
      hvS
intro : ((fun (v : ι → R) (i : ι) ↦ ((eval v : (a : MvPolynomial ι R) → R) (ps i) : R)) fun (i : ι) ↦ (↑(w i) : R)) = v
⊢ Membership.mem (γ := Set ((i : ι) → R))
    ((fun (v : ι → R) (i : ι) ↦ (eval v : (a : MvPolynomial ι R) → R) (ps i)) '' S) v

Tactic:
refine ⟨fun i => w i, hwS', ?_⟩
-- 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))
          ⋯)
      ⋯
hres_surj : Function.Surjective res
w : ι → ↥(Algebra.adjoin K (↑s : Set R))
hwS' : w ∈ S'
hw :
  res (Subtype.mk (p := fun (x : ι → ↥(Algebra.adjoin K (↑s : Set R))) ↦ x ∈ S') w hwS') =
    Subtype.mk (p := fun (x : ι → ↥(Algebra.adjoin K (↑s : Set R))) ↦ x ∈ S')
      (fun (i : ι) ↦
        Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subalgebra K R) (Algebra.adjoin K (↑s : Set R)) x) (v i) ⋯)
      hvS
⊢ ((fun (v : ι → R) (i : ι) ↦ ((eval v : (a : MvPolynomial ι R) → R) (ps i) : R)) fun (i : ι) ↦ (↑(w i) : R)) = v

Tactic:
simpa [Subtype.ext_iff, funext_iff] using hw

Premises used: funext_iff, Subtype.ext_iff
-- Module: Mathlib.FieldTheory.AxGrothendieck
Goal:
ι : Type u_1
α : Type u_2
inst : Finite α
K : Type u_3
inst_1 : Field K
inst_2 : CompatibleRing K
inst_3 : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
tauto tauto₁ :
  ∀ {S : Set (ι → K)} (f : (ι → K) → ι → K),
    (∀ ⦃x₁ : ι → K⦄, x₁ ∈ S → ∀ ⦃x₂ : ι → K⦄, x₂ ∈ S → f x₁ = f x₂ → x₁ = x₂) ↔
      ∀ (x y : ι → K), x ∈ S → y ∈ S → f x = f y → x = y
mp :
  ∀ {S : Set (ι → K)} (f : (ι → K) → ι → K),
    (∀ ⦃x₁ : ι → K⦄, x₁ ∈ S → ∀ ⦃x₂ : ι → K⦄, x₂ ∈ S → f x₁ = f x₂ → x₁ = x₂) →
      ∀ (x y : ι → K), x ∈ S → y ∈ S → f x = f y → x = y
mpr :
  ∀ {S : Set (ι → K)} (f : (ι → K) → ι → K),
    (∀ (x y : ι → K), x ∈ S → y ∈ S → f x = f y → x = y) →
      ∀ ⦃x₁ : ι → K⦄, x₁ ∈ S → ∀ ⦃x₂ : ι → K⦄, x₂ ∈ S → f x₁ = f x₂ → x₁ = x₂
mp₁ mp₂ mp₃ :
  ∀ {S : Set (ι → K)} (f : (ι → K) → ι → K),
    (∀ ⦃x₁ : ι → K⦄, x₁ ∈ S → ∀ ⦃x₂ : ι → K⦄, x₂ ∈ S → f x₁ = f x₂ → x₁ = x₂) →
      ∀ (x y : ι → K), x ∈ S → y ∈ S → f x = f y → x = y
mpr₁ mpr₂ mpr₃ :
  ∀ {S : Set (ι → K)} (f : (ι → K) → ι → K),
    (∀ (x y : ι → K), x ∈ S → y ∈ S → f x = f y → x = y) →
      ∀ ⦃x₁ : ι → K⦄, x₁ ∈ S → ∀ ⦃x₂ : ι → K⦄, x₂ ∈ S → f x₁ = f x₂ → x₁ = x₂
mp₄ mp₅ mp₆ :
  ∀ {S : Set (ι → K)} (f : (ι → K) → ι → K),
    (∀ ⦃x₁ : ι → K⦄, x₁ ∈ S → ∀ ⦃x₂ : ι → K⦄, x₂ ∈ S → f x₁ = f x₂ → x₁ = x₂) →
      ∀ (x y : ι → K), x ∈ S → y ∈ S → f x = f y → x = y
mpr₄ mpr₅ mpr₆ :
  ∀ {S : Set (ι → K)} (f : (ι → K) → ι → K),
    (∀ (x y : ι → K), x ∈ S → y ∈ S → f x = f y → x = y) →
      ∀ ⦃x₁ : ι → K⦄, x₁ ∈ S → ∀ ⦃x₂ : ι → K⦄, x₂ ∈ S → f x₁ = f x₂ → x₁ = x₂
mp₇ mp₈ mp₉ :
  ∀ {S : Set (ι → K)} (f : (ι → K) → ι → K),
    (∀ ⦃x₁ : ι → K⦄, x₁ ∈ S → ∀ ⦃x₂ : ι → K⦄, x₂ ∈ S → f x₁ = f x₂ → x₁ = x₂) →
      ∀ (x y : ι → K), x ∈ S → y ∈ S → f x = f y → x = y
mpr₇ mpr₈ mpr₉ :
  ∀ {S : Set (ι → K)} (f : (ι → K) → ι → K),
    (∀ (x y : ι → K), x ∈ S → y ∈ S → f x = f y → x = y) →
      ∀ ⦃x₁ : ι → K⦄, x₁ ∈ S → ∀ ⦃x₂ : ι → K⦄, x₂ ∈ S → f x₁ = f x₂ → x₁ = x₂
mp₁₀ mp₁₁ mp₁₂ :
  ∀ {S : Set (ι → K)} (f : (ι → K) → ι → K),
    (∀ ⦃x₁ : ι → K⦄, x₁ ∈ S → ∀ ⦃x₂ : ι → K⦄, x₂ ∈ S → f x₁ = f x₂ → x₁ = x₂) →
      ∀ (x y : ι → K), x ∈ S → y ∈ S → f x = f y → x = y
mpr₁₀ mpr₁₁ mpr₁₂ :
  ∀ {S : Set (ι → K)} (f : (ι → K) → ι → K),
    (∀ (x y : ι → K), x ∈ S → y ∈ S → f x = f y → x = y) →
      ∀ ⦃x₁ : ι → K⦄, x₁ ∈ S → ∀ ⦃x₂ : ι → K⦄, x₂ ∈ S → f x₁ = f x₂ → x₁ = x₂
mp₁₃ mp₁₄ :
  ∀ {S : Set (ι → K)} (f : (ι → K) → ι → K),
    (∀ ⦃x₁ : ι → K⦄, x₁ ∈ S → ∀ ⦃x₂ : ι → K⦄, x₂ ∈ S → f x₁ = f x₂ → x₁ = x₂) →
      ∀ (x y : ι → K), x ∈ S → y ∈ S → f x = f y → x = y
mpr₁₃ mpr₁₄ :
  ∀ {S : Set (ι → K)} (f : (ι → K) → ι → K),
    (∀ (x y : ι → K), x ∈ S → y ∈ S → f x = f y → x = y) →
      ∀ ⦃x₁ : ι → K⦄, x₁ ∈ S → ∀ ⦃x₂ : ι → K⦄, x₂ ∈ S → f x₁ = f x₂ → x₁ = x₂
⊢ ∀ {S : Set (ι → K)} (f : (ι → K) → ι → K),
    (∀ ⦃x₁ : ι → K⦄, x₁ ∈ S → ∀ ⦃x₂ : ι → K⦄, x₂ ∈ S → f x₁ = f x₂ → x₁ = x₂) ↔
      ∀ (x y : ι → K), x ∈ S → y ∈ S → f x = f y → x = y

Tactic:
tauto
-- Module: Mathlib.FieldTheory.AxGrothendieck
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 (ι →₀ ℕ)
⊢ ∀ {S : Set (ι → K)} (f : (ι → K) → ι → K), Set.InjOn f S ↔ ∀ (x y : ι → K), x ∈ S → y ∈ S → f x = f y → x = y

Tactic:
have injOnAlt : ∀ {S : Set (ι → K)} (f : (ι → K) → (ι → K)),
      S.InjOn f ↔ ∀ x y, x ∈ S → y ∈ S → f x = f y → x = y := by
    simp [Set.InjOn]; tauto
-- Module: Mathlib.FieldTheory.AxGrothendieck
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 (ι →₀ ℕ)
injOnAlt : ∀ {S : Set (ι → K)} (f : (ι → K) → ι → K), Set.InjOn f S ↔ ∀ (x y : ι → K), x ∈ S → y ∈ S → f x = f y → x = y
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
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]

Premises used: FirstOrder.Ring.lift_genericPolyMap, FirstOrder.Ring.realize_termOfFreeCommRing, Fin.castAdd_zero, Nat.reduceAdd, FirstOrder.Language.Term.realize_relabel, Fin.cons_one, Sum.elim_inr, Function.comp_def, FirstOrder.Language.Term.realize_var, Fin.isValue, Fin.cast_eq_self, Sum.elim_inl, reduceIte, Nat.add_zero, one_ne_zero, Function.uncurry_apply_pair, Fin.cons_zero
-- Module: Mathlib.FieldTheory.AxGrothendieck
Goal:
ι : Type u_1
α : Type u_2
inst : Finite α
inst_1 : Finite ι
p : ℕ
hp : Nat.Prime p
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
⊢ Fact (Nat.Prime p)

Tactic:
have : Fact p.Prime := ⟨hp⟩
-- Module: Mathlib.FieldTheory.AxGrothendieck
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))
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
⊢ Theory.ACF p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons

Tactic:
rw [← (ACF_isComplete (Or.inl hp)).realize_sentence_iff _
    (AlgebraicClosure (ZMod p)), realize_genericPolyMapSurjOnOfInjOn]

Premises used: ZMod, FirstOrder.realize_genericPolyMapSurjOnOfInjOn, FirstOrder.Language.Theory.IsComplete.realize_sentence_iff, Or.inl, AlgebraicClosure, FirstOrder.Field.ACF_isComplete
-- Module: Mathlib.FieldTheory.AxGrothendieck
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))
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:
ax_grothendieck_of_locally_finite (K := ZMod p) (ι := ι) f _

Premises used: ax_grothendieck_of_locally_finite
-- Module: Mathlib.FieldTheory.AxGrothendieck
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))
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:
exact ax_grothendieck_of_locally_finite (K := ZMod p) (ι := ι) f _

Premises used: ax_grothendieck_of_locally_finite
-- Module: Mathlib.FieldTheory.AxGrothendieck
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
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
⊢ 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 _
-- Module: Mathlib.FieldTheory.AxGrothendieck
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
inr : Theory.ACF 0 ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons
⊢ Theory.ACF p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons

Tactic:
rcases hp with hp | rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.AxGrothendieck
Goal:
ι : Type u_1
α : Type u_2
inst : Finite α
inst_1 : Finite ι
p : ℕ
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
hp : Nat.Prime p
⊢ Theory.ACF p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons

Tactic:
ACF_models_genericPolyMapSurjOnOfInjOn_of_prime hp φ mons

Premises used: FirstOrder.ACF_models_genericPolyMapSurjOnOfInjOn_of_prime
-- Module: Mathlib.FieldTheory.AxGrothendieck
Goal:
ι : Type u_1
α : Type u_2
inst : Finite α
inst_1 : Finite ι
p : ℕ
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
hp : Nat.Prime p
⊢ Theory.ACF p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons

Tactic:
exact ACF_models_genericPolyMapSurjOnOfInjOn_of_prime hp φ mons

Premises used: FirstOrder.ACF_models_genericPolyMapSurjOnOfInjOn_of_prime