awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.NormalClosure
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : IsDomain S
inst_4 : Algebra R S
inst_5 : Module.IsTorsionFree R S
⊢ IsScalarTower R S T

Tactic:
IsScalarTower.of_algebraMap_eq' rfl

Premises used: IsScalarTower.of_algebraMap_eq', rfl
-- Module: Mathlib.RingTheory.NormalClosure
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : IsDomain S
inst_4 : Algebra R S
inst_5 : Module.IsTorsionFree R S
⊢ IsScalarTower.{u_1, u_2, u_2} R L ↥E

Tactic:
IsScalarTower.to₁₃₄ R K L E

Premises used: IsScalarTower.to₁₃₄, FractionRing, IntermediateField.normalClosure, Membership.mem, Subtype, AlgebraicClosure
-- Module: Mathlib.RingTheory.NormalClosure
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : IsDomain S
inst_4 : Algebra R S
inst_5 : Module.IsTorsionFree R S
⊢ IsScalarTower R S ↥E

Tactic:
IsScalarTower.to₁₂₄ R S L E

Premises used: FractionRing, IntermediateField.normalClosure, Membership.mem, Subtype, IsScalarTower.to₁₂₄, AlgebraicClosure
-- Module: Mathlib.RingTheory.NormalClosure
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : IsDomain S
inst_4 : Algebra R S
inst_5 : Module.IsTorsionFree R S
⊢ IsScalarTower.{u_1, u_2, u_2} R T ↥E

Tactic:
IsScalarTower.to₁₃₄ R S T E

Premises used: Ring.NormalClosure, IsScalarTower.to₁₃₄, FractionRing, IntermediateField.normalClosure, Membership.mem, Subtype, AlgebraicClosure
-- Module: Mathlib.RingTheory.NormalClosure
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : IsDomain S
inst_4 : Algebra R S
inst_5 : Module.IsTorsionFree R S
⊢ FaithfulSMul S ↥E

Tactic:
(faithfulSMul_iff_algebraMap_injective S E).mpr <|
      (FaithfulSMul.algebraMap_injective L E).comp (FaithfulSMul.algebraMap_injective S L)

Premises used: Iff.mpr, faithfulSMul_iff_algebraMap_injective, FractionRing, IntermediateField.normalClosure, Membership.mem, Subtype, Function.Injective.comp, FaithfulSMul.algebraMap_injective, AlgebraicClosure
-- Module: Mathlib.RingTheory.NormalClosure
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : IsDomain S
inst_4 : Algebra R S
inst_5 : Module.IsTorsionFree R S
⊢ Module.IsTorsionFree S T

Tactic:
Subalgebra.instIsTorsionFree (integralClosure S E)

Premises used: Ring.NormalClosure, Set.Mem, Subalgebra.instIsTorsionFree, FractionRing, IntermediateField.normalClosure, Membership.mem, Subtype, integralClosure, AlgebraicClosure
-- Module: Mathlib.RingTheory.NormalClosure
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : IsDomain S
inst_4 : Algebra R S
inst_5 : Module.IsTorsionFree R S
⊢ FaithfulSMul.{u_1, u_2} R T

Tactic:
(faithfulSMul_iff_algebraMap_injective R T).mpr <|
      (FaithfulSMul.algebraMap_injective S T).comp (FaithfulSMul.algebraMap_injective R S)

Premises used: Iff.mpr, Ring.NormalClosure, faithfulSMul_iff_algebraMap_injective, Function.Injective.comp, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.RingTheory.NormalClosure
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : IsDomain S
inst_4 : Algebra R S
inst_5 : Module.IsTorsionFree R S
inst_6 : Module.Finite R S
⊢ FiniteDimensional.{u_2, u_2} L ↥E

Tactic:
Module.Finite.right K L E

Premises used: FractionRing, IntermediateField.normalClosure, Membership.mem, Module.Finite.right, Subtype, AlgebraicClosure
-- Module: Mathlib.RingTheory.NormalClosure
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : IsDomain S
inst_4 : Algebra R S
inst_5 : Module.IsTorsionFree R S
inst_6 : Module.Finite R S
⊢ IsFractionRing.{u_2, u_2} T ↥E

Tactic:
integralClosure.isFractionRing_of_finite_extension L E

