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)
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₁ : ∀ (hm : ¬coeff n P = 0), False
⊢ coeff n P = 0

Tactic:
by_contra hm
-- 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
hm : ¬coeff n P = 0
h₁ : d ≤ degreeOf none P
⊢ False

Tactic:
apply not_le.mpr hd

Premises used: not_le, Iff.mpr
-- 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
hm : ¬coeff n P = 0
h₁ : d ≤ P.support.sup fun (m : Option σ →₀ ℕ) ↦ (m : (a : Option σ) → ℕ) none
⊢ d ≤ degreeOf none P

Tactic:
rw [MvPolynomial.degreeOf_eq_sup]

Premises used: MvPolynomial.degreeOf_eq_sup
-- 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
hm : ¬coeff n P = 0
⊢ n ∈ P.support

Tactic:
rw [← ne_eq, ← MvPolynomial.mem_support_iff] at hm

Premises used: MvPolynomial.mem_support_iff, ne_eq
-- 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
hm : n ∈ P.support
⊢ LE.le (α := ℕ) ((n : (a : Option σ) → ℕ) none : ℕ)
    (P.support.sup fun (m : Option σ →₀ ℕ) ↦ (m : (a : Option σ) → ℕ) none : ℕ)

Tactic:
Finset.le_sup hm

Premises used: Finset.le_sup
-- 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
hm : n ∈ P.support
h₁ : d = (n : (a : Option σ) → ℕ) none
⊢ d ≤ P.support.sup fun (m : Option σ →₀ ℕ) ↦ (m : (a : Option σ) → ℕ) none

Tactic:
convert! Finset.le_sup hm

Premises used: Finset.le_sup
-- 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
hm : n ∈ P.support
⊢ d = (n : (a : Option σ) → ℕ) none

Tactic:
hn.1.symm

Premises used: And.left, Eq.symm
-- 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
hm : n ∈ P.support
⊢ d = (n : (a : Option σ) → ℕ) none

Tactic:
exact hn.1.symm

Premises used: And.left, Eq.symm
-- 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)), Polynomial.map (eval x) Q = 0

Tactic:
have Heval' (x : σ → R) (hx : ∀ i, x i ∈ S (some i)) : Polynomial.map (eval x) Q = 0 := by
      apply Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zero' _ (S none)
      · intro y hy
        rw [← optionEquivLeft_elim_eval]
        apply Heval
        simp only [Option.forall, Option.elim_none, hy, Option.elim_some, hx, implies_true,
          and_self]
      · apply lt_of_le_of_lt _ (Hdeg none)
        rw [Polynomial.natDegree_le_iff_coeff_eq_zero]
        intro d hd
        simp only [hQ]
        rw [MvPolynomial.coeff_eval_eq_eval_coeff]
        convert! map_zero (MvPolynomial.eval x)
        ext m
        simp only [coeff_zero]
        set n := (embDomain Function.Embedding.some m).update none d with hn
        rw [eq_option_embedding_update_none_iff] at hn
        rw [← hn.1, ← hn.2, optionEquivLeft_coeff_some_coeff_none]
        by_contra hm
        apply not_le.mpr hd
        rw [MvPolynomial.degreeOf_eq_sup]
        rw [← ne_eq, ← MvPolynomial.mem_support_iff] at hm
        convert! Finset.le_sup hm
        exact hn.1.symm
-- 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
Heval' : ∀ (x : σ → R) (hx : ∀ (i : σ), x i ∈ S (Option.some i)), Polynomial.map (eval x) Q = 0
h_option : ∀ (m : ℕ) (d : σ →₀ ℕ), coeff d (Q.coeff m) = coeff d (Polynomial.coeff 0 m)
⊢ Q = 0

Tactic:
ext m d
-- 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
Heval' : ∀ (x : σ → R) (hx : ∀ (i : σ), x i ∈ S (Option.some i)), Polynomial.map (eval x) Q = 0
m : ℕ
d : σ →₀ ℕ
h_option : coeff d (Q.coeff m) = 0
⊢ coeff d (Q.coeff m) = coeff d (Polynomial.coeff 0 m)

