awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Nullstellensatz
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
⊢ 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

Premises used: MvPolynomial.mem_support_iff, ne_eq, MvPolynomial.optionEquivLeft_coeff_some_coeff_none, And.right, And.left
-- Module: Mathlib.Combinatorics.Nullstellensatz
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
he₁ :
  let n := (embDomain Embedding.some e).update none m;
  n ∈ P.support
⊢ let n := (embDomain Embedding.some e).update none m;
  (n : (a : Option σ) → ℕ) none = m ∧ n.some = e

Tactic:
rw [hQ, ← hn.1, ← hn.2, optionEquivLeft_coeff_some_coeff_none, ← ne_eq,
        ← MvPolynomial.mem_support_iff] at he

Premises used: MvPolynomial.mem_support_iff, ne_eq, MvPolynomial.optionEquivLeft_coeff_some_coeff_none, And.right, And.left
-- Module: Mathlib.Combinatorics.Nullstellensatz
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 (α := ℕ) ((n : (a : Option σ) → ℕ) (Option.some i) : ℕ)
    (P.support.sup fun (m : Option σ →₀ ℕ) ↦ (m : (a : Option σ) → ℕ) (Option.some i) : ℕ)

Tactic:
Finset.le_sup he

Premises used: Finset.le_sup
-- Module: Mathlib.Combinatorics.Nullstellensatz
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 (α := ℕ) ((e : (a : σ) → ℕ) i : ℕ) ((n : (a : Option σ) → ℕ) (Option.some i) : ℕ)
⊢ LE.le (α := ℕ) ((e : (a : σ) → ℕ) i : ℕ)
    (P.support.sup fun (m : Option σ →₀ ℕ) ↦ (m : (a : Option σ) → ℕ) (Option.some i) : ℕ)

Tactic:
convert! Finset.le_sup he

Premises used: Finset.le_sup
-- Module: Mathlib.Combinatorics.Nullstellensatz
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) : ℕ)
h₂ h₃ : Eq (α := ℕ) ((n : (a : Option σ) → ℕ) (Option.some i) : ℕ) ((n : (a : Option σ) → ℕ) (Option.some i) : ℕ)
⊢ Eq (α := ℕ) ((e : (a : σ) → ℕ) i : ℕ) ((n : (a : Option σ) → ℕ) (Option.some i) : ℕ)

Tactic:
rw [← hn.2, some_apply]

Premises used: And.right, Finsupp.some_apply
-- Module: Mathlib.Combinatorics.Nullstellensatz
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)
⊢ Polynomial.map (eval x) Q = 0

Tactic:
specialize Heval' x hx
-- Module: Mathlib.Combinatorics.Nullstellensatz
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
⊢ ∀ (n : ℕ), (Polynomial.map (eval x) Q).coeff n = Polynomial.coeff 0 n

Tactic:
rw [Polynomial.ext_iff] at Heval'

Premises used: Polynomial.ext_iff
-- Module: Mathlib.Combinatorics.Nullstellensatz
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' : ∀ (n : ℕ), (Polynomial.map (eval x) Q).coeff n = Polynomial.coeff 0 n
⊢ Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) (Q.coeff m) : R) (0 : R)

Tactic:
simpa only [Polynomial.coeff_map, Polynomial.coeff_zero] using Heval' m

Premises used: Polynomial.coeff_map, Polynomial.coeff_zero
-- Module: Mathlib.Combinatorics.Nullstellensatz
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)
rw₁ :
  ∀ i_1 ∈ S,
    IsRegular
      (m.leadingCoeff
        (HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((C : (a : R) → MvPolynomial σ R) i_1 : MvPolynomial σ R)))
⊢ 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

Tactic:
rw [degree_prod_of_regular]

Premises used: MonomialOrder.degree_prod_of_regular
-- Module: Mathlib.Combinatorics.Nullstellensatz
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 : σ
⊢ 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:
simp [Finset.sum_congr rfl (fun r _ ↦ m.degree_X_sub_C i r)]

Premises used: MonomialOrder.degree_X_sub_C, Finset.sum_congr, rfl
-- Module: Mathlib.Combinatorics.Nullstellensatz
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
_ :
  r ∈ S →
    IsRegular
      (m.leadingCoeff
        (HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)))
⊢ r ∈ S →
    IsRegular
      (m.leadingCoeff
        (HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)))

Tactic:
_
-- Module: Mathlib.Combinatorics.Nullstellensatz
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
rw : IsRegular.{u_1} (R := R) 1
⊢ IsRegular
    (m.leadingCoeff
      (HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
        ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)))

Tactic:
rw [m.monic_X_sub_C]

Premises used: MonomialOrder.monic_X_sub_C
-- Module: Mathlib.Combinatorics.Nullstellensatz
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.{u_1} (R := R) 1

Tactic:
isRegular_one

Premises used: isRegular_one
-- Module: Mathlib.Combinatorics.Nullstellensatz
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.{u_1} (R := R) 1

Tactic:
exact isRegular_one