Premises used: Ring.NormalClosure, Set.Mem, iSup, FractionRing, integralClosure.isFractionRing_of_finite_extension, IntermediateField.normalClosure, Membership.mem, Subtype, IntermediateField.adjoin, AlgebraicClosure
-- Module: Mathlib.RingTheory.NormalClosure
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : IsDomain S
inst_4 : Algebra R S
inst_5 : Module.IsTorsionFree R S
inst_6 : Module.Finite R S
⊢ IsIntegrallyClosed.{u_2} T

Tactic:
integralClosure.isIntegrallyClosedOfFiniteExtension L

Premises used: Ring.NormalClosure, integralClosure.isIntegrallyClosedOfFiniteExtension, Set.Mem, FractionRing
-- Module: Mathlib.RingTheory.NormalClosure
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : IsDomain S
inst_4 : Algebra R S
inst_5 : Module.IsTorsionFree R S
inst_6 : Module.Finite R S
inst_7 : PerfectField.{u_1} K
⊢ Algebra.IsSeparable.{u_2, u_2} L ↥E

Tactic:
Algebra.isSeparable_tower_top_of_isSeparable K L E

Premises used: FractionRing, IntermediateField.normalClosure, Membership.mem, Subtype, Algebra.isSeparable_tower_top_of_isSeparable, AlgebraicClosure
-- Module: Mathlib.RingTheory.NormalClosure
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : IsDomain S
inst_4 : Algebra R S
inst_5 : Module.IsTorsionFree R S
inst_6 : Module.Finite R S
inst_7 : PerfectField.{u_1} K
⊢ IsGalois.{u_1, u_2} K (FractionRing T)

Tactic:
IsGalois.of_equiv_equiv (F := K) («E» := E)
    (f := (FractionRing.algEquiv R K).symm.toRingEquiv)
    (g := (FractionRing.algEquiv T E).symm.toRingEquiv) ?_

Premises used: IsGalois.of_equiv_equiv
-- Module: Mathlib.RingTheory.NormalClosure
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : IsDomain S
inst_4 : Algebra R S
inst_5 : Module.IsTorsionFree R S
inst_6 : Module.Finite R S
inst_7 : PerfectField.{u_1} K
refine :
  Eq (α := RingHom.{u_1, u_2} K (FractionRing T))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K (FractionRing T))
      (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (FractionRing.algEquiv R K))) : K →+* K))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (FractionRing.algEquiv T ↥E))) : ↥E →+* FractionRing T) (algebraMap K ↥E))
⊢ IsGalois.{u_1, u_2} K (FractionRing T)

Tactic:
refine IsGalois.of_equiv_equiv (F := K) («E» := E)
    (f := (FractionRing.algEquiv R K).symm.toRingEquiv)
    (g := (FractionRing.algEquiv T E).symm.toRingEquiv) ?_
-- Module: Mathlib.RingTheory.NormalClosure
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : IsDomain S
inst_4 : Algebra R S
inst_5 : Module.IsTorsionFree R S
inst_6 : Module.Finite R S
inst_7 : PerfectField.{u_1} K
a :
  ∀ (x : K),
    Eq.{u_2 + 1} (α := FractionRing T)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K (FractionRing T))
              (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (FractionRing.algEquiv R K))) : K →+* K) :
            (a : K) → FractionRing T)
          x :
        FractionRing T)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
              (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (FractionRing.algEquiv T ↥E))) : ↥E →+* FractionRing T)
              (algebraMap K ↥E) :
            (a : K) → FractionRing T)
          x :
        FractionRing T)
⊢ Eq (α := RingHom.{u_1, u_2} K (FractionRing T))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K (FractionRing T))
      (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (FractionRing.algEquiv R K))) : K →+* K))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (FractionRing.algEquiv T ↥E))) : ↥E →+* FractionRing T) (algebraMap K ↥E))

Tactic:
ext
-- Module: Mathlib.RingTheory.NormalClosure
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : IsDomain S
inst_4 : Algebra R S
inst_5 : Module.IsTorsionFree R S
inst_6 : Module.Finite R S
inst_7 : PerfectField.{u_1} K
x : K
⊢ Eq.{u_2 + 1} (α := FractionRing T)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K (FractionRing T))
            (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (FractionRing.algEquiv R K))) : K →+* K) :
          (a : K) → FractionRing T)
        x :
      FractionRing T)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (FractionRing.algEquiv T ↥E))) : ↥E →+* FractionRing T)
            (algebraMap K ↥E) :
          (a : K) → FractionRing T)
        x :
      FractionRing T)

