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_3
i : ι
S : Finset R
m : ι →₀ ℕ
hm : m ∈ support (P S i)
have :
  Eq (α := MvPolynomial ι R) (P S i)
    ((rename fun (x : Unit) ↦ i : (a : MvPolynomial Unit R) → MvPolynomial ι R) (P S ()))
have₁ :
  ∀
    (hP :
      Eq (α := MvPolynomial ι R) (P S i)
        ((rename fun (x : Unit) ↦ i : (a : MvPolynomial Unit R) → MvPolynomial ι R) (P S ()))),
    ∃ e ≤ #S, m = single i e
have₂ :
  Eq (α := MvPolynomial ι R) (P S i)
    ((rename fun (x : Unit) ↦ i : (a : MvPolynomial Unit R) → MvPolynomial ι R) (P S ()))
have₃ have₄ :
  ∀
    (hP :
      Eq (α := MvPolynomial ι R) (P S i)
        ((rename fun (x : Unit) ↦ i : (a : MvPolynomial Unit R) → MvPolynomial ι R) (P S ()))),
    ∃ e ≤ #S, m = single i e
have₅ :
  ∀ (hm : Membership.mem (γ := Finset (ι →₀ ℕ)) (Finset.image (mapDomain fun (x : Unit) ↦ i) (support (P S ()))) m)
    (hP :
      Eq (α := MvPolynomial ι R) (P S i)
        ((rename fun (x : Unit) ↦ i : (a : MvPolynomial Unit R) → MvPolynomial ι R) (P S ()))),
    ∃ e ≤ #S, m = single i e
have₆ :
  ∀
    (hP :
      Eq (α := MvPolynomial ι R) (P S i)
        ((rename fun (x : Unit) ↦ i : (a : MvPolynomial Unit R) → MvPolynomial ι R) (P S ())))
    (hm : ∃ (a : Unit →₀ ℕ), ¬coeff a (P S ()) = 0 ∧ mapDomain (fun (x : Unit) ↦ i) a = m), ∃ e ≤ #S, m = single i e
have₇ :
  ∀
    (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), ∃ e ≤ #S, m = single i e
have₈ :
  ∀
    (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),
    ∃ e ≤ #S, m = single i e
⊢ ∃ e ≤ #S, m = single i e
have refine_1 : ∀
  (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),
  (e : (a : Unit) → ℕ) () ≤ #S
Tactic: classical
  have hP : Alon.P S i = .rename (fun _ ↦ i) (Alon.P S ()) := by simp [Alon.P]
  rw [hP, support_rename_of_injective (Function.injective_of_subsingleton _)] at hm
  simp only [Finset.mem_image, mem_support_iff, ne_eq] at hm
  obtain ⟨e, he, hm⟩ := hm
  haveI : Nontrivial R := nontrivial_of_ne _ _ he
  refine ⟨e (), ?_, ?_⟩
  · suffices e ≼[lex] single () #S by
      simpa [MonomialOrder.lex_le_iff_of_unique] using this
    rw [← Alon.degree_P]
    apply MonomialOrder.le_degree
    rw [mem_support_iff]
    convert! he
  · rw [← hm]
    ext j
    by_cases hj : j = i
    · rw [hj, mapDomain_apply (Function.injective_of_subsingleton _), single_eq_same]
    · rw [mapDomain_notin_range, single_eq_of_ne hj]
      simp [Set.range_const, Set.mem_singleton_iff, hj]
Cleared hypotheses: hm
-- 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),
    (∀ (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
have 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
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
-- 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 :
  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
have 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
Tactic: use h
-- 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
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
⊢ (∀ (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
have hf₁ : f =
  (linearCombination (MvPolynomial σ R) fun (i : σ) ↦ Alon.P (S i) i : (a : σ →₀ MvPolynomial σ R) → MvPolynomial σ R) h
Tactic: rw [this, add_zero] at hf
Cleared hypotheses: hf, hh, hr, this
-- 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 :
  f =
    HAdd.hAdd (α := MvPolynomial σ R)
      ((linearCombination (MvPolynomial σ R) fun (i : σ) ↦ Alon.P (S i) i :
            (a : σ →₀ MvPolynomial σ R) → MvPolynomial σ R)
          h :
        MvPolynomial σ R)
      r
hh :
  ∀ (i : σ),
    LE.le (α := syn (σ := σ) degLex)
      ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn)
          (MonomialOrder.degree degLex
            (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (Alon.P (S i) i)
              ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R))) :
        syn (σ := σ) degLex)
      ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn) (MonomialOrder.degree degLex f) : syn (σ := σ) degLex)
