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)
obtain :
  ∀ (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),
    coeff t f = 0
⊢ coeff t f = 0

Tactic:
obtain ⟨h, hh, hf⟩ := combinatorial_nullstellensatz_exists_linearCombination S
    (fun i ↦ by rw [← Finset.card_pos]; exact Nat.zero_lt_of_lt (htS i)) f Heval

Premises used: MvPolynomial.combinatorial_nullstellensatz_exists_linearCombination
-- 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
rw :
  Eq.{u_1 + 1} (α := R)
    (coeff t
      ((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))
    0
⊢ coeff t f = 0

Tactic:
rw [hf]
-- 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
rw :
  Eq.{u_1 + 1} (α := R)
    (∑ x ∈ h.support,
      coeff t
        (HSMul.hSMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
          ((h : (a : σ) → MvPolynomial σ R) x : MvPolynomial σ R)
          (∏ r ∈ S x,
            HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X x)
              ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R))))
    0
⊢ Eq.{u_1 + 1} (α := R)
    (coeff t
      ((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))
    0

Tactic:
rw [linearCombination_apply, Finsupp.sum, coeff_sum]

Premises used: Finsupp.sum, Finsupp.linearCombination_apply, MvPolynomial.coeff_sum
-- 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
h₁ :
  ∀ x ∈ h.support,
    coeff t
        (HSMul.hSMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
          ((h : (a : σ) → MvPolynomial σ R) x : MvPolynomial σ R)
          (∏ r ∈ S x,
            HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X x)
              ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R))) =
      0
⊢ Eq.{u_1 + 1} (α := R)
    (∑ x ∈ h.support,
      coeff t
        (HSMul.hSMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
          ((h : (a : σ) → MvPolynomial σ R) x : MvPolynomial σ R)
          (∏ r ∈ S x,
            HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X x)
              ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R))))
    0

Tactic:
apply Finset.sum_eq_zero

Premises used: Finset.sum_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₁ :
  i ∈ h.support →
    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
⊢ i ∈ h.support →
    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:
_
-- 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
⊢ let g :=
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)
      (Alon.P (S i) i);
  g =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)
      (Alon.P (S i) i)

Tactic:
set g := h i * Alon.P (S i) i with hg

Premises used: _private.0.MvPolynomial.Alon.P, DFunLike.coe
-- 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)
pos :
  ∀ (hi : Eq (α := MvPolynomial σ R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R) (0 : MvPolynomial σ R)),
    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
neg :
  ∀ (hi : ¬Eq (α := MvPolynomial σ R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R) (0 : MvPolynomial σ R)),
    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
⊢ 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:
by_cases hi : h i = 0

Premises used: DFunLike.coe
-- 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)
⊢ 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:
simp [hi]
-- 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)
rw :
  (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (Alon.P (S i) i)
        ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)).totalDegree ≤
    f.totalDegree
⊢ g.totalDegree ≤ f.totalDegree

Tactic:
rw [hg, mul_comm]

Premises used: mul_comm
-- 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)
⊢ (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (Alon.P (S i) i)
        ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)).totalDegree ≤
    f.totalDegree

Tactic:
hh i

Premises used: _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
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)
⊢ (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (Alon.P (S i) i)
        ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)).totalDegree ≤
    f.totalDegree

Tactic:
exact hh i
-- 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)
⊢ g.totalDegree ≤ f.totalDegree

Tactic:
have : g.totalDegree ≤ f.totalDegree := by
    rw [hg, mul_comm]
    exact hh i