awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_2
inst_1 : Finite σ
inst_2 : IsDomain R
S : σ → Finset R
Sne : ∀ (i : σ), (S i).Nonempty
f : MvPolynomial σ R
Heval :
  ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) f : R) (0 : R)
this : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
h : σ →₀ MvPolynomial σ R
r : MvPolynomial σ R
hf :
  f =
    HAdd.hAdd (α := MvPolynomial σ R)
      ((linearCombination (MvPolynomial σ R) fun (i : σ) ↦ Alon.P (S i) i :
            (a : σ →₀ MvPolynomial σ R) → MvPolynomial σ R)
          h :
        MvPolynomial σ R)
      r
hh :
  ∀ (i : σ),
    LE.le (α := syn (σ := σ) degLex)
      ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn)
          (MonomialOrder.degree degLex
            (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (Alon.P (S i) i)
              ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R))) :
        syn (σ := σ) degLex)
      ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn) (MonomialOrder.degree degLex f) : syn (σ := σ) degLex)
hr : ∀ c ∈ r.support, ∀ (i : σ), ¬MonomialOrder.degree degLex (Alon.P (S i) i) ≤ c
i : σ
⊢ ⊥ < #(S i)

Tactic:
simp [Sne i]
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_2
inst_1 : Finite σ
inst_2 : IsDomain R
S : σ → Finset R
Sne : ∀ (i : σ), (S i).Nonempty
f : MvPolynomial σ R
Heval :
  ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) f : R) (0 : R)
this : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
h : σ →₀ MvPolynomial σ R
r : MvPolynomial σ R
hf :
  f =
    HAdd.hAdd (α := MvPolynomial σ R)
      ((linearCombination (MvPolynomial σ R) fun (i : σ) ↦ Alon.P (S i) i :
            (a : σ →₀ MvPolynomial σ R) → MvPolynomial σ R)
          h :
        MvPolynomial σ R)
      r
hh :
  ∀ (i : σ),
    LE.le (α := syn (σ := σ) degLex)
      ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn)
          (MonomialOrder.degree degLex
            (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (Alon.P (S i) i)
              ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R))) :
        syn (σ := σ) degLex)
      ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn) (MonomialOrder.degree degLex f) : syn (σ := σ) degLex)
hr : ∀ c ∈ r.support, ∀ (i : σ), ¬MonomialOrder.degree degLex (Alon.P (S i) i) ≤ c
i : σ
h₁ : ∀ b ∈ r.support, (b : (a : σ) → ℕ) i < #(S i)
⊢ degreeOf i r < #(S i)

Tactic:
rw [degreeOf_eq_sup, Finset.sup_lt_iff (by simp [Sne i])]

Premises used: Finset.sup_lt_iff, MvPolynomial.degreeOf_eq_sup
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_2
inst_1 : Finite σ
inst_2 : IsDomain R
S : σ → Finset R
Sne : ∀ (i : σ), (S i).Nonempty
f : MvPolynomial σ R
Heval :
  ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) f : R) (0 : R)
this : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
h : σ →₀ MvPolynomial σ R
r : MvPolynomial σ R
hf :
  f =
    HAdd.hAdd (α := MvPolynomial σ R)
      ((linearCombination (MvPolynomial σ R) fun (i : σ) ↦ Alon.P (S i) i :
            (a : σ →₀ MvPolynomial σ R) → MvPolynomial σ R)
          h :
        MvPolynomial σ R)
      r
hh :
  ∀ (i : σ),
    LE.le (α := syn (σ := σ) degLex)
      ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn)
          (MonomialOrder.degree degLex
            (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (Alon.P (S i) i)
              ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R))) :
        syn (σ := σ) degLex)
      ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn) (MonomialOrder.degree degLex f) : syn (σ := σ) degLex)
hr : ∀ c ∈ r.support, ∀ (i : σ), ¬MonomialOrder.degree degLex (Alon.P (S i) i) ≤ c
i : σ
⊢ ∀ b ∈ r.support, (b : (a : σ) → ℕ) i < #(S i)