Tactic:
simpa using IsFractionRing.algEquiv_commutes (FractionRing.algEquiv R K).symm
    (FractionRing.algEquiv T E).symm _
-- Module: Mathlib.RingTheory.NormalClosure
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : IsDomain S
inst_4 : Algebra R S
inst_5 : Module.IsTorsionFree R S
inst_6 : Module.Finite R S
inst_7 : PerfectField.{u_1} K
inst_8 : IsDedekindDomain S
⊢ Module.Finite S T

Tactic:
IsIntegralClosure.finite S L E T

Premises used: Ring.NormalClosure, FractionRing, IntermediateField.normalClosure, Membership.mem, Subtype, IsIntegralClosure.finite, AlgebraicClosure
-- Module: Mathlib.RingTheory.NormalClosure
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : IsDomain S
inst_4 : Algebra R S
inst_5 : Module.IsTorsionFree R S
inst_6 : Module.Finite R S
inst_7 : PerfectField.{u_1} K
inst_8 : IsDedekindDomain S
⊢ Module.Finite.{u_1, u_2} R T

Tactic:
Module.Finite.trans S T

Premises used: Ring.NormalClosure, Module.Finite.trans
-- Module: Mathlib.RingTheory.NormalClosure
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : IsDomain S
inst_4 : Algebra R S
inst_5 : Module.IsTorsionFree R S
inst_6 : Module.Finite R S
inst_7 : PerfectField.{u_1} K
inst_8 : IsDedekindDomain S
⊢ IsDedekindDomain.{u_2} T

Tactic:
integralClosure.isDedekindDomain S L E

Premises used: Ring.NormalClosure, Set.Mem, integralClosure.isDedekindDomain, FractionRing, IntermediateField.normalClosure, Membership.mem, Subtype, AlgebraicClosure
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
I : Ideal (MvPolynomial σ k)
x : σ → K
⊢ x ∈ zeroLocus K I ↔ ∀ p ∈ I, Eq.{u_2 + 1} (α := K) ((aeval x : (a : MvPolynomial σ k) → K) p : K) (0 : K)

Tactic:
Iff.rfl

Premises used: MvPolynomial.zeroLocus, Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
I J : Ideal (MvPolynomial σ k)
h : I ≤ J
⊢ zeroLocus K J ≤ zeroLocus K I

Tactic:
fun _ hx p hp => hx p <| h hp

Premises used: MvPolynomial.zeroLocus, Set.Mem, setOf, Set.Subset
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
⊢ Eq (α := Set (σ → K)) (zeroLocus.{u_1, u_2, u_3} (k := k) K ⊥) ⊤

Tactic:
eq_top_iff.2 fun x _ _ hp => Trans.trans (congr_arg (aeval x) (mem_bot.1 hp)) (eval x).map_zero

Premises used: Ideal.mem_bot, Iff.mpr, Trans.trans, eq_top_iff, MvPolynomial.aeval, MvPolynomial.eval, congr_arg, RingHom.map_zero, Iff.mp, DFunLike.coe
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
⊢ Eq (α := Set (σ → K)) (zeroLocus.{u_1, u_2, u_3} (k := k) K ⊤) ⊥

Tactic:
eq_bot_iff.2 fun x hx => one_ne_zero
    ((aeval (R := k) x).map_one ▸ hx 1 Submodule.mem_top : (1 : K) = 0)

Premises used: Iff.mpr, MvPolynomial.aeval, RingHom.map_one, Eq.rec, AlgHom.toRingHom, eq_bot_iff, one_ne_zero, OfNat.ofNat, Submodule.mem_top
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
V : Set (σ → K)
p q : MvPolynomial σ k
hp :
  Membership.mem (γ := Set (MvPolynomial σ k))
    {p : MvPolynomial σ k | ∀ x ∈ V, Eq.{u_2 + 1} (α := K) ((aeval x : (a : MvPolynomial σ k) → K) p : K) (0 : K)} p
hq :
  Membership.mem (γ := Set (MvPolynomial σ k))
    {p : MvPolynomial σ k | ∀ x ∈ V, Eq.{u_2 + 1} (α := K) ((aeval x : (a : MvPolynomial σ k) → K) p : K) (0 : K)} q
x : σ → K
hx : x ∈ V
⊢ Eq.{u_2 + 1} (α := K) ((aeval x : (a : MvPolynomial σ k) → K) (p + q) : K) (0 : K)

