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
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)
h : σ →₀ MvPolynomial σ R
hh :
  ∀ (i : σ),
    (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
          (∏ s ∈ S i,
              HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
                ((C : (a : R) → MvPolynomial σ R) s : MvPolynomial σ R) :
            MvPolynomial σ R)
          ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)).totalDegree ≤
      f.totalDegree
hf :
  f =
    (linearCombination (MvPolynomial σ R) fun (i : σ) ↦
          ∏ r ∈ S i,
            HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
              ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) :
        (a : σ →₀ MvPolynomial σ R) → MvPolynomial σ R)
      h
i : σ
h_1 : i ∈ h.support
g : MvPolynomial σ R :=
  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)
    (Alon.P (S i) i)
hg :
  g =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)
      (Alon.P (S i) i)
hi : ¬Eq (α := MvPolynomial σ R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R) (0 : MvPolynomial σ R)
this :
  (Finsupp.degree : (a : σ →₀ ℕ) → ℕ)
      (MonomialOrder.degree degLex
        (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
          ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R) (Alon.P (S i) i))) ≤
    f.totalDegree
⊢ IsRegular (leadingCoeff degLex (Alon.P (S i) i))

Tactic:
simp only [(Alon.monic_P ..).leadingCoeff_eq_one,
      isRegular_one]

Premises used: MonomialOrder.Monic.leadingCoeff_eq_one, _private.0.MvPolynomial.Alon.monic_P, isRegular_one
-- 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)
h : σ →₀ MvPolynomial σ R
hh :
  ∀ (i : σ),
    (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
          (∏ s ∈ S i,
              HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
                ((C : (a : R) → MvPolynomial σ R) s : MvPolynomial σ R) :
            MvPolynomial σ R)
          ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)).totalDegree ≤
      f.totalDegree
hf :
  f =
    (linearCombination (MvPolynomial σ R) fun (i : σ) ↦
          ∏ r ∈ S i,
            HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
              ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) :
        (a : σ →₀ MvPolynomial σ R) → MvPolynomial σ R)
      h
i : σ
h_1 : i ∈ h.support
g : MvPolynomial σ R :=
  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)
    (Alon.P (S i) i)
hg :
  g =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)
      (Alon.P (S i) i)
hi : ¬Eq (α := MvPolynomial σ R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R) (0 : MvPolynomial σ R)
this : g.totalDegree ≤ f.totalDegree
⊢ totalDegree.{u_1, u_2} (R := R) (σ := σ) ((h : (a : σ) → MvPolynomial σ R) i) + #(S i) ≤
    (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) t

Tactic:
rw [hg, ← degree_degLexDegree,
    degree_mul_of_isRegular_right hi (by simp only [(Alon.monic_P ..).leadingCoeff_eq_one,
      isRegular_one]),
    Alon.degree_P, map_add, degree_degLexDegree, degree_single, ht'] at this

Premises used: map_add, MonomialOrder.degree_mul_of_isRegular_right, MvPolynomial.degree_degLexDegree, Finsupp.degree_single, _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
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)
h : σ →₀ MvPolynomial σ R
hh :
  ∀ (i : σ),
    (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
          (∏ s ∈ S i,
              HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
                ((C : (a : R) → MvPolynomial σ R) s : MvPolynomial σ R) :
            MvPolynomial σ R)
          ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)).totalDegree ≤
      f.totalDegree
hf :
  f =
    (linearCombination (MvPolynomial σ R) fun (i : σ) ↦
          ∏ r ∈ S i,
            HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
              ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) :
        (a : σ →₀ MvPolynomial σ R) → MvPolynomial σ R)
      h
i : σ
h_1 : i ∈ h.support
g : MvPolynomial σ R :=
  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)
    (Alon.P (S i) i)
hg :
  g =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)
      (Alon.P (S i) i)
hi : ¬Eq (α := MvPolynomial σ R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R) (0 : MvPolynomial σ R)
this :
  totalDegree.{u_1, u_2} (R := R) (σ := σ) ((h : (a : σ) → MvPolynomial σ R) i) + #(S i) ≤
    (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) t
neg :
  ∀ x_1 ∈ @Finset.antidiagonal _ instAddMonoid _ t,
    HMul.hMul (α := R) (coeff x_1.1 ((h : (a : σ) → MvPolynomial σ R) i))
        (coeff x_1.2
          (∏ r ∈ S i,
            HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
              ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R))) =
      0
