awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hP :
  Eq (α := MvPolynomial ι R) (P S i)
    ((rename fun (x : Unit) ↦ i : (a : MvPolynomial Unit R) → MvPolynomial ι R) (P S ()))
e : Unit →₀ ℕ
he : ¬coeff e (P S ()) = 0
hm : mapDomain (fun (x : Unit) ↦ i) e = m
this : Nontrivial R
j : ι
pos :
  ∀ (hj : j = i),
    Eq (α := ℕ) ((mapDomain (fun (x : Unit) ↦ i) e : (a : ι) → ℕ) j : ℕ)
      (((single i ((e : (a : Unit) → ℕ) ()) : ι →₀ ℕ) : (a : ι) → ℕ) j : ℕ)
neg :
  ∀ (hj : ¬j = i),
    Eq (α := ℕ) ((mapDomain (fun (x : Unit) ↦ i) e : (a : ι) → ℕ) j : ℕ)
      (((single i ((e : (a : Unit) → ℕ) ()) : ι →₀ ℕ) : (a : ι) → ℕ) j : ℕ)
⊢ Eq (α := ℕ) ((mapDomain (fun (x : Unit) ↦ i) e : (a : ι) → ℕ) j : ℕ)
    (((single i ((e : (a : Unit) → ℕ) ()) : ι →₀ ℕ) : (a : ι) → ℕ) j : ℕ)

Tactic:
by_cases hj : j = i
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hP :
  Eq (α := MvPolynomial ι R) (P S i)
    ((rename fun (x : Unit) ↦ i : (a : MvPolynomial Unit R) → MvPolynomial ι R) (P S ()))
e : Unit →₀ ℕ
he : ¬coeff e (P S ()) = 0
hm : mapDomain (fun (x : Unit) ↦ i) e = m
this : Nontrivial R
j : ι
hj : j = i
pos :
  Eq (α := ℕ) ((mapDomain (fun (x : Unit) ↦ i) e : (a : ι) → ℕ) i : ℕ)
    (((single i ((e : (a : Unit) → ℕ) ()) : ι →₀ ℕ) : (a : ι) → ℕ) i : ℕ)
pos₁ : Eq (α := ℕ) ((e : (a : Unit) → ℕ) () : ℕ) (((single i ((e : (a : Unit) → ℕ) ()) : ι →₀ ℕ) : (a : ι) → ℕ) i : ℕ)
pos₂ : Unit
pos₃ : Eq (α := ℕ) ((e : (a : Unit) → ℕ) () : ℕ) ((e : (a : Unit) → ℕ) () : ℕ)
pos₄ : Unit
pos₅ : Eq (α := ℕ) ((e : (a : Unit) → ℕ) () : ℕ) ((e : (a : Unit) → ℕ) () : ℕ)
pos₆ : Unit
⊢ Eq (α := ℕ) ((mapDomain (fun (x : Unit) ↦ i) e : (a : ι) → ℕ) j : ℕ)
    (((single i ((e : (a : Unit) → ℕ) ()) : ι →₀ ℕ) : (a : ι) → ℕ) j : ℕ)

Tactic:
rw [hj, mapDomain_apply (Function.injective_of_subsingleton _), single_eq_same]

Premises used: Finsupp.single_eq_same, Function.injective_of_subsingleton, Finsupp.mapDomain_apply
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hP :
  Eq (α := MvPolynomial ι R) (P S i)
    ((rename fun (x : Unit) ↦ i : (a : MvPolynomial Unit R) → MvPolynomial ι R) (P S ()))
e : Unit →₀ ℕ
he : ¬coeff e (P S ()) = 0
hm : mapDomain (fun (x : Unit) ↦ i) e = m
this : Nontrivial R
j : ι
hj : ¬j = i
neg : j ∉ Set.range fun (x : Unit) ↦ i
⊢ Eq (α := ℕ) ((mapDomain (fun (x : Unit) ↦ i) e : (a : ι) → ℕ) j : ℕ)
    (((single i ((e : (a : Unit) → ℕ) ()) : ι →₀ ℕ) : (a : ι) → ℕ) j : ℕ)

Tactic:
rw [mapDomain_notin_range, single_eq_of_ne hj]

Premises used: Finsupp.single_eq_of_ne, Finsupp.mapDomain_notin_range
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hP :
  Eq (α := MvPolynomial ι R) (P S i)
    ((rename fun (x : Unit) ↦ i : (a : MvPolynomial Unit R) → MvPolynomial ι R) (P S ()))
e : Unit →₀ ℕ
he : ¬coeff e (P S ()) = 0
hm : mapDomain (fun (x : Unit) ↦ i) e = m
this : Nontrivial R
j : ι
hj : ¬j = i
⊢ j ∉ Set.range fun (x : Unit) ↦ i

