-- Mathlib/RingTheory/Nullstellensatz.lean
theorem vanishingIdeal_zeroLocus_eq_radical (I : Ideal (MvPolynomial σ k)) :
    vanishingIdeal (zeroLocus I) = I.radical

Proof state:
case refine_2
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
p : MvPolynomial σ k
hp : p ∈ I.jacobson
x : σ → k
hx : x ∈ zeroLocus I
⊢ (eval x) p = 0

Tactic:
rw [← mem_vanishingIdeal_singleton_iff x p]

Result:
case refine_2
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
p : MvPolynomial σ k
hp : p ∈ I.jacobson
x : σ → k
hx : x ∈ zeroLocus I
⊢ p ∈ vanishingIdeal {x}

Proof state:
case refine_1.intro.intro
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I J : Ideal (MvPolynomial σ k)
hJI : I ≤ J
hJ : J.IsMaximal
x : σ → k
hx : J = vanishingIdeal {x}
y : σ → k
hy : y ∈ {x}
p : MvPolynomial σ k
hp : p ∈ I
⊢ (eval y) p = 0

Tactic:
rw [← mem_vanishingIdeal_singleton_iff, Set.mem_singleton_iff.1 hy, ← hx]

Result:
case refine_1.intro.intro
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I J : Ideal (MvPolynomial σ k)
hJI : I ≤ J
hJ : J.IsMaximal
x : σ → k
hx : J = vanishingIdeal {x}
y : σ → k
hy : y ∈ {x}
p : MvPolynomial σ k
hp : p ∈ I
⊢ p ∈ J

Proof state:
case refine_1.intro.intro
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I J : Ideal (MvPolynomial σ k)
hJI : I ≤ J
hJ : J.IsMaximal
x : σ → k
hx : J = vanishingIdeal {x}
y : σ → k
hy : y ∈ {x}
p : MvPolynomial σ k
hp : p ∈ I
⊢ p ∈ J

Tactic:
exact hJI hp

Result:
no goals

Proof state:
case refine_2
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
p : MvPolynomial σ k
hp : p ∈ I.jacobson
x : σ → k
hx : x ∈ zeroLocus I
⊢ p ∈ vanishingIdeal {x}

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

Result:
no goals

Proof state:
case refine_1.intro
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I J : Ideal (MvPolynomial σ k)
hJI : I ≤ J
hJ : J.IsMaximal
⊢ vanishingIdeal (zeroLocus I) ≤ J

Tactic:
obtain ⟨x, hx⟩ := (isMaximal_iff_eq_vanishingIdeal_singleton J).1 hJ

Result:
case refine_1.intro.intro
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I J : Ideal (MvPolynomial σ k)
hJI : I ≤ J
hJ : J.IsMaximal
x : σ → k
hx : J = vanishingIdeal {x}
⊢ vanishingIdeal (zeroLocus I) ≤ J

Proof state:
case refine_1
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
⊢ ∀ b ∈ {J | I ≤ J ∧ J.IsMaximal}, vanishingIdeal (zeroLocus I) ≤ b

Tactic:
rintro J ⟨hJI, hJ⟩

Result:
case refine_1.intro
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I J : Ideal (MvPolynomial σ k)
hJI : I ≤ J
hJ : J.IsMaximal
⊢ vanishingIdeal (zeroLocus I) ≤ J

Proof state:
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
⊢ vanishingIdeal (zeroLocus I) = I.jacobson

Tactic:
refine le_antisymm (le_sInf ?_) fun p hp x hx => ?_

Result:
case refine_1
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
⊢ ∀ b ∈ {J | I ≤ J ∧ J.IsMaximal}, vanishingIdeal (zeroLocus I) ≤ b

case refine_2
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
p : MvPolynomial σ k
hp : p ∈ I.jacobson
x : σ → k
hx : x ∈ zeroLocus I
⊢ (eval x) p = 0

Proof state:
case refine_1.intro.intro
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I J : Ideal (MvPolynomial σ k)
hJI : I ≤ J
hJ : J.IsMaximal
x : σ → k
hx : J = vanishingIdeal {x}
⊢ vanishingIdeal (zeroLocus I) ≤ J

Tactic:
refine hx.symm ▸ vanishingIdeal_anti_mono fun y hy p hp => ?_

Result:
case refine_1.intro.intro
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I J : Ideal (MvPolynomial σ k)
hJI : I ≤ J
hJ : J.IsMaximal
x : σ → k
hx : J = vanishingIdeal {x}
y : σ → k
hy : y ∈ {x}
p : MvPolynomial σ k
hp : p ∈ I
⊢ (eval y) p = 0

Proof state:
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
⊢ vanishingIdeal (zeroLocus I) = I.radical

Tactic:
rw [I.radical_eq_jacobson]

Result:
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
⊢ vanishingIdeal (zeroLocus I) = I.jacobson