⊢ coeff t
      (HSMul.hSMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
        ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)
        (∏ r ∈ S i,
          HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
            ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R))) =
    0

Tactic:
rw [smul_eq_mul, coeff_mul, Finset.sum_eq_zero]

Premises used: Finset.sum_eq_zero, smul_eq_mul, MvPolynomial.coeff_mul
-- 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)
h : σ →₀ MvPolynomial σ R
hh :
  ∀ (i : σ),
    (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
          (∏ s ∈ S i,
              HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
                ((C : (a : R) → MvPolynomial σ R) s : MvPolynomial σ R) :
            MvPolynomial σ R)
          ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)).totalDegree ≤
      f.totalDegree
hf :
  f =
    (linearCombination (MvPolynomial σ R) fun (i : σ) ↦
          ∏ r ∈ S i,
            HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
              ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) :
        (a : σ →₀ MvPolynomial σ R) → MvPolynomial σ R)
      h
i : σ
h_1 : i ∈ h.support
g : MvPolynomial σ R :=
  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)
    (Alon.P (S i) i)
hg :
  g =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)
      (Alon.P (S i) i)
hi : ¬Eq (α := MvPolynomial σ R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R) (0 : MvPolynomial σ R)
this :
  totalDegree.{u_1, u_2} (R := R) (σ := σ) ((h : (a : σ) → MvPolynomial σ R) i) + #(S i) ≤
    (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) t
p q : σ →₀ ℕ
hpq : (p, q) ∈ @Finset.antidiagonal _ instAddMonoid _ t
⊢ p + q = t

Tactic:
simp only [Finset.mem_antidiagonal] at hpq

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- 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)
h : σ →₀ MvPolynomial σ R
hh :
  ∀ (i : σ),
    (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
          (∏ s ∈ S i,
              HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
                ((C : (a : R) → MvPolynomial σ R) s : MvPolynomial σ R) :
            MvPolynomial σ R)
          ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)).totalDegree ≤
      f.totalDegree
hf :
  f =
    (linearCombination (MvPolynomial σ R) fun (i : σ) ↦
          ∏ r ∈ S i,
            HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
              ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) :
        (a : σ →₀ MvPolynomial σ R) → MvPolynomial σ R)
      h
i : σ
h_1 : i ∈ h.support
g : MvPolynomial σ R :=
  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)
    (Alon.P (S i) i)
hg :
  g =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)
      (Alon.P (S i) i)
hi : ¬Eq (α := MvPolynomial σ R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R) (0 : MvPolynomial σ R)
this :
  totalDegree.{u_1, u_2} (R := R) (σ := σ) ((h : (a : σ) → MvPolynomial σ R) i) + #(S i) ≤
    (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) t
p q : σ →₀ ℕ
hpq : p + q = t
neg :
  ¬Eq.{u_1 + 1} (α := R)
        (coeff q
          (∏ r ∈ S i,
            HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
              ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)))
        0 →
    Eq.{u_1 + 1} (α := R) (coeff p ((h : (a : σ) → MvPolynomial σ R) i)) 0
⊢ HMul.hMul (α := R) (coeff (p, q).1 ((h : (a : σ) → MvPolynomial σ R) i))
      (coeff (p, q).2
        (∏ r ∈ S i,
          HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
            ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R))) =
    0

Tactic:
simp only [mul_eq_zero, Classical.or_iff_not_imp_right]

Premises used: Classical.or_iff_not_imp_right, mul_eq_zero
-- 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)
h : σ →₀ MvPolynomial σ R
hh :
  ∀ (i : σ),
    (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
          (∏ s ∈ S i,
              HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
                ((C : (a : R) → MvPolynomial σ R) s : MvPolynomial σ R) :
            MvPolynomial σ R)
          ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)).totalDegree ≤
      f.totalDegree
hf :
  f =
    (linearCombination (MvPolynomial σ R) fun (i : σ) ↦
          ∏ r ∈ S i,
            HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
              ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) :
        (a : σ →₀ MvPolynomial σ R) → MvPolynomial σ R)
      h
i : σ
h_1 : i ∈ h.support
g : MvPolynomial σ R :=
  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)
    (Alon.P (S i) i)