Tactic:
simp only [hq x hx, hp x hx, add_zero, map_add]

Premises used: map_add, add_zero
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
V : Set (σ → K)
p q : MvPolynomial σ k
hq :
  Membership.mem (γ := Set (MvPolynomial σ k))
    {p : MvPolynomial σ k | ∀ x ∈ V, Eq.{u_2 + 1} (α := K) ((aeval x : (a : MvPolynomial σ k) → K) p : K) (0 : K)} q
x : σ → K
hx : x ∈ V
⊢ Eq.{u_2 + 1} (α := K) ((aeval x : (a : MvPolynomial σ k) → K) (p • q) : K) (0 : K)

Tactic:
simp only [hq x hx, smul_eq_mul, mul_zero, map_mul]

Premises used: MulZeroClass.mul_zero, map_mul, smul_eq_mul
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
V : Set (σ → K)
p : MvPolynomial σ k
⊢ Membership.mem (γ := Ideal (MvPolynomial σ k)) (vanishingIdeal k V) p ↔
    ∀ x ∈ V, Eq.{u_2 + 1} (α := K) ((aeval x : (a : MvPolynomial σ k) → K) p : K) (0 : K)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
A B : Set (σ → K)
h : A ≤ B
⊢ LE.le (α := Ideal (MvPolynomial σ k)) (vanishingIdeal k B) (vanishingIdeal k A)

Tactic:
fun _ hp x hx => hp x <| h hx

Premises used: Set.Mem, setOf
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
⊢ Eq (α := Ideal (MvPolynomial σ k)) (vanishingIdeal.{u_1, u_2, u_3} k (K := K) ∅) ⊤

Tactic:
le_antisymm le_top fun _ _ x hx => absurd hx (Set.notMem_empty x)

Premises used: le_antisymm, absurd, le_top, Set.notMem_empty
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
I : Ideal (MvPolynomial σ k)
⊢ I ≤ vanishingIdeal k (zeroLocus K I)

Tactic:
fun p hp _ hx => hx p hp

Premises used: Set.Mem, setOf
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
V : Set (σ → K)
⊢ V ≤ zeroLocus K (vanishingIdeal k V)

Tactic:
fun V hV _ hp => hp V hV

Premises used: MvPolynomial.zeroLocus, Set.Mem, setOf, Set.Subset
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
⊢ GaloisConnection (α := Ideal (MvPolynomial σ k)) (zeroLocus K) (vanishingIdeal k)

Tactic:
GaloisConnection.monotone_intro (fun _ _ ↦ vanishingIdeal_anti_mono)
    (fun _ _ ↦ zeroLocus_anti_mono) le_vanishingIdeal_zeroLocus zeroLocus_vanishingIdeal_le

Premises used: MvPolynomial.vanishingIdeal_anti_mono, MvPolynomial.le_vanishingIdeal_zeroLocus, MvPolynomial.zeroLocus_vanishingIdeal_le, GaloisConnection.monotone_intro, MvPolynomial.zeroLocus_anti_mono
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
V : Set (σ → K)
I : Ideal (MvPolynomial σ k)
⊢ V ≤ zeroLocus K I ↔ I ≤ vanishingIdeal k V

Tactic:
zeroLocus_vanishingIdeal_galoisConnection.le_iff_le

Premises used: GaloisConnection.le_iff_le, MvPolynomial.zeroLocus_vanishingIdeal_galoisConnection
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
S : Set (MvPolynomial σ k)
⊢ zeroLocus K (span S) =
    {x : σ → K | ∀ p ∈ S, Eq.{u_2 + 1} (α := K) ((aeval x : (a : MvPolynomial σ k) → K) p : K) (0 : K)}

Tactic:
eq_of_forall_le_iff fun _ => le_zeroLocus_iff_le_vanishingIdeal.trans <|
    Ideal.span_le.trans forall₂_comm

Premises used: Ideal.span_le, MvPolynomial.le_zeroLocus_iff_le_vanishingIdeal, Iff.trans, eq_of_forall_le_iff, forall₂_comm
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
x : σ → K
p : MvPolynomial σ k
⊢ Membership.mem (γ := Ideal (MvPolynomial σ k)) (vanishingIdeal.{u_1, u_2, u_3} k (K := K) {x}) p ↔
    Eq.{u_2 + 1} (α := K) ((aeval x : (a : MvPolynomial σ k) → K) p : K) (0 : K)