Tactic:
aesop (add simp [Alon.degree_P])

Premises used: _private.0.MvPolynomial.Alon.degree_P
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_2
inst_1 : Finite σ
inst_2 : IsDomain R
S : σ → Finset R
Sne : ∀ (i : σ), (S i).Nonempty
f : MvPolynomial σ R
Heval :
  ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) f : R) (0 : R)
this : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
h : σ →₀ MvPolynomial σ R
r : MvPolynomial σ R
hf :
  f =
    HAdd.hAdd (α := MvPolynomial σ R)
      ((linearCombination (MvPolynomial σ R) fun (i : σ) ↦ Alon.P (S i) i :
            (a : σ →₀ MvPolynomial σ R) → MvPolynomial σ R)
          h :
        MvPolynomial σ R)
      r
hh :
  ∀ (i : σ),
    LE.le (α := syn (σ := σ) degLex)
      ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn)
          (MonomialOrder.degree degLex
            (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (Alon.P (S i) i)
              ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R))) :
        syn (σ := σ) degLex)
      ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn) (MonomialOrder.degree degLex f) : syn (σ := σ) degLex)
hr : ∀ c ∈ r.support, ∀ (i : σ), ¬MonomialOrder.degree degLex (Alon.P (S i) i) ≤ c
x : σ → R
hx : ∀ (i : σ), x i ∈ S i
h₁ :
  ∀
    (hf :
      HSub.hSub (β := MvPolynomial σ R) f
          ((linearCombination (MvPolynomial σ R) fun (i : σ) ↦ Alon.P (S i) i :
                (a : σ →₀ MvPolynomial σ R) → MvPolynomial σ R)
              h :
            MvPolynomial σ R) =
        r)
    (hh :
      ∀ (i : σ),
        LE.le (α := syn (σ := σ) degLex)
          ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn)
              (MonomialOrder.degree degLex
                (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (Alon.P (S i) i)
                  ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R))) :
            syn (σ := σ) degLex)
          ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn) (MonomialOrder.degree degLex f) : syn (σ := σ) degLex))
    (hr : ∀ c ∈ r.support, ∀ (i : σ), ¬MonomialOrder.degree degLex (Alon.P (S i) i) ≤ c) (x : σ → R)
    (hx : ∀ (i : σ), x i ∈ S i), Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) r : R) (0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) r : R) (0 : R)

Tactic:
rw [Iff.symm sub_eq_iff_eq_add'] at hf

Premises used: Iff.symm, sub_eq_iff_eq_add'
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_2
inst_1 : Finite σ
inst_2 : IsDomain R
S : σ → Finset R
Sne : ∀ (i : σ), (S i).Nonempty
f : MvPolynomial σ R
Heval :
  ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) f : R) (0 : R)
this : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
h : σ →₀ MvPolynomial σ R
r : MvPolynomial σ R
hf :
  HSub.hSub (β := MvPolynomial σ R) f
      ((linearCombination (MvPolynomial σ R) fun (i : σ) ↦ Alon.P (S i) i :
            (a : σ →₀ MvPolynomial σ R) → MvPolynomial σ R)
          h :
        MvPolynomial σ R) =
    r
hh :
  ∀ (i : σ),
    LE.le (α := syn (σ := σ) degLex)
      ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn)
          (MonomialOrder.degree degLex
            (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (Alon.P (S i) i)
              ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R))) :
        syn (σ := σ) degLex)
      ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn) (MonomialOrder.degree degLex f) : syn (σ := σ) degLex)
hr : ∀ c ∈ r.support, ∀ (i : σ), ¬MonomialOrder.degree degLex (Alon.P (S i) i) ≤ c
x : σ → R
hx : ∀ (i : σ), x i ∈ S i
h₁ :
  ∀ x_1 ∈ h.support,
    Eq.{u_1 + 1} (α := R)
      ((eval x : (a : MvPolynomial σ R) → R)
          (HSMul.hSMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
            ((h : (a : σ) → MvPolynomial σ R) x_1 : MvPolynomial σ R) (Alon.P (S x_1) x_1)) :
        R)
      (0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) r : R) (0 : R)

