-- Mathlib/ModelTheory/Algebra/Ring/Definability.lean
theorem mvPolynomial_zeroLocus_definable {ι K : Type*} [Field K]
    [CompatibleRing K] (S : Finset (MvPolynomial ι K)) :
    Set.Definable (⋃ p ∈ S, p.coeff '' p.support : Set K) Language.ring
      (zeroLocus (Ideal.span (S : Set (MvPolynomial ι K))))

Proof state:
ι : Type u_1
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
S : Finset (MvPolynomial ι K)
p' : { x // x ∈ S } → FreeCommRing ((i : { x // x ∈ S }) × { x // x ∈ (↑i).support } ⊕ ι) :=
  genericPolyMap fun p => (↑p).support
⊢ ∃ φ, zeroLocus (Ideal.span ↑S) = {v | φ.Realize (Sum.elim Subtype.val v)}

Tactic:
letI := Classical.decEq ι

Result:
ι : Type u_1
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
S : Finset (MvPolynomial ι K)
p' : { x // x ∈ S } → FreeCommRing ((i : { x // x ∈ S }) × { x // x ∈ (↑i).support } ⊕ ι) :=
  genericPolyMap fun p => (↑p).support
this : DecidableEq ι := Classical.decEq ι
⊢ ∃ φ, zeroLocus (Ideal.span ↑S) = {v | φ.Realize (Sum.elim Subtype.val v)}

Proof state:
ι : Type u_1
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
S : Finset (MvPolynomial ι K)
⊢ (⋃ p ∈ S, (fun m => coeff m p) '' ↑p.support).Definable ring (zeroLocus (Ideal.span ↑S))

Tactic:
rw [Set.definable_iff_exists_formula_sum]

Result:
ι : Type u_1
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
S : Finset (MvPolynomial ι K)
⊢ ∃ φ, zeroLocus (Ideal.span ↑S) = {v | φ.Realize (Sum.elim Subtype.val v)}

Proof state:
ι : Type u_1
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
S : Finset (MvPolynomial ι K)
p' : { x // x ∈ S } → FreeCommRing ((i : { x // x ∈ S }) × { x // x ∈ (↑i).support } ⊕ ι) :=
  genericPolyMap fun p => (↑p).support
this✝ : DecidableEq ι := Classical.decEq ι
this : DecidableEq K := Classical.decEq K
⊢ ∃ φ, zeroLocus (Ideal.span ↑S) = {v | φ.Realize (Sum.elim Subtype.val v)}

Tactic:
rw [MvPolynomial.zeroLocus_span]

Result:
ι : Type u_1
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
S : Finset (MvPolynomial ι K)
p' : { x // x ∈ S } → FreeCommRing ((i : { x // x ∈ S }) × { x // x ∈ (↑i).support } ⊕ ι) :=
  genericPolyMap fun p => (↑p).support
this✝ : DecidableEq ι := Classical.decEq ι
this : DecidableEq K := Classical.decEq K
⊢ ∃ φ, {x | ∀ p ∈ ↑S, (eval x) p = 0} = {v | φ.Realize (Sum.elim Subtype.val v)}

Proof state:
ι : Type u_1
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
S : Finset (MvPolynomial ι K)
p' : { x // x ∈ S } → FreeCommRing ((i : { x // x ∈ S }) × { x // x ∈ (↑i).support } ⊕ ι) :=
  genericPolyMap fun p => (↑p).support