hg :
  g =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)
      (Alon.P (S i) i)
hi : ¬Eq (α := MvPolynomial σ R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R) (0 : MvPolynomial σ R)
this :
  totalDegree.{u_1, u_2} (R := R) (σ := σ) ((h : (a : σ) → MvPolynomial σ R) i) + #(S i) ≤
    (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) t
p q : σ →₀ ℕ
hpq : p + q = t
neg :
  Membership.mem (γ := Finset (σ →₀ ℕ))
      (support.{u_1, u_2} (R := R)
        (∏ r ∈ S i,
          HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
            ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)))
      q →
    Eq.{u_1 + 1} (α := R) (coeff p ((h : (a : σ) → MvPolynomial σ R) i)) 0
⊢ ¬Eq.{u_1 + 1} (α := R)
        (coeff q
          (∏ r ∈ S i,
            HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
              ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)))
        0 →
    Eq.{u_1 + 1} (α := R) (coeff p ((h : (a : σ) → MvPolynomial σ R) i)) 0

Tactic:
rw [← ne_eq, ← mem_support_iff]

Premises used: MvPolynomial.mem_support_iff, ne_eq
-- 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)
h : σ →₀ MvPolynomial σ R
hh :
  ∀ (i : σ),
    (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
          (∏ s ∈ S i,
              HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
                ((C : (a : R) → MvPolynomial σ R) s : MvPolynomial σ R) :
            MvPolynomial σ R)
          ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)).totalDegree ≤
      f.totalDegree
hf :
  f =
    (linearCombination (MvPolynomial σ R) fun (i : σ) ↦
          ∏ r ∈ S i,
            HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
              ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) :
        (a : σ →₀ MvPolynomial σ R) → MvPolynomial σ R)
      h
i : σ
h_1 : i ∈ h.support
g : MvPolynomial σ R :=
  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)
    (Alon.P (S i) i)
hg :
  g =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)
      (Alon.P (S i) i)
hi : ¬Eq (α := MvPolynomial σ R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R) (0 : MvPolynomial σ R)
this :
  totalDegree.{u_1, u_2} (R := R) (σ := σ) ((h : (a : σ) → MvPolynomial σ R) i) + #(S i) ≤
    (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) t
p q : σ →₀ ℕ
hpq : p + q = t
hq :
  Membership.mem (γ := Finset (σ →₀ ℕ))
    (support.{u_1, u_2} (R := R)
      (∏ r ∈ S i,
        HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)))
    q
neg :
  ∀ (e : ℕ) (hq' : e ≤ #(S i)) (hq : q = single i e),
    Eq.{u_1 + 1} (α := R) (coeff p ((h : (a : σ) → MvPolynomial σ R) i)) 0
⊢ Eq.{u_1 + 1} (α := R) (coeff p ((h : (a : σ) → MvPolynomial σ R) i)) 0

Tactic:
obtain ⟨e, hq', hq⟩ := Alon.of_mem_P_support _ _ _ hq

Premises used: _private.0.MvPolynomial.Alon.of_mem_P_support
-- 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)
h : σ →₀ MvPolynomial σ R
hh :
  ∀ (i : σ),
    (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
          (∏ s ∈ S i,
              HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
                ((C : (a : R) → MvPolynomial σ R) s : MvPolynomial σ R) :
            MvPolynomial σ R)
          ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)).totalDegree ≤
      f.totalDegree
hf :
  f =
    (linearCombination (MvPolynomial σ R) fun (i : σ) ↦
          ∏ r ∈ S i,
            HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
              ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) :
        (a : σ →₀ MvPolynomial σ R) → MvPolynomial σ R)
      h
i : σ
h_1 : i ∈ h.support
g : MvPolynomial σ R :=
  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)
    (Alon.P (S i) i)
hg :
  g =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)
      (Alon.P (S i) i)
hi : ¬Eq (α := MvPolynomial σ R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R) (0 : MvPolynomial σ R)
this :
  totalDegree.{u_1, u_2} (R := R) (σ := σ) ((h : (a : σ) → MvPolynomial σ R) i) + #(S i) ≤
    (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) t
p q : σ →₀ ℕ
hpq : p + q = t
hq_1 :
  Membership.mem (γ := Finset (σ →₀ ℕ))
    (support.{u_1, u_2} (R := R)
      (∏ r ∈ S i,
        HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)))
    q