Tactic:
⟨fun h => h x rfl, fun hpx _ hy => hy.symm ▸ hpx⟩

Premises used: Eq.rec, Iff.intro, Eq.symm, rfl
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
x : σ → K
⊢ IsPrime (RingHom.ker (F := MvPolynomial σ k →ₐ[k] K) (aeval x))

Tactic:
RingHom.ker_isPrime (aeval (R := k) x)

Premises used: MvPolynomial.aeval, RingHom.ker_isPrime
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
x : σ → K
h : vanishingIdeal.{u_1, u_2, u_3} k (K := K) {x} = RingHom.ker (F := MvPolynomial σ k →ₐ[k] K) (aeval x)
⊢ IsPrime (α := MvPolynomial σ k) (vanishingIdeal.{u_1, u_2, u_3} k (K := K) {x})

Tactic:
convert! RingHom.ker_isPrime (aeval (R := k) x)

Premises used: MvPolynomial.aeval, RingHom.ker_isPrime
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
x : σ → K
h :
  ∀ (x_1 : MvPolynomial σ k),
    Membership.mem (γ := Ideal (MvPolynomial σ k)) (vanishingIdeal.{u_1, u_2, u_3} k (K := K) {x}) x_1 ↔
      Membership.mem (γ := Ideal (MvPolynomial σ k)) (RingHom.ker (F := MvPolynomial σ k →ₐ[k] K) (aeval x)) x_1
⊢ vanishingIdeal.{u_1, u_2, u_3} k (K := K) {x} = RingHom.ker (F := MvPolynomial σ k →ₐ[k] K) (aeval x)

Tactic:
ext
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
x : σ → K
x_1 : MvPolynomial σ k
⊢ Membership.mem (γ := Ideal (MvPolynomial σ k)) (vanishingIdeal.{u_1, u_2, u_3} k (K := K) {x}) x_1 ↔
    Membership.mem (γ := Ideal (MvPolynomial σ k)) (RingHom.ker (F := MvPolynomial σ k →ₐ[k] K) (aeval x)) x_1

Tactic:
simp
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
x : σ → K
⊢ IsMaximal (RingHom.ker (F := MvPolynomial σ K →ₐ[K] K) (aeval x))

Tactic:
RingHom.ker_isMaximal_of_surjective (aeval (R := K) x) ?_

Premises used: MvPolynomial.aeval, RingHom.ker_isMaximal_of_surjective
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
x : σ → K
h :
  Eq (α := Semiring (MvPolynomial σ K)) AddMonoidAlgebra.semiring Ring.toSemiring →
    vanishingIdeal K (K := K) {x} = RingHom.ker (F := MvPolynomial σ K →ₐ[K] K) (aeval x)
convert! : Function.Surjective (α := MvPolynomial σ K) (β := K) (⇑(aeval x) : (a : MvPolynomial σ K) → K)
⊢ IsMaximal (α := MvPolynomial σ K) (vanishingIdeal K (K := K) {x})

Tactic:
convert! RingHom.ker_isMaximal_of_surjective (aeval (R := K) x) ?_

Premises used: MvPolynomial.aeval, RingHom.ker_isMaximal_of_surjective
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
x : σ → K
e_2 : Eq (α := Semiring (MvPolynomial σ K)) AddMonoidAlgebra.semiring Ring.toSemiring
h :
  ∀ (x_1 : MvPolynomial σ K),
    Membership.mem (γ := Ideal (MvPolynomial σ K)) (vanishingIdeal K (K := K) {x}) x_1 ↔
      Membership.mem (γ := Ideal (MvPolynomial σ K)) (RingHom.ker (F := MvPolynomial σ K →ₐ[K] K) (aeval x)) x_1
⊢ vanishingIdeal K (K := K) {x} = RingHom.ker (F := MvPolynomial σ K →ₐ[K] K) (aeval x)

Tactic:
ext
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
x : σ → K
e_2 : Eq (α := Semiring (MvPolynomial σ K)) AddMonoidAlgebra.semiring Ring.toSemiring
x_1 : MvPolynomial σ K
⊢ Membership.mem (γ := Ideal (MvPolynomial σ K)) (vanishingIdeal K (K := K) {x}) x_1 ↔
    Membership.mem (γ := Ideal (MvPolynomial σ K)) (RingHom.ker (F := MvPolynomial σ K →ₐ[K] K) (aeval x)) x_1