Tactic:
simp only [Polynomial.coeff_zero, coeff_zero]

Premises used: MvPolynomial.coeff_zero, Polynomial.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
Heval' : ∀ (x : σ → R) (hx : ∀ (i : σ), x i ∈ S (Option.some i)), Polynomial.map (eval x) Q = 0
m : ℕ
d : σ →₀ ℕ
this : Q.coeff m = 0
⊢ coeff d (Q.coeff m) = 0

Tactic:
simp only [this, 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
Heval' : ∀ (x : σ → R) (hx : ∀ (i : σ), x i ∈ S (Option.some i)), Polynomial.map (eval x) Q = 0
m : ℕ
d : σ →₀ ℕ
h_option : Q.coeff m = 0
⊢ coeff d (Q.coeff m) = 0

Tactic:
suffices Q.coeff m = 0 by simp only [this, 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
Heval' : ∀ (x : σ → R) (hx : ∀ (i : σ), x i ∈ S (Option.some i)), Polynomial.map (eval x) Q = 0
m : ℕ
d : σ →₀ ℕ
h_option : ∀ (i : σ), degreeOf i (Q.coeff m) < #(S (Option.some i))
h_option₁ :
  ∀ (x : σ → R),
    (∀ (i : σ), x i ∈ S (Option.some i)) →
      Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) (Q.coeff m) : R) (0 : R)
⊢ Q.coeff m = 0

Tactic:
apply h _ (fun i ↦ S (some i))

Premises used: Option.some
-- 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
Heval' : ∀ (x : σ → R) (hx : ∀ (i : σ), x i ∈ S (Option.some i)), Polynomial.map (eval x) Q = 0
m : ℕ
d : σ →₀ ℕ
i : σ
apply : degreeOf i (Q.coeff m) ≤ degreeOf (Option.some i) P
⊢ degreeOf i (Q.coeff m) < #(S (Option.some i))

Tactic:
apply lt_of_le_of_lt _ (Hdeg (some i))

Premises used: lt_of_le_of_lt, Option.some
-- 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
Heval' : ∀ (x : σ → R) (hx : ∀ (i : σ), x i ∈ S (Option.some i)), Polynomial.map (eval x) Q = 0
m : ℕ
d : σ →₀ ℕ
i : σ
simp :
  ∀ (b : σ →₀ ℕ),
    ¬coeff b (Q.coeff m) = 0 →
      LE.le (α := ℕ) ((b : (a : σ) → ℕ) i : ℕ)
        (P.support.sup fun (m : Option σ →₀ ℕ) ↦ (m : (a : Option σ) → ℕ) (Option.some i) : ℕ)
⊢ degreeOf i (Q.coeff m) ≤ degreeOf (Option.some i) P

Tactic:
simp only [degreeOf_eq_sup, Finset.sup_le_iff, mem_support_iff, ne_eq]

Premises used: MvPolynomial.mem_support_iff, ne_eq, MvPolynomial.degreeOf_eq_sup, Finset.sup_le_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
Heval' : ∀ (x : σ → R) (hx : ∀ (i : σ), x i ∈ S (Option.some i)), Polynomial.map (eval x) Q = 0
m : ℕ
d : σ →₀ ℕ
i : σ
e : σ →₀ ℕ
he : ¬coeff e (Q.coeff m) = 0
⊢ let n := (embDomain Embedding.some e).update none m;
  n = (embDomain Embedding.some e).update none m

Tactic:
set n := (embDomain Function.Embedding.some e).update none m 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
Heval' : ∀ (x : σ → R) (hx : ∀ (i : σ), x i ∈ S (Option.some i)), Polynomial.map (eval x) Q = 0
m : ℕ
d : σ →₀ ℕ
i : σ
e : σ →₀ ℕ
he : ¬coeff e (Q.coeff m) = 0
n : Option σ →₀ ℕ := (embDomain Embedding.some e).update none m
hn : n = (embDomain Embedding.some e).update none m
⊢ (n : (a : Option σ) → ℕ) none = m ∧ n.some = e

Tactic:
rw [eq_option_embedding_update_none_iff] at hn

Premises used: Finsupp.eq_option_embedding_update_none_iff