Tactic:
simp [Set.range_const, Set.mem_singleton_iff, hj]

Premises used: Set.mem_singleton_iff, Set.range_const
-- 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
i : σ
⊢ IsUnit.{u_1} (M := R)
    (leadingCoeff.{u_2, u_1, u_2} (σ := σ) degLex ((fun (i : σ) ↦ (Alon.P (S i) i : MvPolynomial σ R)) i))

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

Premises used: MonomialOrder.Monic.leadingCoeff_eq_one, _private.0.MvPolynomial.Alon.monic_P, isUnit_one
-- 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
obtain :
  ∀ (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),
    ∃ (h : σ →₀ MvPolynomial σ R),
      (∀ (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) ∧
        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
⊢ ∃ (h : σ →₀ MvPolynomial σ R),
    (∀ (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) ∧
      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

Tactic:
obtain ⟨h, r, hf, hh, hr⟩ := degLex.div (b := fun i ↦ Alon.P (S i) i)
      (fun i ↦ by simp only [(Alon.monic_P ..).leadingCoeff_eq_one, isUnit_one]) f

Premises used: MonomialOrder.div
-- 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
h₁ :
  (∀ (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) ∧
    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
⊢ ∃ (h : σ →₀ MvPolynomial σ R),
    (∀ (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) ∧
      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

Tactic:
use h
-- 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_1 : 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
this : r = 0
⊢ f =
    (linearCombination (MvPolynomial σ R) fun (i : σ) ↦ Alon.P (S i) i : (a : σ →₀ MvPolynomial σ R) → MvPolynomial σ R)
      h

Tactic:
rw [this, add_zero] at hf

Premises used: add_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_1 : 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
this : r = 0
hf₁ :
  f =
    (linearCombination (MvPolynomial σ R) fun (i : σ) ↦ Alon.P (S i) i : (a : σ →₀ MvPolynomial σ R) → MvPolynomial σ R)
      h
⊢ ∀ (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)

Tactic:
rw [this, add_zero] at hf

Premises used: add_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_1 : 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
this : r = 0
hf₁ :
  f =
    (linearCombination (MvPolynomial σ R) fun (i : σ) ↦ Alon.P (S i) i : (a : σ →₀ MvPolynomial σ R) → MvPolynomial σ R)
      h
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)
⊢ ∀ c ∈ r.support, ∀ (i : σ), ¬MonomialOrder.degree degLex (Alon.P (S i) i) ≤ c

Tactic:
rw [this, add_zero] at hf

Premises used: add_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_1 : 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
this : r = 0
hf₁ :
  f =
    (linearCombination (MvPolynomial σ R) fun (i : σ) ↦ Alon.P (S i) i : (a : σ →₀ MvPolynomial σ R) → MvPolynomial σ R)
      h
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
⊢ r = 0

Tactic:
rw [this, add_zero] at hf

Premises used: add_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_1 : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
h : σ →₀ MvPolynomial σ R
r : MvPolynomial σ R
hf :
  f =
    (linearCombination (MvPolynomial σ R) fun (i : σ) ↦ Alon.P (S i) i : (a : σ →₀ MvPolynomial σ R) → MvPolynomial σ R)
      h
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
this : r = 0
⊢ (∀ (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) ∧
    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

Tactic:
⟨fun i ↦ degLex_totalDegree_monotone (hh i), hf⟩

Premises used: And.intro, MvPolynomial.degLex_totalDegree_monotone
-- 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_1 : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
h : σ →₀ MvPolynomial σ R
r : MvPolynomial σ R
hf :
  f =
    (linearCombination (MvPolynomial σ R) fun (i : σ) ↦ Alon.P (S i) i : (a : σ →₀ MvPolynomial σ R) → MvPolynomial σ R)
      h
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
this : r = 0
⊢ (∀ (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) ∧
    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

Tactic:
exact ⟨fun i ↦ degLex_totalDegree_monotone (hh i), hf⟩
-- 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
h₁ : r = 0
⊢ (∀ (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) ∧
    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

Tactic:
suffices r = 0 by
    rw [this, add_zero] at hf
    exact ⟨fun i ↦ degLex_totalDegree_monotone (hh i), hf⟩
-- 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
h₁ : ∀ (i : σ), degreeOf i r < #(S i)
h₂ : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) r : R) (0 : R)
⊢ r = 0

Tactic:
apply eq_zero_of_eval_zero_at_prod_finset r S

Premises used: MvPolynomial.eq_zero_of_eval_zero_at_prod_finset