awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
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)
      ((eval x : (a : MvPolynomial σ R) → R) (Alon.P (S i) i) : R) =
    0
have h₁ : Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) (Alon.P (S i) i) : R) (0 : R)
Tactic: convert! mul_zero _
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
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) (Alon.P (S i) i) : R) (0 : R)
have 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
Tactic: rw [Alon.P, _root_.map_prod]
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
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 (α := 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
have 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)
Tactic: apply Finset.prod_eq_zero (hx i)
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
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
⊢ ∃ (s : σ → R), (∀ (i : σ), s i ∈ S i) ∧ Ne.{u_1 + 1} (α := R) ((eval s : (a : MvPolynomial σ R) → R) f : R) (0 : R)
have 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
Tactic: by_contra! Heval
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
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)
⊢ False
have apply : coeff t f = 0
Tactic: apply ht
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
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 : σ
⊢ (S i).Nonempty
have rw : 0 < #(S i)
Tactic: rw [← Finset.card_pos]
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
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)
⊢ coeff t f = 0
have 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
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
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
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
⊢ coeff t f = 0
have 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
Tactic: rw [hf]
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
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
⊢ 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
have 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
Tactic: rw [linearCombination_apply, Finsupp.sum, coeff_sum]
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
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
⊢ 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
have 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
Tactic: apply Finset.sum_eq_zero
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (hypothesis)
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
⊢ 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
have hg : 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
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
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)
⊢ 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
have 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
Tactic: by_cases hi : h i = 0
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
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
⊢ 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
have 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
Tactic: by_cases hi : h i = 0
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
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
have rw : (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (Alon.P (S i) i)
      ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R)).totalDegree ≤
  f.totalDegree
Tactic: rw [hg, mul_comm]