Tactic:
rw [← hf, map_sub, Heval x hx, zero_sub, neg_eq_zero,
      linearCombination_apply, map_finsuppSum, Finsupp.sum, Finset.sum_eq_zero]

Premises used: map_sub, Finset.sum_eq_zero, Finsupp.sum, neg_eq_zero, Finsupp.linearCombination_apply, map_finsuppSum, zero_sub
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_2
inst_1 : Finite σ
inst_2 : IsDomain R
S : σ → Finset R
Sne : ∀ (i : σ), (S i).Nonempty
f : MvPolynomial σ R
Heval :
  ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) f : R) (0 : R)
this : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
h : σ →₀ MvPolynomial σ R
r : MvPolynomial σ R
hf :
  HSub.hSub (β := MvPolynomial σ R) f
      ((linearCombination (MvPolynomial σ R) fun (i : σ) ↦ Alon.P (S i) i :
            (a : σ →₀ MvPolynomial σ R) → MvPolynomial σ R)
          h :
        MvPolynomial σ R) =
    r
hh :
  ∀ (i : σ),
    LE.le (α := syn (σ := σ) degLex)
      ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn)
          (MonomialOrder.degree degLex
            (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (Alon.P (S i) i)
              ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R))) :
        syn (σ := σ) degLex)
      ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn) (MonomialOrder.degree degLex f) : syn (σ := σ) degLex)
hr : ∀ c ∈ r.support, ∀ (i : σ), ¬MonomialOrder.degree degLex (Alon.P (S i) i) ≤ c
x : σ → R
hx : ∀ (i : σ), x i ∈ S i
i : σ
h₁ :
  i ∈ h.support →
    Eq.{u_1 + 1} (α := R)
      ((eval x : (a : MvPolynomial σ R) → R)
          (HSMul.hSMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
            ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R) (Alon.P (S i) i)) :
        R)
      (0 : R)
⊢ i ∈ h.support →
    Eq.{u_1 + 1} (α := R)
      ((eval x : (a : MvPolynomial σ R) → R)
          (HSMul.hSMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
            ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R) (Alon.P (S i) i)) :
        R)
      (0 : R)

Tactic:
_
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_2
inst_1 : Finite σ
inst_2 : IsDomain R
S : σ → Finset R
Sne : ∀ (i : σ), (S i).Nonempty
f : MvPolynomial σ R
Heval :
  ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) f : R) (0 : R)
this : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
h : σ →₀ MvPolynomial σ R
r : MvPolynomial σ R
hf :
  HSub.hSub (β := MvPolynomial σ R) f
      ((linearCombination (MvPolynomial σ R) fun (i : σ) ↦ Alon.P (S i) i :
            (a : σ →₀ MvPolynomial σ R) → MvPolynomial σ R)
          h :
        MvPolynomial σ R) =
    r
hh :
  ∀ (i : σ),
    LE.le (α := syn (σ := σ) degLex)
      ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn)
          (MonomialOrder.degree degLex
            (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (Alon.P (S i) i)
              ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R))) :
        syn (σ := σ) degLex)
      ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn) (MonomialOrder.degree degLex f) : syn (σ := σ) degLex)
hr : ∀ c ∈ r.support, ∀ (i : σ), ¬MonomialOrder.degree degLex (Alon.P (S i) i) ≤ c
x : σ → R
hx : ∀ (i : σ), x i ∈ S i
i : σ
h_1 : i ∈ h.support
h₁ :
  HMul.hMul (α := R) (β := R)
      ((eval x : (a : MvPolynomial σ R) → R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R) : R)
      ((eval x : (a : MvPolynomial σ R) → R) (Alon.P (S i) i) : R) =
    0
⊢ Eq.{u_1 + 1} (α := R)
    ((eval x : (a : MvPolynomial σ R) → R)
        (HSMul.hSMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
          ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R) (Alon.P (S i) i)) :
      R)
    (0 : R)

Tactic:
rw [smul_eq_mul, map_mul]