hr : ∀ c ∈ r.support, ∀ (i : σ), ¬MonomialOrder.degree degLex (Alon.P (S i) i) ≤ c
⊢ (∀ (i : σ),
      (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
have h₁ : r = 0
Tactic: suffices r = 0 by
    rw [this, add_zero] at hf
    exact ⟨fun i ↦ degLex_totalDegree_monotone (hh i), 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
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
⊢ r = 0
have h₁ : ∀ (i : σ), degreeOf i r < #(S i)
Tactic: apply eq_zero_of_eval_zero_at_prod_finset r S
-- 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 :
  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)
⊢ r = 0
have h₂ : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) r : R) (0 : R)
Tactic: apply eq_zero_of_eval_zero_at_prod_finset r S
-- 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 :
  f =
    HAdd.hAdd (α := MvPolynomial σ R)
      ((linearCombination (MvPolynomial σ R) fun (i : σ) ↦ Alon.P (S i) i :
            (a : σ →₀ MvPolynomial σ R) → MvPolynomial σ R)
          h :
        MvPolynomial σ R)
      r
hh :
  ∀ (i : σ),
    LE.le (α := syn (σ := σ) degLex)
      ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn)
          (MonomialOrder.degree degLex
            (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (Alon.P (S i) i)
              ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R))) :
        syn (σ := σ) degLex)
      ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn) (MonomialOrder.degree degLex f) : syn (σ := σ) degLex)
hr : ∀ c ∈ r.support, ∀ (i : σ), ¬MonomialOrder.degree degLex (Alon.P (S i) i) ≤ c
i : σ
⊢ degreeOf i r < #(S i)
have h₁ : ∀ b ∈ r.support, (b : (a : σ) → ℕ) i < #(S i)
Tactic: rw [degreeOf_eq_sup, Finset.sup_lt_iff (by simp [Sne 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
S : σ → Finset R
Sne : ∀ (i : σ), (S i).Nonempty
f : MvPolynomial σ R
Heval :
  ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) f : R) (0 : R)
this : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
h : σ →₀ MvPolynomial σ R
r : MvPolynomial σ R
hf :
  f =
    HAdd.hAdd (α := MvPolynomial σ R)
      ((linearCombination (MvPolynomial σ R) fun (i : σ) ↦ Alon.P (S i) i :
            (a : σ →₀ MvPolynomial σ R) → MvPolynomial σ R)
          h :
        MvPolynomial σ R)
      r
hh :
  ∀ (i : σ),
    LE.le (α := syn (σ := σ) degLex)
      ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn)
          (MonomialOrder.degree degLex
            (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (Alon.P (S i) i)
              ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R))) :
        syn (σ := σ) degLex)
      ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn) (MonomialOrder.degree degLex f) : syn (σ := σ) degLex)
hr : ∀ c ∈ r.support, ∀ (i : σ), ¬MonomialOrder.degree degLex (Alon.P (S i) i) ≤ c
x : σ → R
hx : ∀ (i : σ), x i ∈ S i
⊢ Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) r : R) (0 : R)
have h₁ : ∀
  (hf :
    HSub.hSub (β := MvPolynomial σ R) f
        ((linearCombination (MvPolynomial σ R) fun (i : σ) ↦ Alon.P (S i) i :
              (a : σ →₀ MvPolynomial σ R) → MvPolynomial σ R)
            h :
          MvPolynomial σ R) =
      r)
  (hh :
    ∀ (i : σ),
      LE.le (α := syn (σ := σ) degLex)
        ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn)
            (MonomialOrder.degree degLex
              (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (Alon.P (S i) i)
                ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R))) :
          syn (σ := σ) degLex)
        ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn) (MonomialOrder.degree degLex f) : syn (σ := σ) degLex))
  (hr : ∀ c ∈ r.support, ∀ (i : σ), ¬MonomialOrder.degree degLex (Alon.P (S i) i) ≤ c) (x : σ → R)
  (hx : ∀ (i : σ), x i ∈ S i), Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) r : R) (0 : R)
Tactic: rw [Iff.symm sub_eq_iff_eq_add'] at hf
Cleared hypotheses: hf, hh, hr, x, hx
-- 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
⊢ Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) r : R) (0 : R)
have h₁ : ∀ x_1 ∈ h.support,
  Eq.{u_1 + 1} (α := R)
    ((eval x : (a : MvPolynomial σ R) → R)
        (HSMul.hSMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
          ((h : (a : σ) → MvPolynomial σ R) x_1 : MvPolynomial σ R) (Alon.P (S x_1) x_1)) :
      R)
    (0 : R)
Tactic: rw [← hf, map_sub, Heval x hx, zero_sub, neg_eq_zero,
      linearCombination_apply, map_finsuppSum, Finsupp.sum, Finset.sum_eq_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)
        (HSMul.hSMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
          ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R) (Alon.P (S i) i)) :
      R)
    (0 : R)
have h₁ : HMul.hMul (α := R) (β := R)
    ((eval x : (a : MvPolynomial σ R) → R) ((h : (a : σ) → MvPolynomial σ R) i : MvPolynomial σ R) : R)
    ((eval x : (a : MvPolynomial σ R) → R) (Alon.P (S i) i) : R) =
  0
Tactic: rw [smul_eq_mul, map_mul]