-- Mathlib/RingTheory/Nullstellensatz.lean
theorem isMaximal_iff_eq_vanishingIdeal_singleton (I : Ideal (MvPolynomial σ k)) :
    I.IsMaximal ↔ ∃ x : σ → k, I = vanishingIdeal {x}

Proof state:
case intro
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
val✝ : Fintype σ
hI : I.IsMaximal
this✝ : I.IsMaximal := hI
this : Field (MvPolynomial σ k ⧸ I) := Quotient.field I
ϕ : k →+* MvPolynomial σ k ⧸ I := (Ideal.Quotient.mk I).comp C
⊢ ∃ x, I = vanishingIdeal {x}

Tactic:
have hϕ : Function.Bijective ϕ :=
  ⟨quotient_mk_comp_C_injective _ _ I hI.ne_top,
    IsAlgClosed.algebraMap_surjective_of_isIntegral' ϕ
      (MvPolynomial.comp_C_integral_of_surjective_of_isJacobsonRing _ Quotient.mk_surjective)⟩

Result:
case intro
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
val✝ : Fintype σ
hI : I.IsMaximal
this✝ : I.IsMaximal := hI
this : Field (MvPolynomial σ k ⧸ I) := Quotient.field I
ϕ : k →+* MvPolynomial σ k ⧸ I := (Ideal.Quotient.mk I).comp C
hϕ : Function.Bijective ⇑ϕ
⊢ ∃ x, I = vanishingIdeal {x}

Proof state:
case intro.intro
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
val✝ : Fintype σ
hI : I.IsMaximal
this✝ : I.IsMaximal := hI
this : Field (MvPolynomial σ k ⧸ I) := Quotient.field I
ϕ : k →+* MvPolynomial σ k ⧸ I := (Ideal.Quotient.mk I).comp C
hϕ : Function.Bijective ⇑ϕ
φ : MvPolynomial σ k ⧸ I → k
hφ : Function.RightInverse φ ⇑ϕ
x : σ → k := fun s => φ ((Ideal.Quotient.mk I) (X s))
hx : ∀ (s : σ), ϕ (x s) = (Ideal.Quotient.mk I) (X s)
p : MvPolynomial σ k
hp : p ∈ vanishingIdeal {x}
⊢ p ∈ I