Premises used: map_mul, smul_eq_mul
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_2
inst_1 : Finite σ
inst_2 : IsDomain R
S : σ → Finset R
Sne : ∀ (i : σ), (S i).Nonempty
f : MvPolynomial σ R
Heval :
  ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) f : R) (0 : R)
this : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
h : σ →₀ MvPolynomial σ R
r : MvPolynomial σ R
hf :
  HSub.hSub (β := MvPolynomial σ R) f
      ((linearCombination (MvPolynomial σ R) fun (i : σ) ↦ Alon.P (S i) i :
            (a : σ →₀ MvPolynomial σ R) → MvPolynomial σ R)
          h :
        MvPolynomial σ R) =
    r
hh :
  ∀ (i : σ),
    LE.le (α := syn (σ := σ) degLex)
      ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn)
          (MonomialOrder.degree degLex
            (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (Alon.P (S i) i)
              ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R))) :
        syn (σ := σ) degLex)
      ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn) (MonomialOrder.degree degLex f) : syn (σ := σ) degLex)
hr : ∀ c ∈ r.support, ∀ (i : σ), ¬MonomialOrder.degree degLex (Alon.P (S i) i) ≤ c
x : σ → R
hx : ∀ (i : σ), x i ∈ S i
i : σ
h_1 : i ∈ h.support
⊢ HMul.hMul (α := R) (β := R)
      ((eval x : (a : MvPolynomial σ R) → R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R) : R) (0 : R) =
    0

Tactic:
mul_zero _

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_2
inst_1 : Finite σ
inst_2 : IsDomain R
S : σ → Finset R
Sne : ∀ (i : σ), (S i).Nonempty
f : MvPolynomial σ R
Heval :
  ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) f : R) (0 : R)
this : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
h : σ →₀ MvPolynomial σ R
r : MvPolynomial σ R
hf :
  HSub.hSub (β := MvPolynomial σ R) f
      ((linearCombination (MvPolynomial σ R) fun (i : σ) ↦ Alon.P (S i) i :
            (a : σ →₀ MvPolynomial σ R) → MvPolynomial σ R)
          h :
        MvPolynomial σ R) =
    r
hh :
  ∀ (i : σ),
    LE.le (α := syn (σ := σ) degLex)
      ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn)
          (MonomialOrder.degree degLex
            (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (Alon.P (S i) i)
              ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R))) :
        syn (σ := σ) degLex)
      ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn) (MonomialOrder.degree degLex f) : syn (σ := σ) degLex)
hr : ∀ c ∈ r.support, ∀ (i : σ), ¬MonomialOrder.degree degLex (Alon.P (S i) i) ≤ c
x : σ → R
hx : ∀ (i : σ), x i ∈ S i
i : σ
h_1 : i ∈ h.support
h₁ : Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) (Alon.P (S i) i) : R) (0 : R)
⊢ HMul.hMul (α := R) (β := R)
      ((eval x : (a : MvPolynomial σ R) → R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R) : R)
      ((eval x : (a : MvPolynomial σ R) → R) (Alon.P (S i) i) : R) =
    0

Tactic:
convert! mul_zero _

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_2
inst_1 : Finite σ
inst_2 : IsDomain R
S : σ → Finset R
Sne : ∀ (i : σ), (S i).Nonempty
f : MvPolynomial σ R
Heval :
  ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) f : R) (0 : R)
this : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
h : σ →₀ MvPolynomial σ R
r : MvPolynomial σ R
hf :
  HSub.hSub (β := MvPolynomial σ R) f
      ((linearCombination (MvPolynomial σ R) fun (i : σ) ↦ Alon.P (S i) i :
            (a : σ →₀ MvPolynomial σ R) → MvPolynomial σ R)
          h :
        MvPolynomial σ R) =
    r
hh :
  ∀ (i : σ),
    LE.le (α := syn (σ := σ) degLex)
      ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn)
          (MonomialOrder.degree degLex
            (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (Alon.P (S i) i)
              ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R))) :
        syn (σ := σ) degLex)
      ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn) (MonomialOrder.degree degLex f) : syn (σ := σ) degLex)