e : ℕ
hq' : e ≤ #(S i)
hq : q = single i e
neg :
  totalDegree.{u_1, u_2} (R := R) (σ := σ) ((h : (a : σ) → MvPolynomial σ R) i) < ∑ i ∈ p.support, (p : (a : σ) → ℕ) i
⊢ Eq.{u_1 + 1} (α := R) (coeff p ((h : (a : σ) → MvPolynomial σ R) i)) 0

Tactic:
apply coeff_eq_zero_of_totalDegree_lt

Premises used: MvPolynomial.coeff_eq_zero_of_totalDegree_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)
h : σ →₀ MvPolynomial σ R
hh :
  ∀ (i : σ),
    (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
          (∏ s ∈ S i,
              HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
                ((C : (a : R) → MvPolynomial σ R) s : MvPolynomial σ R) :
            MvPolynomial σ R)
          ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)).totalDegree ≤
      f.totalDegree
hf :
  f =
    (linearCombination (MvPolynomial σ R) fun (i : σ) ↦
          ∏ r ∈ S i,
            HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
              ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) :
        (a : σ →₀ MvPolynomial σ R) → MvPolynomial σ R)
      h
i : σ
h_1 : i ∈ h.support
g : MvPolynomial σ R :=
  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)
    (Alon.P (S i) i)
hg :
  g =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)
      (Alon.P (S i) i)
hi : ¬Eq (α := MvPolynomial σ R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R) (0 : MvPolynomial σ R)
this :
  totalDegree.{u_1, u_2} (R := R) (σ := σ) ((h : (a : σ) → MvPolynomial σ R) i) + #(S i) ≤
    (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) t
p q : σ →₀ ℕ
hpq : p + q = t
hq_1 :
  Membership.mem (γ := Finset (σ →₀ ℕ))
    (support.{u_1, u_2} (R := R)
      (∏ r ∈ S i,
        HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)))
    q
e : ℕ
hq' : e ≤ #(S i)
hq : q = single i e
neg :
  totalDegree.{u_1, u_2} (R := R) (σ := σ) ((h : (a : σ) → MvPolynomial σ R) i) < (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) p
⊢ totalDegree.{u_1, u_2} (R := R) (σ := σ) ((h : (a : σ) → MvPolynomial σ R) i) < ∑ i ∈ p.support, (p : (a : σ) → ℕ) i

Tactic:
rw [← Finsupp.degree_apply]

Premises used: Finsupp.degree_apply
-- 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)
h : σ →₀ MvPolynomial σ R
hh :
  ∀ (i : σ),
    (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
          (∏ s ∈ S i,
              HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
                ((C : (a : R) → MvPolynomial σ R) s : MvPolynomial σ R) :
            MvPolynomial σ R)
          ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)).totalDegree ≤
      f.totalDegree
hf :
  f =
    (linearCombination (MvPolynomial σ R) fun (i : σ) ↦
          ∏ r ∈ S i,
            HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
              ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) :
        (a : σ →₀ MvPolynomial σ R) → MvPolynomial σ R)
      h
i : σ
h_1 : i ∈ h.support
g : MvPolynomial σ R :=
  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)
    (Alon.P (S i) i)
hg :
  g =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)
      (Alon.P (S i) i)
hi : ¬Eq (α := MvPolynomial σ R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R) (0 : MvPolynomial σ R)
this :
  totalDegree.{u_1, u_2} (R := R) (σ := σ) ((h : (a : σ) → MvPolynomial σ R) i) + #(S i) ≤
    (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) t
p q : σ →₀ ℕ
hpq : p + q = t
hq_1 :
  Membership.mem (γ := Finset (σ →₀ ℕ))
    (support.{u_1, u_2} (R := R)
      (∏ r ∈ S i,
        HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)))
    q
e : ℕ
hq' : e ≤ #(S i)
hq : q = single i e
apply : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) t < HAdd.hAdd (α := ℕ) ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) p : ℕ) #(S i)
⊢ totalDegree.{u_1, u_2} (R := R) (σ := σ) ((h : (a : σ) → MvPolynomial σ R) i) < (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) p

Tactic:
apply lt_of_add_lt_add_right (lt_of_le_of_lt this _)

Premises used: lt_of_le_of_lt, lt_of_add_lt_add_right