Tactic:
rw [← Quotient.eq_zero_iff_mem, map_mvPolynomial_eq_eval₂ (Ideal.Quotient.mk I) p, eval₂_eq']

Result:
case intro.intro
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
val✝ : Fintype σ
hI : I.IsMaximal
this✝ : I.IsMaximal := hI
this : Field (MvPolynomial σ k ⧸ I) := Quotient.field I
ϕ : k →+* MvPolynomial σ k ⧸ I := (Ideal.Quotient.mk I).comp C
hϕ : Function.Bijective ⇑ϕ
φ : MvPolynomial σ k ⧸ I → k
hφ : Function.RightInverse φ ⇑ϕ
x : σ → k := fun s => φ ((Ideal.Quotient.mk I) (X s))
hx : ∀ (s : σ), ϕ (x s) = (Ideal.Quotient.mk I) (X s)
p : MvPolynomial σ k
hp : p ∈ vanishingIdeal {x}
⊢ ∑ d ∈ p.support, ((Ideal.Quotient.mk I).comp C) (coeff d p) * ∏ i : σ, (Ideal.Quotient.mk I) (X i) ^ d i = 0

Proof state:
case intro.intro
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
val✝ : Fintype σ
hI : I.IsMaximal
this✝ : I.IsMaximal := hI
this : Field (MvPolynomial σ k ⧸ I) := Quotient.field I
ϕ : k →+* MvPolynomial σ k ⧸ I := (Ideal.Quotient.mk I).comp C
hϕ : Function.Bijective ⇑ϕ
φ : MvPolynomial σ k ⧸ I → k
hφ : Function.RightInverse φ ⇑ϕ
x : σ → k := fun s => φ ((Ideal.Quotient.mk I) (X s))
hx : ∀ (s : σ), ϕ (x s) = (Ideal.Quotient.mk I) (X s)
p : MvPolynomial σ k
hp : ∑ d ∈ p.support, coeff d p * ∏ i : σ, x i ^ d i = 0
⊢ ∑ d ∈ p.support, ((Ideal.Quotient.mk I).comp C) (coeff d p) * ∏ i : σ, (Ideal.Quotient.mk I) (X i) ^ d i = 0

Tactic:
simpa only [map_sum ϕ, ϕ.map_mul, map_prod ϕ, ϕ.map_pow, ϕ.map_zero, hx] using congr_arg ϕ hp

Result:
no goals

Proof state:
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
val✝ : Fintype σ
hI : I.IsMaximal
this✝ : I.IsMaximal := hI
this : Field (MvPolynomial σ k ⧸ I) := Quotient.field I
ϕ : k →+* MvPolynomial σ k ⧸ I := (Ideal.Quotient.mk I).comp C
hϕ : Function.Bijective ⇑ϕ
φ : MvPolynomial σ k ⧸ I → k
hφ : Function.RightInverse φ ⇑ϕ
x : σ → k := fun s => φ ((Ideal.Quotient.mk I) (X s))
hx : ∀ (s : σ), ϕ (x s) = (Ideal.Quotient.mk I) (X s)
⊢ (vanishingIdeal {x}).IsMaximal

Tactic:
infer_instance

Result:
no goals

Proof state:
case intro
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
val✝ : Fintype σ
hI : I.IsMaximal
this✝ : I.IsMaximal := hI
this : Field (MvPolynomial σ k ⧸ I) := Quotient.field I
ϕ : k →+* MvPolynomial σ k ⧸ I := (Ideal.Quotient.mk I).comp C
hϕ : Function.Bijective ⇑ϕ
⊢ ∃ x, I = vanishingIdeal {x}

Tactic:
obtain ⟨φ, hφ⟩ := Function.Surjective.hasRightInverse hϕ.2

Result:
case intro.intro
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
val✝ : Fintype σ
hI : I.IsMaximal
this✝ : I.IsMaximal := hI
this : Field (MvPolynomial σ k ⧸ I) := Quotient.field I
ϕ : k →+* MvPolynomial σ k ⧸ I := (Ideal.Quotient.mk I).comp C
hϕ : Function.Bijective ⇑ϕ
φ : MvPolynomial σ k ⧸ I → k
hφ : Function.RightInverse φ ⇑ϕ
⊢ ∃ x, I = vanishingIdeal {x}

Proof state:
case intro
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
val✝ : Fintype σ
hI : I.IsMaximal
⊢ ∃ x, I = vanishingIdeal {x}

Tactic:
letI : I.IsMaximal := hI

Result:
case intro
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
val✝ : Fintype σ
hI : I.IsMaximal
this : I.IsMaximal := hI
⊢ ∃ x, I = vanishingIdeal {x}

Proof state:
case intro.intro
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
val✝ : Fintype σ
hI : I.IsMaximal
this✝ : I.IsMaximal := hI
this : Field (MvPolynomial σ k ⧸ I) := Quotient.field I
ϕ : k →+* MvPolynomial σ k ⧸ I := (Ideal.Quotient.mk I).comp C
hϕ : Function.Bijective ⇑ϕ
φ : MvPolynomial σ k ⧸ I → k
hφ : Function.RightInverse φ ⇑ϕ
x : σ → k := fun s => φ ((Ideal.Quotient.mk I) (X s))
⊢ ∃ x, I = vanishingIdeal {x}

Tactic:
have hx : ∀ s : σ, ϕ (x s) = (Ideal.Quotient.mk I) (X s) := fun s =>
  hφ ((Ideal.Quotient.mk I) (X s))

Result:
case intro.intro
k : Type u_1
inst✝² : Field k
σ : Type u_2
inst✝¹ : IsAlgClosed k
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
val✝ : Fintype σ
hI : I.IsMaximal
this✝ : I.IsMaximal := hI
this : Field (MvPolynomial σ k ⧸ I) := Quotient.field I
ϕ : k →+* MvPolynomial σ k ⧸ I := (Ideal.Quotient.mk I).comp C
hϕ : Function.Bijective ⇑ϕ
φ : MvPolynomial σ k ⧸ I → k
hφ : Function.RightInverse φ ⇑ϕ
x : σ → k := fun s => φ ((Ideal.Quotient.mk I) (X s))
hx : ∀ (s : σ), ϕ (x s) = (Ideal.Quotient.mk I) (X s)
⊢ ∃ x, I = vanishingIdeal {x}