hr : ∀ c ∈ r.support, ∀ (i : σ), ¬MonomialOrder.degree degLex (Alon.P (S i) i) ≤ c
x : σ → R
hx : ∀ (i : σ), x i ∈ S i
i : σ
h_1 : i ∈ h.support
h₁ :
  Eq (α := R)
    (∏ x_1 ∈ S i,
      (eval x : (a : MvPolynomial σ R) → R)
        (HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((C : (a : R) → MvPolynomial σ R) x_1 : MvPolynomial σ R)))
    0
⊢ Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) (Alon.P (S i) i) : R) (0 : R)

Tactic:
rw [Alon.P, _root_.map_prod]

Premises used: map_prod, _private.0.MvPolynomial.Alon.P
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_2
inst_1 : Finite σ
inst_2 : IsDomain R
S : σ → Finset R
Sne : ∀ (i : σ), (S i).Nonempty
f : MvPolynomial σ R
Heval :
  ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) f : R) (0 : R)
this : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
h : σ →₀ MvPolynomial σ R
r : MvPolynomial σ R
hf :
  HSub.hSub (β := MvPolynomial σ R) f
      ((linearCombination (MvPolynomial σ R) fun (i : σ) ↦ Alon.P (S i) i :
            (a : σ →₀ MvPolynomial σ R) → MvPolynomial σ R)
          h :
        MvPolynomial σ R) =
    r
hh :
  ∀ (i : σ),
    LE.le (α := syn (σ := σ) degLex)
      ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn)
          (MonomialOrder.degree degLex
            (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (Alon.P (S i) i)
              ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R))) :
        syn (σ := σ) degLex)
      ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn) (MonomialOrder.degree degLex f) : syn (σ := σ) degLex)
hr : ∀ c ∈ r.support, ∀ (i : σ), ¬MonomialOrder.degree degLex (Alon.P (S i) i) ≤ c
x : σ → R
hx : ∀ (i : σ), x i ∈ S i
i : σ
h_1 : i ∈ h.support
h₁ :
  Eq.{u_1 + 1} (α := R)
    ((eval x : (a : MvPolynomial σ R) → R)
        (HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((C : (a : R) → MvPolynomial σ R) (x i) : MvPolynomial σ R)) :
      R)
    (0 : R)
⊢ Eq (α := R)
    (∏ x_1 ∈ S i,
      (eval x : (a : MvPolynomial σ R) → R)
        (HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((C : (a : R) → MvPolynomial σ R) x_1 : MvPolynomial σ R)))
    0

Tactic:
apply Finset.prod_eq_zero (hx i)

Premises used: Finset.prod_eq_zero
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_2
inst_1 : Finite σ
inst_2 : IsDomain R
S : σ → Finset R
Sne : ∀ (i : σ), (S i).Nonempty
f : MvPolynomial σ R
Heval :
  ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) f : R) (0 : R)
this : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
h : σ →₀ MvPolynomial σ R
r : MvPolynomial σ R
hf :
  HSub.hSub (β := MvPolynomial σ R) f
      ((linearCombination (MvPolynomial σ R) fun (i : σ) ↦ Alon.P (S i) i :
            (a : σ →₀ MvPolynomial σ R) → MvPolynomial σ R)
          h :
        MvPolynomial σ R) =
    r
hh :
  ∀ (i : σ),
    LE.le (α := syn (σ := σ) degLex)
      ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn)
          (MonomialOrder.degree degLex
            (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (Alon.P (S i) i)
              ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R))) :
        syn (σ := σ) degLex)
      ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn) (MonomialOrder.degree degLex f) : syn (σ := σ) degLex)
hr : ∀ c ∈ r.support, ∀ (i : σ), ¬MonomialOrder.degree degLex (Alon.P (S i) i) ≤ c
x : σ → R
hx : ∀ (i : σ), x i ∈ S i
i : σ
h_1 : i ∈ h.support
⊢ Eq.{u_1 + 1} (α := R)
    ((eval x : (a : MvPolynomial σ R) → R)
        (HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((C : (a : R) → MvPolynomial σ R) (x i) : MvPolynomial σ R)) :
      R)
    (0 : R)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_2
