awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
σ_1 : Type u_2
inst_1 : Finite σ_1
inst_2 : IsDomain R
σ : Type u_2
inst_3 : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R) (Hdeg : ∀ (i : σ), degreeOf i P < #(S i))
    (Heval :
      ∀ (x : σ → R),
        (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) P : R) (0 : R)),
    P = 0
P : MvPolynomial.{u_2, u_1} (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval :
  ∀ (x : Option σ → R),
    (∀ (i : Option σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial (Option σ) R) → R) P : R) (0 : R)
⊢ let Q : Polynomial (MvPolynomial σ R) :=
    (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P;
  Q = (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P

Tactic:
set Q := optionEquivLeft R σ P with hQ

Premises used: MvPolynomial.optionEquivLeft, DFunLike.coe
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
σ_1 : Type u_2
inst_1 : Finite σ_1
inst_2 : IsDomain R
σ : Type u_2
inst_3 : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R) (Hdeg : ∀ (i : σ), degreeOf i P < #(S i))
    (Heval :
      ∀ (x : σ → R),
        (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) P : R) (0 : R)),
    P = 0
P : MvPolynomial.{u_2, u_1} (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval :
  ∀ (x : Option σ → R),
    (∀ (i : Option σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial (Option σ) R) → R) P : R) (0 : R)
Q : Polynomial (MvPolynomial σ R) :=
  (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
hQ : Q = (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
this : Q = 0
rw :
  Eq (α := MvPolynomial.{u_2, u_1} (Option σ) R)
    ((AlgEquiv.symm (optionEquivLeft R σ) : (a : Polynomial (MvPolynomial σ R)) → MvPolynomial (Option σ) R)
        ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P) :
      MvPolynomial.{u_2, u_1} (Option σ) R)
    (0 : MvPolynomial.{u_2, u_1} (Option σ) R)
rw₁ :
  Eq (α := MvPolynomial.{u_2, u_1} (Option σ) R)
    ((AlgEquiv.symm (optionEquivLeft R σ) : (a : Polynomial (MvPolynomial σ R)) → MvPolynomial (Option σ) R) Q :
      MvPolynomial.{u_2, u_1} (Option σ) R)
    (0 : MvPolynomial.{u_2, u_1} (Option σ) R)
rw₂ :
  Eq (α := MvPolynomial.{u_2, u_1} (Option σ) R)
    ((AlgEquiv.symm (optionEquivLeft R σ) : (a : Polynomial (MvPolynomial σ R)) → MvPolynomial (Option σ) R) 0) 0
rw₃ rw₄ : Eq (α := MvPolynomial.{u_2, u_1} (Option σ) R) 0 0
⊢ P = 0

Tactic:
rw [← AlgEquiv.symm_apply_apply (optionEquivLeft R σ) P, ← hQ, this, map_zero]

Premises used: map_zero, AlgEquiv.symm_apply_apply, MvPolynomial.optionEquivLeft
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
σ_1 : Type u_2
inst_1 : Finite σ_1
inst_2 : IsDomain R
σ : Type u_2
inst_3 : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R) (Hdeg : ∀ (i : σ), degreeOf i P < #(S i))
    (Heval :
      ∀ (x : σ → R),
        (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) P : R) (0 : R)),
    P = 0
P : MvPolynomial.{u_2, u_1} (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval :
  ∀ (x : Option σ → R),
    (∀ (i : Option σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial (Option σ) R) → R) P : R) (0 : R)
Q : Polynomial (MvPolynomial σ R) :=
  (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
hQ : Q = (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
h_option : Q = 0
⊢ P = 0

Tactic:
suffices Q = 0 by
      rw [← AlgEquiv.symm_apply_apply (optionEquivLeft R σ) P, ← hQ, this, map_zero]
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
σ_1 : Type u_2
inst_1 : Finite σ_1
inst_2 : IsDomain R
σ : Type u_2
inst_3 : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R) (Hdeg : ∀ (i : σ), degreeOf i P < #(S i))
    (Heval :
      ∀ (x : σ → R),
        (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) P : R) (0 : R)),
    P = 0
P : MvPolynomial.{u_2, u_1} (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval :
  ∀ (x : Option σ → R),
    (∀ (i : Option σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial (Option σ) R) → R) P : R) (0 : R)
Q : Polynomial (MvPolynomial σ R) :=
  (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
hQ : Q = (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
x : σ → R
hx : ∀ (i : σ), x i ∈ S (Option.some i)
heval : ∀ i ∈ S none, Polynomial.eval i (Polynomial.map (eval x) Q) = 0
hcard : (Polynomial.map (eval x) Q).natDegree < #(S none)
⊢ Polynomial.map (eval x) Q = 0

Tactic:
apply Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zero' _ (S none)

Premises used: Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zero', Option.none
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
σ_1 : Type u_2
inst_1 : Finite σ_1
inst_2 : IsDomain R
σ : Type u_2
inst_3 : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R) (Hdeg : ∀ (i : σ), degreeOf i P < #(S i))
    (Heval :
      ∀ (x : σ → R),
        (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) P : R) (0 : R)),
    P = 0
P : MvPolynomial.{u_2, u_1} (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval :
  ∀ (x : Option σ → R),
    (∀ (i : Option σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial (Option σ) R) → R) P : R) (0 : R)
Q : Polynomial (MvPolynomial σ R) :=
  (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
hQ : Q = (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
x : σ → R
hx : ∀ (i : σ), x i ∈ S (Option.some i)
y : R
hy : y ∈ S none
heval :
  Eq.{u_1 + 1} (α := R) ((eval fun (x_1 : Option σ) ↦ x_1.elim y x : (a : MvPolynomial (Option σ) R) → R) P : R) (0 : R)
⊢ Polynomial.eval y (Polynomial.map (eval x) Q) = 0

Tactic:
rw [← optionEquivLeft_elim_eval]

Premises used: MvPolynomial.optionEquivLeft_elim_eval
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
σ_1 : Type u_2
inst_1 : Finite σ_1
inst_2 : IsDomain R
σ : Type u_2
inst_3 : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R) (Hdeg : ∀ (i : σ), degreeOf i P < #(S i))
    (Heval :
      ∀ (x : σ → R),
        (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) P : R) (0 : R)),
    P = 0
P : MvPolynomial.{u_2, u_1} (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval :
  ∀ (x : Option σ → R),
    (∀ (i : Option σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial (Option σ) R) → R) P : R) (0 : R)
Q : Polynomial (MvPolynomial σ R) :=
  (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
hQ : Q = (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
x : σ → R
hx : ∀ (i : σ), x i ∈ S (Option.some i)
y : R
hy : y ∈ S none
heval : ∀ (i : Option σ), i.elim y x ∈ S i
⊢ Eq.{u_1 + 1} (α := R) ((eval fun (x_1 : Option σ) ↦ x_1.elim y x : (a : MvPolynomial (Option σ) R) → R) P : R) (0 : R)

Tactic:
apply Heval
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
σ_1 : Type u_2
inst_1 : Finite σ_1
inst_2 : IsDomain R
σ : Type u_2
inst_3 : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R) (Hdeg : ∀ (i : σ), degreeOf i P < #(S i))
    (Heval :
      ∀ (x : σ → R),
        (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) P : R) (0 : R)),
    P = 0
P : MvPolynomial.{u_2, u_1} (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval :
  ∀ (x : Option σ → R),
    (∀ (i : Option σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial (Option σ) R) → R) P : R) (0 : R)
Q : Polynomial (MvPolynomial σ R) :=
  (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
hQ : Q = (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
x : σ → R
hx : ∀ (i : σ), x i ∈ S (Option.some i)
y : R
hy : y ∈ S none
⊢ ∀ (i : Option σ), i.elim y x ∈ S i

Tactic:
simp only [Option.forall, Option.elim_none, hy, Option.elim_some, hx, implies_true,
          and_self]

Premises used: and_self, Option.elim_none, Option.forall, Option.elim_some, implies_true
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
σ_1 : Type u_2
inst_1 : Finite σ_1
inst_2 : IsDomain R
σ : Type u_2
inst_3 : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R) (Hdeg : ∀ (i : σ), degreeOf i P < #(S i))
    (Heval :
      ∀ (x : σ → R),
        (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) P : R) (0 : R)),
    P = 0
P : MvPolynomial.{u_2, u_1} (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval :
  ∀ (x : Option σ → R),
    (∀ (i : Option σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial (Option σ) R) → R) P : R) (0 : R)
Q : Polynomial (MvPolynomial σ R) :=
  (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
hQ : Q = (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
x : σ → R
hx : ∀ (i : σ), x i ∈ S (Option.some i)
apply : (Polynomial.map (eval x) Q).natDegree ≤ degreeOf none P
⊢ (Polynomial.map (eval x) Q).natDegree < #(S none)

Tactic:
apply lt_of_le_of_lt _ (Hdeg none)

Premises used: lt_of_le_of_lt, Option.none
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
σ_1 : Type u_2
inst_1 : Finite σ_1
inst_2 : IsDomain R
σ : Type u_2
inst_3 : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R) (Hdeg : ∀ (i : σ), degreeOf i P < #(S i))
    (Heval :
      ∀ (x : σ → R),
        (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) P : R) (0 : R)),
    P = 0
P : MvPolynomial.{u_2, u_1} (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval :
  ∀ (x : Option σ → R),
    (∀ (i : Option σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial (Option σ) R) → R) P : R) (0 : R)
Q : Polynomial (MvPolynomial σ R) :=
  (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
hQ : Q = (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
x : σ → R
hx : ∀ (i : σ), x i ∈ S (Option.some i)
rw : ∀ (N : ℕ), degreeOf none P < N → (Polynomial.map (eval x) Q).coeff N = 0
⊢ (Polynomial.map (eval x) Q).natDegree ≤ degreeOf none P

Tactic:
rw [Polynomial.natDegree_le_iff_coeff_eq_zero]

Premises used: Polynomial.natDegree_le_iff_coeff_eq_zero
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
σ_1 : Type u_2
inst_1 : Finite σ_1
inst_2 : IsDomain R
σ : Type u_2
inst_3 : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R) (Hdeg : ∀ (i : σ), degreeOf i P < #(S i))
    (Heval :
      ∀ (x : σ → R),
        (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) P : R) (0 : R)),
    P = 0
P : MvPolynomial.{u_2, u_1} (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval :
  ∀ (x : Option σ → R),
    (∀ (i : Option σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial (Option σ) R) → R) P : R) (0 : R)
Q : Polynomial (MvPolynomial σ R) :=
  (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
hQ : Q = (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
x : σ → R
hx : ∀ (i : σ), x i ∈ S (Option.some i)
d : ℕ
hd : degreeOf none P < d
simp :
  Polynomial.coeff
      (Polynomial.map (eval x)
        ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P))
      d =
    0
⊢ (Polynomial.map (eval x) Q).coeff d = 0

Tactic:
simp only [hQ]
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
σ_1 : Type u_2
inst_1 : Finite σ_1
inst_2 : IsDomain R
σ : Type u_2
inst_3 : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R) (Hdeg : ∀ (i : σ), degreeOf i P < #(S i))
    (Heval :
      ∀ (x : σ → R),
        (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) P : R) (0 : R)),
    P = 0
P : MvPolynomial.{u_2, u_1} (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval :
  ∀ (x : Option σ → R),
    (∀ (i : Option σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial (Option σ) R) → R) P : R) (0 : R)
Q : Polynomial (MvPolynomial σ R) :=
  (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
hQ : Q = (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
x : σ → R
hx : ∀ (i : σ), x i ∈ S (Option.some i)
d : ℕ
hd : degreeOf none P < d
rw :
  Eq.{u_1 + 1} (α := R)
    ((eval x : (a : MvPolynomial σ R) → R)
        (Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P)
          d) :
      R)
    (0 : R)
⊢ Polynomial.coeff
      (Polynomial.map (eval x)
        ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P))
      d =
    0

Tactic:
rw [MvPolynomial.coeff_eval_eq_eval_coeff]

Premises used: MvPolynomial.coeff_eval_eq_eval_coeff
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
σ_1 : Type u_2
inst_1 : Finite σ_1
inst_2 : IsDomain R
σ : Type u_2
inst_3 : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R) (Hdeg : ∀ (i : σ), degreeOf i P < #(S i))
    (Heval :
      ∀ (x : σ → R),
        (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) P : R) (0 : R)),
    P = 0
P : MvPolynomial.{u_2, u_1} (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval :
  ∀ (x : Option σ → R),
    (∀ (i : Option σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial (Option σ) R) → R) P : R) (0 : R)
Q : Polynomial (MvPolynomial σ R) :=
  (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
hQ : Q = (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
x : σ → R
hx : ∀ (i : σ), x i ∈ S (Option.some i)
d : ℕ
hd : degreeOf none P < d
⊢ Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) 0 : R) (0 : R)

Tactic:
map_zero (MvPolynomial.eval x)

Premises used: map_zero, MvPolynomial.eval
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
σ_1 : Type u_2
inst_1 : Finite σ_1
inst_2 : IsDomain R
σ : Type u_2
inst_3 : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R) (Hdeg : ∀ (i : σ), degreeOf i P < #(S i))
    (Heval :
      ∀ (x : σ → R),
        (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) P : R) (0 : R)),
    P = 0
P : MvPolynomial.{u_2, u_1} (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval :
  ∀ (x : Option σ → R),
    (∀ (i : Option σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial (Option σ) R) → R) P : R) (0 : R)
Q : Polynomial (MvPolynomial σ R) :=
  (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
hQ : Q = (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
x : σ → R
hx : ∀ (i : σ), x i ∈ S (Option.some i)
d : ℕ
hd : degreeOf none P < d
h₁ :
  Eq (α := MvPolynomial σ R)
    (Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P) d) 0
⊢ Eq.{u_1 + 1} (α := R)
    ((eval x : (a : MvPolynomial σ R) → R)
        (Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P)
          d) :
      R)
    (0 : R)

Tactic:
convert! map_zero (MvPolynomial.eval x)

Premises used: map_zero, MvPolynomial.eval
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
σ_1 : Type u_2
inst_1 : Finite σ_1
inst_2 : IsDomain R
σ : Type u_2
inst_3 : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R) (Hdeg : ∀ (i : σ), degreeOf i P < #(S i))
    (Heval :
      ∀ (x : σ → R),
        (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) P : R) (0 : R)),
    P = 0
P : MvPolynomial.{u_2, u_1} (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval :
  ∀ (x : Option σ → R),
    (∀ (i : Option σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial (Option σ) R) → R) P : R) (0 : R)
Q : Polynomial (MvPolynomial σ R) :=
  (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
hQ : Q = (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
x : σ → R
hx : ∀ (i : σ), x i ∈ S (Option.some i)
d : ℕ
hd : degreeOf none P < d
h₁ :
  ∀ (m : σ →₀ ℕ),
    Eq.{u_1 + 1} (α := R)
      (coeff m
        (Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P)
          d))
      (coeff m 0)
⊢ Eq (α := MvPolynomial σ R)
    (Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P) d) 0

Tactic:
ext m
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
σ_1 : Type u_2
inst_1 : Finite σ_1
inst_2 : IsDomain R
σ : Type u_2
inst_3 : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R) (Hdeg : ∀ (i : σ), degreeOf i P < #(S i))
    (Heval :
      ∀ (x : σ → R),
        (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) P : R) (0 : R)),
    P = 0
P : MvPolynomial.{u_2, u_1} (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval :
  ∀ (x : Option σ → R),
    (∀ (i : Option σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial (Option σ) R) → R) P : R) (0 : R)
Q : Polynomial (MvPolynomial σ R) :=
  (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
hQ : Q = (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
x : σ → R
hx : ∀ (i : σ), x i ∈ S (Option.some i)
d : ℕ
hd : degreeOf none P < d
m : σ →₀ ℕ
h₁ :
  Eq.{u_1 + 1} (α := R)
    (coeff m
      (Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P) d))
    0
⊢ Eq.{u_1 + 1} (α := R)
    (coeff m
      (Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P) d))
    (coeff m 0)

Tactic:
simp only [coeff_zero]

Premises used: MvPolynomial.coeff_zero
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
σ_1 : Type u_2
inst_1 : Finite σ_1
inst_2 : IsDomain R
σ : Type u_2
inst_3 : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R) (Hdeg : ∀ (i : σ), degreeOf i P < #(S i))
    (Heval :
      ∀ (x : σ → R),
        (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) P : R) (0 : R)),
    P = 0
P : MvPolynomial.{u_2, u_1} (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval :
  ∀ (x : Option σ → R),
    (∀ (i : Option σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial (Option σ) R) → R) P : R) (0 : R)
Q : Polynomial (MvPolynomial σ R) :=
  (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
hQ : Q = (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
x : σ → R
hx : ∀ (i : σ), x i ∈ S (Option.some i)
d : ℕ
hd : degreeOf none P < d
m : σ →₀ ℕ
⊢ let n := (embDomain Embedding.some m).update none d;
  n = (embDomain Embedding.some m).update none d

Tactic:
set n := (embDomain Function.Embedding.some m).update none d with hn

Premises used: Function.Embedding.some, Finsupp.update, Option.none, Finsupp.embDomain
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
σ_1 : Type u_2
inst_1 : Finite σ_1
inst_2 : IsDomain R
σ : Type u_2
inst_3 : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R) (Hdeg : ∀ (i : σ), degreeOf i P < #(S i))
    (Heval :
      ∀ (x : σ → R),
        (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) P : R) (0 : R)),
    P = 0
P : MvPolynomial.{u_2, u_1} (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval :
  ∀ (x : Option σ → R),
    (∀ (i : Option σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial (Option σ) R) → R) P : R) (0 : R)
Q : Polynomial (MvPolynomial σ R) :=
  (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
hQ : Q = (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
x : σ → R
hx : ∀ (i : σ), x i ∈ S (Option.some i)
d : ℕ
hd : degreeOf none P < d
m : σ →₀ ℕ
n : Option σ →₀ ℕ := (embDomain Embedding.some m).update none d
hn : n = (embDomain Embedding.some m).update none d
⊢ (n : (a : Option σ) → ℕ) none = d ∧ n.some = m

Tactic:
rw [eq_option_embedding_update_none_iff] at hn

Premises used: Finsupp.eq_option_embedding_update_none_iff
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
σ_1 : Type u_2
inst_1 : Finite σ_1
inst_2 : IsDomain R
σ : Type u_2
inst_3 : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R) (Hdeg : ∀ (i : σ), degreeOf i P < #(S i))
    (Heval :
      ∀ (x : σ → R),
        (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) P : R) (0 : R)),
    P = 0
P : MvPolynomial.{u_2, u_1} (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval :
  ∀ (x : Option σ → R),
    (∀ (i : Option σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial (Option σ) R) → R) P : R) (0 : R)
Q : Polynomial (MvPolynomial σ R) :=
  (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
hQ : Q = (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
x : σ → R
hx : ∀ (i : σ), x i ∈ S (Option.some i)
d : ℕ
hd : degreeOf none P < d
m : σ →₀ ℕ
n : Option σ →₀ ℕ := (embDomain Embedding.some m).update none d
hn : (n : (a : Option σ) → ℕ) none = d ∧ n.some = m
h₁ : coeff n P = 0
⊢ Eq.{u_1 + 1} (α := R)
    (coeff m
      (Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P) d))
    0

Tactic:
rw [← hn.1, ← hn.2, optionEquivLeft_coeff_some_coeff_none]

Premises used: MvPolynomial.optionEquivLeft_coeff_some_coeff_none, And.right, And.left