Tactic:
simp
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
x : σ → K
z : K
h : (aeval x : (a : MvPolynomial σ K) → K) ((C : (a : K) → MvPolynomial σ K) z : MvPolynomial σ K) = z
⊢ ∃ (a : MvPolynomial σ K), (aeval x : (a : MvPolynomial σ K) → K) a = z

Tactic:
use C z

Premises used: MvPolynomial.C, DFunLike.coe
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
x : σ → K
z : K
⊢ (aeval x : (a : MvPolynomial σ K) → K) ((C : (a : K) → MvPolynomial σ K) z : MvPolynomial σ K) = z

Tactic:
simp
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
I : Ideal (MvPolynomial σ k)
p : MvPolynomial σ k
hp : p ∈ I.radical
x : σ → K
hx : x ∈ zeroLocus K I
rw : Membership.mem (γ := Ideal (MvPolynomial σ k)) (vanishingIdeal.{u_1, u_2, u_3} k (K := K) {x}) p
⊢ Eq.{u_2 + 1} (α := K) ((aeval x : (a : MvPolynomial σ k) → K) p : K) (0 : K)

Tactic:
rw [← mem_vanishingIdeal_singleton_iff]

Premises used: MvPolynomial.mem_vanishingIdeal_singleton_iff
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
I : Ideal (MvPolynomial σ k)
p : MvPolynomial σ k
hp : p ∈ I.radical
x : σ → K
hx : x ∈ zeroLocus K I
rw :
  ∀
    (hp :
      Membership.mem (γ := Submodule (MvPolynomial σ k) (MvPolynomial σ k))
        (sInf {J : Ideal (MvPolynomial σ k) | I ≤ J ∧ J.IsPrime}) p)
    (x : σ → K) (hx : x ∈ zeroLocus K I),
    Membership.mem (γ := Ideal (MvPolynomial σ k)) (vanishingIdeal.{u_1, u_2, u_3} k (K := K) {x}) p
⊢ Membership.mem (γ := Ideal (MvPolynomial σ k)) (vanishingIdeal.{u_1, u_2, u_3} k (K := K) {x}) p

Tactic:
rw [radical_eq_sInf] at hp

Premises used: Ideal.radical_eq_sInf
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
I : Ideal (MvPolynomial σ k)
p : MvPolynomial σ k
hp :
  Membership.mem (γ := Submodule (MvPolynomial σ k) (MvPolynomial σ k))
    (sInf {J : Ideal (MvPolynomial σ k) | I ≤ J ∧ J.IsPrime}) p
x : σ → K
hx : x ∈ zeroLocus K I
⊢ Membership.mem (γ := Ideal (MvPolynomial σ k)) (vanishingIdeal.{u_1, u_2, u_3} k (K := K) {x}) p

Tactic:
(mem_sInf.mp hp)
      ⟨le_trans (le_vanishingIdeal_zeroLocus I)
          (vanishingIdeal_anti_mono fun y hy => hy.symm ▸ hx),
        inferInstance⟩

Premises used: MvPolynomial.vanishingIdeal_anti_mono, MvPolynomial.le_vanishingIdeal_zeroLocus, Set.Mem, Eq.rec, inferInstance, Ideal.mem_sInf, And.intro, Iff.mp, Eq.symm, le_trans
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
I : Ideal (MvPolynomial σ k)
p : MvPolynomial σ k
hp :
  Membership.mem (γ := Submodule (MvPolynomial σ k) (MvPolynomial σ k))
    (sInf {J : Ideal (MvPolynomial σ k) | I ≤ J ∧ J.IsPrime}) p
x : σ → K
hx : x ∈ zeroLocus K I
⊢ Membership.mem (γ := Ideal (MvPolynomial σ k)) (vanishingIdeal.{u_1, u_2, u_3} k (K := K) {x}) p

Tactic:
refine
    (mem_sInf.mp hp)
      ⟨le_trans (le_vanishingIdeal_zeroLocus I)
          (vanishingIdeal_anti_mono fun y hy => hy.symm ▸ hx),
        inferInstance⟩

Premises used: MvPolynomial.vanishingIdeal_anti_mono, MvPolynomial.le_vanishingIdeal_zeroLocus, inferInstance, Ideal.mem_sInf, And.intro, Iff.mp, le_trans
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
x : σ → K
⊢ IsPrime (α := MvPolynomial σ k) (vanishingIdeal.{u_1, u_2, u_3} k (K := K) {x})

Tactic:
infer_instance