Premises used: isRegular_one
-- Module: Mathlib.Combinatorics.Nullstellensatz
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 : σ
⊢ m.Monic (P S i)

Tactic:
Monic.prod (fun r _ ↦ m.monic_X_sub_C i r)

Premises used: MonomialOrder.monic_X_sub_C, _private.0.MvPolynomial.Alon.P, MonomialOrder.Monic.prod
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hm : m ∈ support (P S i)
⊢ Eq (α := MvPolynomial ι R) (P S i)
    ((rename fun (x : Unit) ↦ i : (a : MvPolynomial Unit R) → MvPolynomial ι R) (P S ()))

Tactic:
simp [Alon.P]

Premises used: _private.0.MvPolynomial.Alon.P
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hm : m ∈ support (P S i)
⊢ 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]
-- Module: Mathlib.Combinatorics.Nullstellensatz
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 ()))
⊢ 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

Premises used: MvPolynomial.support_rename_of_injective, Function.injective_of_subsingleton
-- Module: Mathlib.Combinatorics.Nullstellensatz
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 ()))
hm₁ : Membership.mem (γ := Finset (ι →₀ ℕ)) (Finset.image (mapDomain fun (x : Unit) ↦ i) (support (P S ()))) m
⊢ Eq (α := MvPolynomial ι R) (P S i)
    ((rename fun (x : Unit) ↦ i : (a : MvPolynomial Unit R) → MvPolynomial ι R) (P S ()))

Tactic:
rw [hP, support_rename_of_injective (Function.injective_of_subsingleton _)] at hm