inst_1 : Finite σ
inst_2 : IsDomain R
f : MvPolynomial σ R
t : σ →₀ ℕ
ht : coeff t f ≠ 0
ht' : f.totalDegree = (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) t
S : σ → Finset R
htS : ∀ (i : σ), (t : (a : σ) → ℕ) i < #(S i)
x : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
by_contra! :
  ∀
    (Heval :
      ∀ (s : σ → R) (_ : ∀ (i : σ), s i ∈ S i),
        Eq.{u_1 + 1} (α := R) ((eval s : (a : MvPolynomial σ R) → R) f : R) (0 : R)),
    False
⊢ ∃ (s : σ → R), (∀ (i : σ), s i ∈ S i) ∧ Ne.{u_1 + 1} (α := R) ((eval s : (a : MvPolynomial σ R) → R) f : R) (0 : R)

Tactic:
by_contra! Heval
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_2
inst_1 : Finite σ
inst_2 : IsDomain R
f : MvPolynomial σ R
t : σ →₀ ℕ
ht : coeff t f ≠ 0
ht' : f.totalDegree = (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) t
S : σ → Finset R
htS : ∀ (i : σ), (t : (a : σ) → ℕ) i < #(S i)
x : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
Heval :
  ∀ (s : σ → R) (_ : ∀ (i : σ), s i ∈ S i), Eq.{u_1 + 1} (α := R) ((eval s : (a : MvPolynomial σ R) → R) f : R) (0 : R)
apply : coeff t f = 0
⊢ False

Tactic:
apply ht
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_2
inst_1 : Finite σ
inst_2 : IsDomain R
f : MvPolynomial σ R
t : σ →₀ ℕ
ht : coeff t f ≠ 0
ht' : f.totalDegree = (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) t
S : σ → Finset R
htS : ∀ (i : σ), (t : (a : σ) → ℕ) i < #(S i)
x : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
Heval :
  ∀ (s : σ → R) (_ : ∀ (i : σ), s i ∈ S i), Eq.{u_1 + 1} (α := R) ((eval s : (a : MvPolynomial σ R) → R) f : R) (0 : R)
i : σ
rw : 0 < #(S i)
⊢ (S i).Nonempty

Tactic:
rw [← Finset.card_pos]

Premises used: Finset.card_pos
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_2
inst_1 : Finite σ
inst_2 : IsDomain R
f : MvPolynomial σ R
t : σ →₀ ℕ
ht : coeff t f ≠ 0
ht' : f.totalDegree = (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) t
S : σ → Finset R
htS : ∀ (i : σ), (t : (a : σ) → ℕ) i < #(S i)
x : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
Heval :
  ∀ (s : σ → R) (_ : ∀ (i : σ), s i ∈ S i), Eq.{u_1 + 1} (α := R) ((eval s : (a : MvPolynomial σ R) → R) f : R) (0 : R)
i : σ
⊢ 0 < #(S i)

Tactic:
Nat.zero_lt_of_lt (htS i)

Premises used: Nat.zero_lt_of_lt
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_2
inst_1 : Finite σ
inst_2 : IsDomain R
f : MvPolynomial σ R
t : σ →₀ ℕ
ht : coeff t f ≠ 0
ht' : f.totalDegree = (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) t
S : σ → Finset R
htS : ∀ (i : σ), (t : (a : σ) → ℕ) i < #(S i)
x : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
Heval :
  ∀ (s : σ → R) (_ : ∀ (i : σ), s i ∈ S i), Eq.{u_1 + 1} (α := R) ((eval s : (a : MvPolynomial σ R) → R) f : R) (0 : R)
i : σ
⊢ 0 < #(S i)

Tactic:
exact Nat.zero_lt_of_lt (htS i)

Premises used: Nat.zero_lt_of_lt