this✝ : DecidableEq ι := Classical.decEq ι
this : DecidableEq K := Classical.decEq K
⊢ {x | ∀ p ∈ ↑S, (eval x) p = 0} =
    {v |
      Formula.Realize
        (BoundedFormula.iInf fun i =>
          (Term.relabel (Sum.map (fun p => ⟨coeff ↑p.snd ↑p.fst, ⋯⟩) id) (termOfFreeCommRing (p' i))).equal 0)
        (Sum.elim Subtype.val v)}

Tactic:
simp only [Finset.mem_coe, Formula.Realize, Term.equal, Term.relabel_relabel,
Function.comp_def, realize_iInf, realize_bdEqual, Term.realize_relabel, Sum.elim_inl,
realize_termOfFreeCommRing, lift_genericPolyMap, Sum.map_inr, id_eq, Sum.elim_inr, Sum.map_inl,
MvPolynomialSupportLEEquiv_symm_apply_coeff, realize_zero, Subtype.forall, p']

Result:
no goals

Proof state:
ι : Type u_1
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
S : Finset (MvPolynomial ι K)
p' : { x // x ∈ S } → FreeCommRing ((i : { x // x ∈ S }) × { x // x ∈ (↑i).support } ⊕ ι) :=
  genericPolyMap fun p => (↑p).support
this✝ : DecidableEq ι := Classical.decEq ι
this : DecidableEq K := Classical.decEq K
i : { x // x ∈ S }
p : (i : { x // x ∈ S }) × { x // x ∈ (↑i).support }
⊢ coeff ↑p.snd ↑p.fst ∈ ⋃ p ∈ S, (fun m => coeff m p) '' ↑p.support

Tactic:
simp only [Set.mem_iUnion]

Result:
ι : Type u_1
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
S : Finset (MvPolynomial ι K)
p' : { x // x ∈ S } → FreeCommRing ((i : { x // x ∈ S }) × { x // x ∈ (↑i).support } ⊕ ι) :=
  genericPolyMap fun p => (↑p).support
this✝ : DecidableEq ι := Classical.decEq ι
this : DecidableEq K := Classical.decEq K
i : { x // x ∈ S }
p : (i : { x // x ∈ S }) × { x // x ∈ (↑i).support }
⊢ ∃ i, ∃ (_ : i ∈ S), coeff ↑p.snd ↑p.fst ∈ (fun m => coeff m i) '' ↑i.support

Proof state:
ι : Type u_1
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
S : Finset (MvPolynomial ι K)
p' : { x // x ∈ S } → FreeCommRing ((i : { x // x ∈ S }) × { x // x ∈ (↑i).support } ⊕ ι) :=
  genericPolyMap fun p => (↑p).support
this : DecidableEq ι := Classical.decEq ι
⊢ ∃ φ, zeroLocus (Ideal.span ↑S) = {v | φ.Realize (Sum.elim Subtype.val v)}

Tactic:
letI := Classical.decEq K

Result:
ι : Type u_1
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
S : Finset (MvPolynomial ι K)
p' : { x // x ∈ S } → FreeCommRing ((i : { x // x ∈ S }) × { x // x ∈ (↑i).support } ⊕ ι) :=
  genericPolyMap fun p => (↑p).support
this✝ : DecidableEq ι := Classical.decEq ι
this : DecidableEq K := Classical.decEq K
⊢ ∃ φ, zeroLocus (Ideal.span ↑S) = {v | φ.Realize (Sum.elim Subtype.val v)}

Proof state:
ι : Type u_1
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
S : Finset (MvPolynomial ι K)
p' : { x // x ∈ S } → FreeCommRing ((i : { x // x ∈ S }) × { x // x ∈ (↑i).support } ⊕ ι) :=
  genericPolyMap fun p => (↑p).support
this✝ : DecidableEq ι := Classical.decEq ι
this : DecidableEq K := Classical.decEq K
i : { x // x ∈ S }
p : (i : { x // x ∈ S }) × { x // x ∈ (↑i).support }
⊢ ∃ i, ∃ (_ : i ∈ S), coeff ↑p.snd ↑p.fst ∈ (fun m => coeff m i) '' ↑i.support

Tactic:
exact ⟨p.1.1, p.1.2, Set.mem_image_of_mem _ p.2.2⟩

Result:
no goals

Proof state:
ι : Type u_1
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
S : Finset (MvPolynomial ι K)
p' : { x // x ∈ S } → FreeCommRing ((i : { x // x ∈ S }) × { x // x ∈ (↑i).support } ⊕ ι) :=
  genericPolyMap fun p => (↑p).support
this✝ : DecidableEq ι := Classical.decEq ι
this : DecidableEq K := Classical.decEq K
⊢ {x | ∀ p ∈ ↑S, (eval x) p = 0} =
    {v |
      Formula.Realize
        (BoundedFormula.iInf fun i =>
          (Term.relabel (Sum.map (fun p => ⟨coeff ↑p.snd ↑p.fst, ⋯⟩) id) (termOfFreeCommRing (p' i))).equal 0)
        (Sum.elim Subtype.val v)}

Tactic:
simp? [Formula.Realize, Term.equal, Function.comp_def, p'] says
  simp only [Finset.mem_coe, Formula.Realize, Term.equal, Term.relabel_relabel,
  Function.comp_def, realize_iInf, realize_bdEqual, Term.realize_relabel, Sum.elim_inl,
  realize_termOfFreeCommRing, lift_genericPolyMap, Sum.map_inr, id_eq, Sum.elim_inr, Sum.map_inl,
  MvPolynomialSupportLEEquiv_symm_apply_coeff, realize_zero, Subtype.forall, p']

Result:
no goals

Proof state:
ι : Type u_1
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
S : Finset (MvPolynomial ι K)
⊢ ∃ φ, zeroLocus (Ideal.span ↑S) = {v | φ.Realize (Sum.elim Subtype.val v)}

Tactic:
let p' := genericPolyMap (fun p : S => p.1.support)

Result:
ι : Type u_1
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
S : Finset (MvPolynomial ι K)
p' : { x // x ∈ S } → FreeCommRing ((i : { x // x ∈ S }) × { x // x ∈ (↑i).support } ⊕ ι) :=
  genericPolyMap fun p => (↑p).support
⊢ ∃ φ, zeroLocus (Ideal.span ↑S) = {v | φ.Realize (Sum.elim Subtype.val v)}