Premises used: MvPolynomial.support_rename_of_injective, Function.injective_of_subsingleton
-- Module: Mathlib.Combinatorics.Nullstellensatz
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 ()))
⊢ ∃ (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

Premises used: MvPolynomial.mem_support_iff, Finset.mem_image, ne_eq
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hP :
  Eq (α := MvPolynomial ι R) (P S i)
    ((rename fun (x : Unit) ↦ i : (a : MvPolynomial Unit R) → MvPolynomial ι R) (P S ()))
hm : ∃ (a : Unit →₀ ℕ), ¬coeff a (P S ()) = 0 ∧ mapDomain (fun (x : Unit) ↦ i) a = m
obtain :
  ∀ (e : Unit →₀ ℕ) (he : ¬coeff e (P S ()) = 0) (hm : mapDomain (fun (x : Unit) ↦ i) e = m), ∃ e ≤ #S, m = single i e
⊢ ∃ e ≤ #S, m = single i e

Tactic:
obtain ⟨e, he, hm⟩ := hm
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hP :
  Eq (α := MvPolynomial ι R) (P S i)
    ((rename fun (x : Unit) ↦ i : (a : MvPolynomial Unit R) → MvPolynomial ι R) (P S ()))
e : Unit →₀ ℕ
he : ¬coeff e (P S ()) = 0
hm : mapDomain (fun (x : Unit) ↦ i) e = m
⊢ Nontrivial R

Tactic:
haveI : Nontrivial R := nontrivial_of_ne _ _ he
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hP :
  Eq (α := MvPolynomial ι R) (P S i)
    ((rename fun (x : Unit) ↦ i : (a : MvPolynomial Unit R) → MvPolynomial ι R) (P S ()))
e : Unit →₀ ℕ
he : ¬coeff e (P S ()) = 0
hm : mapDomain (fun (x : Unit) ↦ i) e = m
this : Nontrivial R
⊢ ∃ e ≤ #S, m = single i e

Tactic:
⟨e (), ?_, ?_⟩

Premises used: Unit.unit, And.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hP :
  Eq (α := MvPolynomial ι R) (P S i)
    ((rename fun (x : Unit) ↦ i : (a : MvPolynomial Unit R) → MvPolynomial ι R) (P S ()))
e : Unit →₀ ℕ
he : ¬coeff e (P S ()) = 0
hm : mapDomain (fun (x : Unit) ↦ i) e = m
this : Nontrivial R
refine_1 : (e : (a : Unit) → ℕ) () ≤ #S
refine_2 : m = single i ((e : (a : Unit) → ℕ) ())
⊢ ∃ e ≤ #S, m = single i e

Tactic:
refine ⟨e (), ?_, ?_⟩
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hP :
  Eq (α := MvPolynomial ι R) (P S i)
    ((rename fun (x : Unit) ↦ i : (a : MvPolynomial Unit R) → MvPolynomial ι R) (P S ()))
e : Unit →₀ ℕ
he : ¬coeff e (P S ()) = 0
hm : mapDomain (fun (x : Unit) ↦ i) e = m
this_1 : Nontrivial R
this :
  LE.le (α := syn (σ := Unit) lex) ((toSyn lex : (a : Unit →₀ ℕ) → lex.syn) e : syn (σ := Unit) lex)
    ((toSyn lex : (a : Unit →₀ ℕ) → lex.syn) (single () #S) : syn (σ := Unit) lex)
⊢ (e : (a : Unit) → ℕ) () ≤ #S

Tactic:
simpa [MonomialOrder.lex_le_iff_of_unique] using this

Premises used: MonomialOrder.lex_le_iff_of_unique
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hP :
  Eq (α := MvPolynomial ι R) (P S i)
    ((rename fun (x : Unit) ↦ i : (a : MvPolynomial Unit R) → MvPolynomial ι R) (P S ()))
e : Unit →₀ ℕ
he : ¬coeff e (P S ()) = 0
hm : mapDomain (fun (x : Unit) ↦ i) e = m
this : Nontrivial R
refine_1 :
  LE.le (α := syn (σ := Unit) lex) ((toSyn lex : (a : Unit →₀ ℕ) → lex.syn) e : syn (σ := Unit) lex)
    ((toSyn lex : (a : Unit →₀ ℕ) → lex.syn) (single () #S) : syn (σ := Unit) lex)
⊢ (e : (a : Unit) → ℕ) () ≤ #S

Tactic:
suffices e ≼[lex] single () #S by
      simpa [MonomialOrder.lex_le_iff_of_unique] using this
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hP :
  Eq (α := MvPolynomial ι R) (P S i)
    ((rename fun (x : Unit) ↦ i : (a : MvPolynomial Unit R) → MvPolynomial ι R) (P S ()))
e : Unit →₀ ℕ
he : ¬coeff e (P S ()) = 0
hm : mapDomain (fun (x : Unit) ↦ i) e = m
this : Nontrivial R
refine_1 :
  LE.le (α := syn (σ := Unit) lex) ((toSyn lex : (a : Unit →₀ ℕ) → lex.syn) e : syn (σ := Unit) lex)
    ((toSyn lex : (a : Unit →₀ ℕ) → lex.syn) (MonomialOrder.degree lex (P S ())) : syn (σ := Unit) lex)
refine_1₁ : MonomialOrder Unit
⊢ LE.le (α := syn (σ := Unit) lex) ((toSyn lex : (a : Unit →₀ ℕ) → lex.syn) e : syn (σ := Unit) lex)
    ((toSyn lex : (a : Unit →₀ ℕ) → lex.syn) (single () #S) : syn (σ := Unit) lex)

Tactic:
rw [← Alon.degree_P]

Premises used: _private.0.MvPolynomial.Alon.degree_P
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hP :
  Eq (α := MvPolynomial ι R) (P S i)
    ((rename fun (x : Unit) ↦ i : (a : MvPolynomial Unit R) → MvPolynomial ι R) (P S ()))
e : Unit →₀ ℕ
he : ¬coeff e (P S ()) = 0
hm : mapDomain (fun (x : Unit) ↦ i) e = m
this : Nontrivial R
refine_1 : coeff e (P S ()) ≠ 0
⊢ e ∈ support (P S ())

Tactic:
rw [mem_support_iff]

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

Tactic:
he
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hP :
  Eq (α := MvPolynomial ι R) (P S i)
    ((rename fun (x : Unit) ↦ i : (a : MvPolynomial Unit R) → MvPolynomial ι R) (P S ()))
e : Unit →₀ ℕ
he : ¬coeff e (P S ()) = 0
hm : mapDomain (fun (x : Unit) ↦ i) e = m
this : Nontrivial R
⊢ coeff e (P S ()) ≠ 0

Tactic:
convert! he
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hP :
  Eq (α := MvPolynomial ι R) (P S i)
    ((rename fun (x : Unit) ↦ i : (a : MvPolynomial Unit R) → MvPolynomial ι R) (P S ()))
e : Unit →₀ ℕ
he : ¬coeff e (P S ()) = 0
hm : mapDomain (fun (x : Unit) ↦ i) e = m
this : Nontrivial R
refine_2 : Eq.{u_3 + 1} (α := ι →₀ ℕ) (mapDomain (fun (x : Unit) ↦ i) e) (single i ((e : (a : Unit) → ℕ) ()))
⊢ m = single i ((e : (a : Unit) → ℕ) ())

Tactic:
rw [← hm]
-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hP :
  Eq (α := MvPolynomial ι R) (P S i)
    ((rename fun (x : Unit) ↦ i : (a : MvPolynomial Unit R) → MvPolynomial ι R) (P S ()))
e : Unit →₀ ℕ
he : ¬coeff e (P S ()) = 0
hm : mapDomain (fun (x : Unit) ↦ i) e = m
this : Nontrivial R
refine_2 :
  ∀ (j : ι),
    Eq (α := ℕ) ((mapDomain (fun (x : Unit) ↦ i) e : (a : ι) → ℕ) j : ℕ)
      (((single i ((e : (a : Unit) → ℕ) ()) : ι →₀ ℕ) : (a : ι) → ℕ) j : ℕ)
⊢ Eq.{u_3 + 1} (α := ι →₀ ℕ) (mapDomain (fun (x : Unit) ↦ i) e) (single i ((e : (a : Unit) → ℕ) ()))

Tactic:
ext j