awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
Goal:
R : Type u_1
inst : CommRing R
σ_1 : Type u_2
inst_1 : Finite σ_1
inst_2 : IsDomain R
σ : Type u_2
inst_3 : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R) (Hdeg : ∀ (i : σ), degreeOf i P < #(S i))
    (Heval :
      ∀ (x : σ → R),
        (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) P : R) (0 : R)),
    P = 0
P : MvPolynomial.{u_2, u_1} (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval :
  ∀ (x : Option σ → R),
    (∀ (i : Option σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial (Option σ) R) → R) P : R) (0 : R)
Q : Polynomial (MvPolynomial σ R) :=
  (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
hQ : Q = (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
Heval' : ∀ (x : σ → R) (hx : ∀ (i : σ), x i ∈ S (Option.some i)), Polynomial.map (eval x) Q = 0
m : ℕ
d : σ →₀ ℕ
⊢ coeff d (Q.coeff m) = coeff d (Polynomial.coeff 0 m)
have h_option : coeff d (Q.coeff m) = 0
Tactic: simp only [Polynomial.coeff_zero, coeff_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
Goal:
R : Type u_1
inst : CommRing R
σ_1 : Type u_2
inst_1 : Finite σ_1
inst_2 : IsDomain R
σ : Type u_2
inst_3 : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R) (Hdeg : ∀ (i : σ), degreeOf i P < #(S i))
    (Heval :
      ∀ (x : σ → R),
        (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) P : R) (0 : R)),
    P = 0
P : MvPolynomial.{u_2, u_1} (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval :
  ∀ (x : Option σ → R),
    (∀ (i : Option σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial (Option σ) R) → R) P : R) (0 : R)
Q : Polynomial (MvPolynomial σ R) :=
  (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
hQ : Q = (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
Heval' : ∀ (x : σ → R) (hx : ∀ (i : σ), x i ∈ S (Option.some i)), Polynomial.map (eval x) Q = 0
m : ℕ
d : σ →₀ ℕ
⊢ coeff d (Q.coeff m) = 0
have h_option : Q.coeff m = 0
Tactic: suffices Q.coeff m = 0 by simp only [this, coeff_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
Goal:
R : Type u_1
inst : CommRing R
σ_1 : Type u_2
inst_1 : Finite σ_1
inst_2 : IsDomain R
σ : Type u_2
inst_3 : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R) (Hdeg : ∀ (i : σ), degreeOf i P < #(S i))
    (Heval :
      ∀ (x : σ → R),
        (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) P : R) (0 : R)),
    P = 0
P : MvPolynomial.{u_2, u_1} (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval :
  ∀ (x : Option σ → R),
    (∀ (i : Option σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial (Option σ) R) → R) P : R) (0 : R)
Q : Polynomial (MvPolynomial σ R) :=
  (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
hQ : Q = (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
Heval' : ∀ (x : σ → R) (hx : ∀ (i : σ), x i ∈ S (Option.some i)), Polynomial.map (eval x) Q = 0
m : ℕ
d : σ →₀ ℕ
⊢ Q.coeff m = 0
have h_option : ∀ (i : σ), degreeOf i (Q.coeff m) < #(S (Option.some i))
Tactic: apply h _ (fun i ↦ S (some i))
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
Goal:
R : Type u_1
inst : CommRing R
σ_1 : Type u_2
inst_1 : Finite σ_1
inst_2 : IsDomain R
σ : Type u_2
inst_3 : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R) (Hdeg : ∀ (i : σ), degreeOf i P < #(S i))
    (Heval :
      ∀ (x : σ → R),
        (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) P : R) (0 : R)),
    P = 0
P : MvPolynomial.{u_2, u_1} (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval :
  ∀ (x : Option σ → R),
    (∀ (i : Option σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial (Option σ) R) → R) P : R) (0 : R)
Q : Polynomial (MvPolynomial σ R) :=
  (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
hQ : Q = (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
Heval' : ∀ (x : σ → R) (hx : ∀ (i : σ), x i ∈ S (Option.some i)), Polynomial.map (eval x) Q = 0
m : ℕ
d : σ →₀ ℕ
h_option : ∀ (i : σ), degreeOf i (Q.coeff m) < #(S (Option.some i))
⊢ Q.coeff m = 0
have h_option₁ : ∀ (x : σ → R),
  (∀ (i : σ), x i ∈ S (Option.some i)) →
    Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) (Q.coeff m) : R) (0 : R)
Tactic: apply h _ (fun i ↦ S (some i))
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
Goal:
R : Type u_1
inst : CommRing R
σ_1 : Type u_2
inst_1 : Finite σ_1
inst_2 : IsDomain R
σ : Type u_2
inst_3 : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R) (Hdeg : ∀ (i : σ), degreeOf i P < #(S i))
    (Heval :
      ∀ (x : σ → R),
        (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) P : R) (0 : R)),
    P = 0
P : MvPolynomial.{u_2, u_1} (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval :
  ∀ (x : Option σ → R),
    (∀ (i : Option σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial (Option σ) R) → R) P : R) (0 : R)
Q : Polynomial (MvPolynomial σ R) :=
  (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
hQ : Q = (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
Heval' : ∀ (x : σ → R) (hx : ∀ (i : σ), x i ∈ S (Option.some i)), Polynomial.map (eval x) Q = 0
m : ℕ
d : σ →₀ ℕ
i : σ
⊢ degreeOf i (Q.coeff m) < #(S (Option.some i))
have apply : degreeOf i (Q.coeff m) ≤ degreeOf (Option.some i) P
Tactic: apply lt_of_le_of_lt _ (Hdeg (some i))
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
Goal:
R : Type u_1
inst : CommRing R
σ_1 : Type u_2
inst_1 : Finite σ_1
inst_2 : IsDomain R
σ : Type u_2
inst_3 : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R) (Hdeg : ∀ (i : σ), degreeOf i P < #(S i))
    (Heval :
      ∀ (x : σ → R),
        (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) P : R) (0 : R)),
    P = 0
P : MvPolynomial.{u_2, u_1} (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval :
  ∀ (x : Option σ → R),
    (∀ (i : Option σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial (Option σ) R) → R) P : R) (0 : R)
Q : Polynomial (MvPolynomial σ R) :=
  (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
hQ : Q = (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
Heval' : ∀ (x : σ → R) (hx : ∀ (i : σ), x i ∈ S (Option.some i)), Polynomial.map (eval x) Q = 0
m : ℕ
d : σ →₀ ℕ
i : σ
⊢ degreeOf i (Q.coeff m) ≤ degreeOf (Option.some i) P
have simp : ∀ (b : σ →₀ ℕ),
  ¬coeff b (Q.coeff m) = 0 →
    LE.le (α := ℕ) ((b : (a : σ) → ℕ) i : ℕ)
      (P.support.sup fun (m : Option σ →₀ ℕ) ↦ (m : (a : Option σ) → ℕ) (Option.some i) : ℕ)
Tactic: simp only [degreeOf_eq_sup, Finset.sup_le_iff, mem_support_iff, ne_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
σ_1 : Type u_2
inst_1 : Finite σ_1
inst_2 : IsDomain R
σ : Type u_2
inst_3 : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R) (Hdeg : ∀ (i : σ), degreeOf i P < #(S i))
    (Heval :
      ∀ (x : σ → R),
        (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) P : R) (0 : R)),
    P = 0
P : MvPolynomial.{u_2, u_1} (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval :
  ∀ (x : Option σ → R),
    (∀ (i : Option σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial (Option σ) R) → R) P : R) (0 : R)
Q : Polynomial (MvPolynomial σ R) :=
  (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
hQ : Q = (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
Heval' : ∀ (x : σ → R) (hx : ∀ (i : σ), x i ∈ S (Option.some i)), Polynomial.map (eval x) Q = 0
m : ℕ
d : σ →₀ ℕ
i : σ
e : σ →₀ ℕ
he : ¬coeff e (Q.coeff m) = 0
⊢ LE.le (α := ℕ) ((e : (a : σ) → ℕ) i : ℕ)
    (P.support.sup fun (m : Option σ →₀ ℕ) ↦ (m : (a : Option σ) → ℕ) (Option.some i) : ℕ)
have hn : let n := (embDomain Embedding.some e).update none m;
n = (embDomain Embedding.some e).update none m
Tactic: set n := (embDomain Function.Embedding.some e).update none m with hn
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
σ_1 : Type u_2
inst_1 : Finite σ_1
inst_2 : IsDomain R
σ : Type u_2
inst_3 : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R) (Hdeg : ∀ (i : σ), degreeOf i P < #(S i))
    (Heval :
      ∀ (x : σ → R),
        (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) P : R) (0 : R)),
    P = 0
P : MvPolynomial.{u_2, u_1} (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval :
  ∀ (x : Option σ → R),
    (∀ (i : Option σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial (Option σ) R) → R) P : R) (0 : R)
Q : Polynomial (MvPolynomial σ R) :=
  (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
hQ : Q = (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
Heval' : ∀ (x : σ → R) (hx : ∀ (i : σ), x i ∈ S (Option.some i)), Polynomial.map (eval x) Q = 0
m : ℕ
d : σ →₀ ℕ
i : σ
e : σ →₀ ℕ
he : ¬coeff e (Q.coeff m) = 0
n : Option σ →₀ ℕ := (embDomain Embedding.some e).update none m
hn : n = (embDomain Embedding.some e).update none m
⊢ LE.le (α := ℕ) ((e : (a : σ) → ℕ) i : ℕ)
    (P.support.sup fun (m : Option σ →₀ ℕ) ↦ (m : (a : Option σ) → ℕ) (Option.some i) : ℕ)
have hn₁ : (n : (a : Option σ) → ℕ) none = m ∧ n.some = e
Tactic: rw [eq_option_embedding_update_none_iff] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
σ_1 : Type u_2
inst_1 : Finite σ_1
inst_2 : IsDomain R
σ : Type u_2
inst_3 : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R) (Hdeg : ∀ (i : σ), degreeOf i P < #(S i))
    (Heval :
      ∀ (x : σ → R),
        (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) P : R) (0 : R)),
    P = 0
P : MvPolynomial.{u_2, u_1} (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval :
  ∀ (x : Option σ → R),
    (∀ (i : Option σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial (Option σ) R) → R) P : R) (0 : R)
Q : Polynomial (MvPolynomial σ R) :=
  (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
hQ : Q = (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
Heval' : ∀ (x : σ → R) (hx : ∀ (i : σ), x i ∈ S (Option.some i)), Polynomial.map (eval x) Q = 0
m : ℕ
d : σ →₀ ℕ
i : σ
e : σ →₀ ℕ
he : ¬coeff e (Q.coeff m) = 0
n : Option σ →₀ ℕ := (embDomain Embedding.some e).update none m
hn : (n : (a : Option σ) → ℕ) none = m ∧ n.some = e
⊢ LE.le (α := ℕ) ((e : (a : σ) → ℕ) i : ℕ)
    (P.support.sup fun (m : Option σ →₀ ℕ) ↦ (m : (a : Option σ) → ℕ) (Option.some i) : ℕ)
have he₁ : let n := (embDomain Embedding.some e).update none m;
n ∈ P.support
Tactic: rw [hQ, ← hn.1, ← hn.2, optionEquivLeft_coeff_some_coeff_none, ← ne_eq,
        ← MvPolynomial.mem_support_iff] at he
Cleared hypotheses: he, n, hn
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
Goal:
R : Type u_1
inst : CommRing R
σ_1 : Type u_2
inst_1 : Finite σ_1
inst_2 : IsDomain R
σ : Type u_2
inst_3 : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R) (Hdeg : ∀ (i : σ), degreeOf i P < #(S i))
    (Heval :
      ∀ (x : σ → R),
        (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) P : R) (0 : R)),
    P = 0
P : MvPolynomial.{u_2, u_1} (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval :
  ∀ (x : Option σ → R),
    (∀ (i : Option σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial (Option σ) R) → R) P : R) (0 : R)
Q : Polynomial (MvPolynomial σ R) :=
  (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
hQ : Q = (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
Heval' : ∀ (x : σ → R) (hx : ∀ (i : σ), x i ∈ S (Option.some i)), Polynomial.map (eval x) Q = 0
m : ℕ
d : σ →₀ ℕ
i : σ
e : σ →₀ ℕ
n : Option σ →₀ ℕ := (embDomain Embedding.some e).update none m
he : n ∈ P.support
hn : (n : (a : Option σ) → ℕ) none = m ∧ n.some = e
⊢ LE.le (α := ℕ) ((e : (a : σ) → ℕ) i : ℕ)
    (P.support.sup fun (m : Option σ →₀ ℕ) ↦ (m : (a : Option σ) → ℕ) (Option.some i) : ℕ)
have h₁ : Eq (α := ℕ) ((e : (a : σ) → ℕ) i : ℕ) ((n : (a : Option σ) → ℕ) (Option.some i) : ℕ)
Tactic: convert! Finset.le_sup he
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
Goal:
R : Type u_1
inst : CommRing R
σ_1 : Type u_2
inst_1 : Finite σ_1
inst_2 : IsDomain R
σ : Type u_2
inst_3 : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R) (Hdeg : ∀ (i : σ), degreeOf i P < #(S i))
    (Heval :
      ∀ (x : σ → R),
        (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) P : R) (0 : R)),
    P = 0
P : MvPolynomial.{u_2, u_1} (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval :
  ∀ (x : Option σ → R),
    (∀ (i : Option σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial (Option σ) R) → R) P : R) (0 : R)
Q : Polynomial (MvPolynomial σ R) :=
  (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
hQ : Q = (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
Heval' : ∀ (x : σ → R) (hx : ∀ (i : σ), x i ∈ S (Option.some i)), Polynomial.map (eval x) Q = 0
m : ℕ
d : σ →₀ ℕ
i : σ
e : σ →₀ ℕ
n : Option σ →₀ ℕ := (embDomain Embedding.some e).update none m
he : n ∈ P.support
hn : (n : (a : Option σ) → ℕ) none = m ∧ n.some = e
⊢ Eq (α := ℕ) ((e : (a : σ) → ℕ) i : ℕ) ((n : (a : Option σ) → ℕ) (Option.some i) : ℕ)
have h₁ : Eq (α := ℕ) ((n.some : (a : σ) → ℕ) i : ℕ) ((n : (a : Option σ) → ℕ) (Option.some i) : ℕ)
Tactic: rw [← hn.2, some_apply]
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
Goal:
R : Type u_1
inst : CommRing R
σ_1 : Type u_2
inst_1 : Finite σ_1
inst_2 : IsDomain R
σ : Type u_2
inst_3 : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R) (Hdeg : ∀ (i : σ), degreeOf i P < #(S i))
    (Heval :
      ∀ (x : σ → R),
        (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) P : R) (0 : R)),
    P = 0
P : MvPolynomial.{u_2, u_1} (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval :
  ∀ (x : Option σ → R),
    (∀ (i : Option σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial (Option σ) R) → R) P : R) (0 : R)
Q : Polynomial (MvPolynomial σ R) :=
  (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
hQ : Q = (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
Heval' : ∀ (x : σ → R) (hx : ∀ (i : σ), x i ∈ S (Option.some i)), Polynomial.map (eval x) Q = 0
m : ℕ
d : σ →₀ ℕ
i : σ
e : σ →₀ ℕ
n : Option σ →₀ ℕ := (embDomain Embedding.some e).update none m
he : n ∈ P.support
hn : (n : (a : Option σ) → ℕ) none = m ∧ n.some = e
h₁ : Eq (α := ℕ) ((n.some : (a : σ) → ℕ) i : ℕ) ((n : (a : Option σ) → ℕ) (Option.some i) : ℕ)
⊢ Eq (α := ℕ) ((e : (a : σ) → ℕ) i : ℕ) ((n : (a : Option σ) → ℕ) (Option.some i) : ℕ)
have h₂ : Eq (α := ℕ) ((n : (a : Option σ) → ℕ) (Option.some i) : ℕ) ((n : (a : Option σ) → ℕ) (Option.some i) : ℕ)
Tactic: rw [← hn.2, some_apply]
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
σ_1 : Type u_2
inst_1 : Finite σ_1
inst_2 : IsDomain R
σ : Type u_2
inst_3 : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R) (Hdeg : ∀ (i : σ), degreeOf i P < #(S i))
    (Heval :
      ∀ (x : σ → R),
        (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) P : R) (0 : R)),
    P = 0
P : MvPolynomial.{u_2, u_1} (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval :
  ∀ (x : Option σ → R),
    (∀ (i : Option σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial (Option σ) R) → R) P : R) (0 : R)
Q : Polynomial (MvPolynomial σ R) :=
  (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
hQ : Q = (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
Heval' : ∀ (x : σ → R) (hx : ∀ (i : σ), x i ∈ S (Option.some i)), Polynomial.map (eval x) Q = 0
m : ℕ
d : σ →₀ ℕ
x : σ → R
hx : ∀ (i : σ), x i ∈ S (Option.some i)
⊢ Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) (Q.coeff m) : R) (0 : R)
have Heval'₁ : Polynomial.map (eval x) Q = 0
Tactic: specialize Heval' x hx
Cleared hypotheses: Heval'
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
σ_1 : Type u_2
inst_1 : Finite σ_1
inst_2 : IsDomain R
σ : Type u_2
inst_3 : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R) (Hdeg : ∀ (i : σ), degreeOf i P < #(S i))
    (Heval :
      ∀ (x : σ → R),
        (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) P : R) (0 : R)),
    P = 0
P : MvPolynomial.{u_2, u_1} (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval :
  ∀ (x : Option σ → R),
    (∀ (i : Option σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial (Option σ) R) → R) P : R) (0 : R)
Q : Polynomial (MvPolynomial σ R) :=
  (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
hQ : Q = (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
m : ℕ
d : σ →₀ ℕ
x : σ → R
hx : ∀ (i : σ), x i ∈ S (Option.some i)
Heval' : Polynomial.map (eval x) Q = 0
⊢ Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) (Q.coeff m) : R) (0 : R)
have Heval'₁ : ∀ (n : ℕ), (Polynomial.map (eval x) Q).coeff n = Polynomial.coeff 0 n
Tactic: rw [Polynomial.ext_iff] at Heval'
Cleared hypotheses: Heval'
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_2
inst_1 : Nontrivial R
m : MonomialOrder.{u_2, u_3} σ
S : Finset R
i : σ
⊢ MonomialOrder.degree.{u_2, u_1, u_3} m (R := R)
      (∏ r ∈ S,
        HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)) =
    single i #S
have rw : Eq (α := σ →₀ ℕ)
  (∑ i_1 ∈ S,
    m.degree
      (HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
        ((C : (a : R) → MvPolynomial σ R) i_1 : MvPolynomial σ R)))
  (single i #S)
Tactic: rw [degree_prod_of_regular]
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_2
inst_1 : Nontrivial R
m : MonomialOrder.{u_2, u_3} σ
S : Finset R
i : σ
rw :
  Eq (α := σ →₀ ℕ)
    (∑ i_1 ∈ S,
      m.degree
        (HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((C : (a : R) → MvPolynomial σ R) i_1 : MvPolynomial σ R)))
    (single i #S)
⊢ MonomialOrder.degree.{u_2, u_1, u_3} m (R := R)
      (∏ r ∈ S,
        HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)) =
    single i #S
have rw₁ : ∀ i_1 ∈ S,
  IsRegular
    (m.leadingCoeff
      (HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
        ((C : (a : R) → MvPolynomial σ R) i_1 : MvPolynomial σ R)))
Tactic: rw [degree_prod_of_regular]
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_2
inst_1 : Nontrivial R
m : MonomialOrder.{u_2, u_3} σ
S : Finset R
i : σ
r : R
h : r ∈ S
⊢ IsRegular
    (m.leadingCoeff
      (HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
        ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)))
have rw : IsRegular.{u_1} (R := R) 1
Tactic: rw [m.monic_X_sub_C]
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hm : m ∈ support (P S i)
⊢ ∃ 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 ()))
Tactic: have hP : Alon.P S i = .rename (fun _ ↦ i) (Alon.P S ()) := by simp [Alon.P]
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hm : m ∈ support (P S i)
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
Tactic: rw [hP, support_rename_of_injective (Function.injective_of_subsingleton _)] at hm
Cleared hypotheses: hm, hP
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
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 hm₁ : ∃ (a : Unit →₀ ℕ), ¬coeff a (P S ()) = 0 ∧ mapDomain (fun (x : Unit) ↦ i) a = m
Tactic: simp only [Finset.mem_image, mem_support_iff, ne_eq] at hm
Cleared hypotheses: hm
-- 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 : ι →₀ ℕ
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 obtain : ∀ (e : Unit →₀ ℕ) (he : ¬coeff e (P S ()) = 0) (hm : mapDomain (fun (x : Unit) ↦ i) e = m), ∃ e ≤ #S, m = single i e
Tactic: obtain ⟨e, he, hm⟩ := hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (hypothesis)
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
⊢ ∃ e ≤ #S, m = single i e
have this : Nontrivial R
Tactic: haveI : Nontrivial R := nontrivial_of_ne _ _ he
-- 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 : ι →₀ ℕ
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
have refine_1 : (e : (a : Unit) → ℕ) () ≤ #S
Tactic: refine ⟨e (), ?_, ?_⟩