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
e : σ ≃ τ
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 τ 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)
i : σ
⊢ degreeOf.{u_1, u_2} (R := R) i ((rename (⇑e.symm : (a : τ) → σ) : (a : MvPolynomial τ R) → MvPolynomial σ R) P) =
    degreeOf ((e : (a : σ) → τ) i) P
have conv_lhs : degreeOf.{u_1, u_2} (R := R) i ((rename (⇑e.symm : (a : τ) → σ) : (a : MvPolynomial τ R) → MvPolynomial σ R) P) =
  degreeOf ((e : (a : σ) → τ) i) P
Tactic: conv_lhs => rw [← e.symm_apply_apply i, degreeOf_rename_of_injective e.symm.injective]
-- 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
e : σ ≃ τ
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 τ 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)
i : σ
conv_lhs :
  degreeOf.{u_1, u_2} (R := R) i ((rename (⇑e.symm : (a : τ) → σ) : (a : MvPolynomial τ R) → MvPolynomial σ R) P) =
    degreeOf ((e : (a : σ) → τ) i) P
⊢ degreeOf.{u_1, u_2} (R := R) i ((rename (⇑e.symm : (a : τ) → σ) : (a : MvPolynomial τ R) → MvPolynomial σ R) P) =
    degreeOf ((e : (a : σ) → τ) i) P
have h₁ : degreeOf ((e : (a : σ) → τ) i) P = degreeOf ((e : (a : σ) → τ) i) P
Tactic: conv_lhs => rw [← e.symm_apply_apply i, degreeOf_rename_of_injective e.symm.injective]
-- 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
e : σ ≃ τ
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 τ 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)
i : σ
⊢ degreeOf.{u_1, u_2} (R := R) i ((rename (⇑e.symm : (a : τ) → σ) : (a : MvPolynomial τ R) → MvPolynomial σ R) P) <
    #(S ((e : (a : σ) → τ) i))
have h₁ : degreeOf.{u_1, u_2} (R := R) i ((rename (⇑e.symm : (a : τ) → σ) : (a : MvPolynomial τ R) → MvPolynomial σ R) P) =
  degreeOf ((e : (a : σ) → τ) i) P
Tactic: classical
      convert! Hdeg (e i)
      conv_lhs => rw [← e.symm_apply_apply i, degreeOf_rename_of_injective e.symm.injective]
-- 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
e : σ ≃ τ
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 τ 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)
x : σ → R
hx : ∀ (i : σ), x i ∈ S ((e : (a : σ) → τ) i)
⊢ Eq.{u_1 + 1} (α := R)
    ((eval x : (a : MvPolynomial σ R) → R)
        ((rename (⇑e.symm : (a : τ) → σ) : (a : MvPolynomial τ R) → MvPolynomial σ R) P : MvPolynomial σ R) :
      R)
    (0 : R)
have of_equiv : Eq.{u_1 + 1} (α := R) ((eval (x ∘ (⇑e.symm : (a : τ) → σ)) : (a : MvPolynomial τ R) → R) P : R) (0 : R)
Tactic: simp only [MvPolynomial.eval_rename]
-- 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
e : σ ≃ τ
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 τ 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)
x : σ → R
hx : ∀ (i : σ), x i ∈ S ((e : (a : σ) → τ) i)
⊢ Eq.{u_1 + 1} (α := R) ((eval (x ∘ (⇑e.symm : (a : τ) → σ)) : (a : MvPolynomial τ R) → R) P : R) (0 : R)
have of_equiv : ∀ (i : τ), (x ∘ (⇑e.symm : (a : τ) → σ)) i ∈ S i
Tactic: apply Heval
-- 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
e : σ ≃ τ
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 τ 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)
x : σ → R
hx : ∀ (i : σ), x i ∈ S ((e : (a : σ) → τ) i)
s : τ
⊢ (x ∘ (⇑e.symm : (a : τ) → σ)) s ∈ S s
have of_equiv : x ((e.symm : (a : τ) → σ) s) ∈ S s
Tactic: simp only [Function.comp_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
e : σ ≃ τ
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 τ 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)
x : σ → R
hx : ∀ (i : σ), x i ∈ S ((e : (a : σ) → τ) i)
s : τ
⊢ x ((e.symm : (a : τ) → σ) s) ∈ S s
have h₁ : s = (e : (a : σ) → τ) ((e.symm : (a : τ) → σ) s : σ)
Tactic: convert! hx (e.symm s)
-- 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
P : MvPolynomial PEmpty.{u_2 + 1} R
S : PEmpty.{u_2 + 1} → Finset R
Hdeg : ∀ (i : PEmpty.{u_2 + 1}), degreeOf i P < #(S i)
Heval :
  ∀ (x : PEmpty.{u_2 + 1} → R),
    (∀ (i : PEmpty.{u_2 + 1}), x i ∈ S i) →
      Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial PEmpty.{u_2 + 1} R) → R) P : R) (0 : R)
this :
  P = (C : (a : R) → MvPolynomial PEmpty.{u_2 + 1} R) ((constantCoeff : (a : MvPolynomial PEmpty.{u_2 + 1} R) → R) P)
⊢ P = 0
have Heval₁ : Eq.{u_1 + 1} (α := R) ((eval default : (a : MvPolynomial PEmpty.{u_2 + 1} R) → R) P : R) (0 : R)
Tactic: specialize Heval default (fun i ↦ PEmpty.elim i)
Cleared hypotheses: Heval
-- 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
P : MvPolynomial PEmpty.{u_2 + 1} R
S : PEmpty.{u_2 + 1} → Finset R
Hdeg : ∀ (i : PEmpty.{u_2 + 1}), degreeOf i P < #(S i)
this :
  P = (C : (a : R) → MvPolynomial PEmpty.{u_2 + 1} R) ((constantCoeff : (a : MvPolynomial PEmpty.{u_2 + 1} R) → R) P)
Heval : Eq.{u_1 + 1} (α := R) ((eval default : (a : MvPolynomial PEmpty.{u_2 + 1} R) → R) P : R) (0 : R)
⊢ P = 0
have Heval₁ : Eq.{u_1 + 1} (α := R) ((constantCoeff : (a : MvPolynomial PEmpty.{u_2 + 1} R) → R) P : R) (0 : R)
Tactic: rw [this, eval_C] 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 : Finite σ
inst_2 : IsDomain R
P : MvPolynomial PEmpty.{u_2 + 1} R
S : PEmpty.{u_2 + 1} → Finset R
Hdeg : ∀ (i : PEmpty.{u_2 + 1}), degreeOf i P < #(S i)
this :
  P = (C : (a : R) → MvPolynomial PEmpty.{u_2 + 1} R) ((constantCoeff : (a : MvPolynomial PEmpty.{u_2 + 1} R) → R) P)
Heval : Eq.{u_1 + 1} (α := R) ((constantCoeff : (a : MvPolynomial PEmpty.{u_2 + 1} R) → R) P : R) (0 : R)
⊢ P = 0
have rw : Eq (α := MvPolynomial PEmpty.{u_2 + 1} R)
  ((C : (a : R) → MvPolynomial PEmpty.{u_2 + 1} R) ((constantCoeff : (a : MvPolynomial PEmpty.{u_2 + 1} R) → R) P) :
    MvPolynomial PEmpty.{u_2 + 1} R)
  (0 : MvPolynomial PEmpty.{u_2 + 1} R)
Tactic: rw [this, Heval, C_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
P : MvPolynomial PEmpty.{u_2 + 1} R
S : PEmpty.{u_2 + 1} → Finset R
Hdeg : ∀ (i : PEmpty.{u_2 + 1}), degreeOf i P < #(S i)
this :
  P = (C : (a : R) → MvPolynomial PEmpty.{u_2 + 1} R) ((constantCoeff : (a : MvPolynomial PEmpty.{u_2 + 1} R) → R) P)
Heval : Eq.{u_1 + 1} (α := R) ((constantCoeff : (a : MvPolynomial PEmpty.{u_2 + 1} R) → R) P : R) (0 : R)
rw :
  Eq (α := MvPolynomial PEmpty.{u_2 + 1} R)
    ((C : (a : R) → MvPolynomial PEmpty.{u_2 + 1} R) ((constantCoeff : (a : MvPolynomial PEmpty.{u_2 + 1} R) → R) P) :
      MvPolynomial PEmpty.{u_2 + 1} R)
    (0 : MvPolynomial PEmpty.{u_2 + 1} R)
⊢ P = 0
have rw₁ : Eq (α := MvPolynomial PEmpty.{u_2 + 1} R) ((C : (a : R) → MvPolynomial PEmpty.{u_2 + 1} R) 0) 0
Tactic: rw [this, Heval, C_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
P : MvPolynomial PEmpty.{u_2 + 1} R
S : PEmpty.{u_2 + 1} → Finset R
Hdeg : ∀ (i : PEmpty.{u_2 + 1}), degreeOf i P < #(S i)
this :
  P = (C : (a : R) → MvPolynomial PEmpty.{u_2 + 1} R) ((constantCoeff : (a : MvPolynomial PEmpty.{u_2 + 1} R) → R) P)
Heval : Eq.{u_1 + 1} (α := R) ((constantCoeff : (a : MvPolynomial PEmpty.{u_2 + 1} R) → R) P : R) (0 : R)
rw :
  Eq (α := MvPolynomial PEmpty.{u_2 + 1} R)
    ((C : (a : R) → MvPolynomial PEmpty.{u_2 + 1} R) ((constantCoeff : (a : MvPolynomial PEmpty.{u_2 + 1} R) → R) P) :
      MvPolynomial PEmpty.{u_2 + 1} R)
    (0 : MvPolynomial PEmpty.{u_2 + 1} R)
rw₁ : Eq (α := MvPolynomial PEmpty.{u_2 + 1} R) ((C : (a : R) → MvPolynomial PEmpty.{u_2 + 1} R) 0) 0
⊢ P = 0
have rw₂ : Eq (α := MvPolynomial PEmpty.{u_2 + 1} R) 0 0
Tactic: rw [this, Heval, C_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
P : MvPolynomial PEmpty.{u_2 + 1} R
S : PEmpty.{u_2 + 1} → Finset R
Hdeg : ∀ (i : PEmpty.{u_2 + 1}), degreeOf i P < #(S i)
Heval :
  ∀ (x : PEmpty.{u_2 + 1} → R),
    (∀ (i : PEmpty.{u_2 + 1}), x i ∈ S i) →
      Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial PEmpty.{u_2 + 1} R) → R) P : R) (0 : R)
⊢ P = 0
have h_empty : P = (C : (a : R) → MvPolynomial PEmpty.{u_2 + 1} R) ((constantCoeff : (a : MvPolynomial PEmpty.{u_2 + 1} R) → R) P)
Tactic: suffices P = C (constantCoeff P) by
      specialize Heval default (fun i ↦ PEmpty.elim i)
      rw [this, eval_C] at Heval
      rw [this, Heval, C_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
P : MvPolynomial PEmpty.{u_2 + 1} R
S : PEmpty.{u_2 + 1} → Finset R
Hdeg : ∀ (i : PEmpty.{u_2 + 1}), degreeOf i P < #(S i)
Heval :
  ∀ (x : PEmpty.{u_2 + 1} → R),
    (∀ (i : PEmpty.{u_2 + 1}), x i ∈ S i) →
      Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial PEmpty.{u_2 + 1} R) → R) P : R) (0 : R)
⊢ P = (C : (a : R) → MvPolynomial PEmpty.{u_2 + 1} R) ((constantCoeff : (a : MvPolynomial PEmpty.{u_2 + 1} R) → R) P)
have h_empty : ∀ (m : PEmpty.{u_2 + 1} →₀ ℕ),
  coeff m P =
    coeff m
      ((C : (a : R) → MvPolynomial PEmpty.{u_2 + 1} R) ((constantCoeff : (a : MvPolynomial PEmpty.{u_2 + 1} R) → R) P))
Tactic: ext m
-- 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
P : MvPolynomial PEmpty.{u_2 + 1} R
S : PEmpty.{u_2 + 1} → Finset R
Hdeg : ∀ (i : PEmpty.{u_2 + 1}), degreeOf i P < #(S i)
Heval :
  ∀ (x : PEmpty.{u_2 + 1} → R),
    (∀ (i : PEmpty.{u_2 + 1}), x i ∈ S i) →
      Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial PEmpty.{u_2 + 1} R) → R) P : R) (0 : R)
m : PEmpty.{u_2 + 1} →₀ ℕ
⊢ coeff m P =
    coeff m
      ((C : (a : R) → MvPolynomial PEmpty.{u_2 + 1} R) ((constantCoeff : (a : MvPolynomial PEmpty.{u_2 + 1} R) → R) P))
have h_empty : m = 0
Tactic: suffices m = 0 by simp [this, ← constantCoeff_eq]
-- 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
P : MvPolynomial PEmpty.{u_2 + 1} R
S : PEmpty.{u_2 + 1} → Finset R
Hdeg : ∀ (i : PEmpty.{u_2 + 1}), degreeOf i P < #(S i)
Heval :
  ∀ (x : PEmpty.{u_2 + 1} → R),
    (∀ (i : PEmpty.{u_2 + 1}), x i ∈ S i) →
      Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial PEmpty.{u_2 + 1} R) → R) P : R) (0 : R)
m : PEmpty.{u_2 + 1} →₀ ℕ
⊢ m = 0
have h_empty : ∀ (d : PEmpty.{u_2 + 1}), Eq (α := ℕ) ((m : (a : PEmpty.{u_2 + 1}) → ℕ) d : ℕ) ((0 : (a : PEmpty.{u_2 + 1}) → ℕ) d : ℕ)
Tactic: ext d
-- 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)
⊢ P = 0
have hQ : let Q : Polynomial (MvPolynomial σ R) :=
  (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P;
Q = (optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P
Tactic: set Q := optionEquivLeft R σ P with hQ
-- 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
this : Q = 0
⊢ P = 0
have rw : Eq (α := MvPolynomial.{u_2, u_1} (Option σ) R)
  ((AlgEquiv.symm (optionEquivLeft R σ) : (a : Polynomial (MvPolynomial σ R)) → MvPolynomial (Option σ) R)
      ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P) :
    MvPolynomial.{u_2, u_1} (Option σ) R)
  (0 : MvPolynomial.{u_2, u_1} (Option σ) R)
Tactic: rw [← AlgEquiv.symm_apply_apply (optionEquivLeft R σ) P, ← hQ, this, map_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
this : Q = 0
rw :
  Eq (α := MvPolynomial.{u_2, u_1} (Option σ) R)
    ((AlgEquiv.symm (optionEquivLeft R σ) : (a : Polynomial (MvPolynomial σ R)) → MvPolynomial (Option σ) R)
        ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P) :
      MvPolynomial.{u_2, u_1} (Option σ) R)
    (0 : MvPolynomial.{u_2, u_1} (Option σ) R)
rw₁ :
  Eq (α := MvPolynomial.{u_2, u_1} (Option σ) R)
    ((AlgEquiv.symm (optionEquivLeft R σ) : (a : Polynomial (MvPolynomial σ R)) → MvPolynomial (Option σ) R) Q :
      MvPolynomial.{u_2, u_1} (Option σ) R)
    (0 : MvPolynomial.{u_2, u_1} (Option σ) R)
⊢ P = 0
have rw₂ : Eq (α := MvPolynomial.{u_2, u_1} (Option σ) R)
  ((AlgEquiv.symm (optionEquivLeft R σ) : (a : Polynomial (MvPolynomial σ R)) → MvPolynomial (Option σ) R) 0) 0
Tactic: rw [← AlgEquiv.symm_apply_apply (optionEquivLeft R σ) P, ← hQ, this, map_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
this : Q = 0
rw :
  Eq (α := MvPolynomial.{u_2, u_1} (Option σ) R)
    ((AlgEquiv.symm (optionEquivLeft R σ) : (a : Polynomial (MvPolynomial σ R)) → MvPolynomial (Option σ) R)
        ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → Polynomial (MvPolynomial σ R)) P) :
      MvPolynomial.{u_2, u_1} (Option σ) R)
    (0 : MvPolynomial.{u_2, u_1} (Option σ) R)
rw₁ :
  Eq (α := MvPolynomial.{u_2, u_1} (Option σ) R)
    ((AlgEquiv.symm (optionEquivLeft R σ) : (a : Polynomial (MvPolynomial σ R)) → MvPolynomial (Option σ) R) Q :
      MvPolynomial.{u_2, u_1} (Option σ) R)
    (0 : MvPolynomial.{u_2, u_1} (Option σ) R)
rw₂ :
  Eq (α := MvPolynomial.{u_2, u_1} (Option σ) R)
    ((AlgEquiv.symm (optionEquivLeft R σ) : (a : Polynomial (MvPolynomial σ R)) → MvPolynomial (Option σ) R) 0) 0
⊢ P = 0
have rw₃ : Eq (α := MvPolynomial.{u_2, u_1} (Option σ) R) 0 0
Tactic: rw [← AlgEquiv.symm_apply_apply (optionEquivLeft R σ) P, ← hQ, this, map_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
⊢ P = 0
have h_option : Q = 0
Tactic: suffices Q = 0 by
      rw [← AlgEquiv.symm_apply_apply (optionEquivLeft R σ) P, ← hQ, this, map_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
x : σ → R
hx : ∀ (i : σ), x i ∈ S (Option.some i)
⊢ Polynomial.map (eval x) Q = 0
have heval : ∀ i ∈ S none, Polynomial.eval i (Polynomial.map (eval x) Q) = 0
Tactic: apply Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zero' _ (S none)
-- 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
x : σ → R
hx : ∀ (i : σ), x i ∈ S (Option.some i)
heval : ∀ i ∈ S none, Polynomial.eval i (Polynomial.map (eval x) Q) = 0
⊢ Polynomial.map (eval x) Q = 0
have hcard : (Polynomial.map (eval x) Q).natDegree < #(S none)
Tactic: apply Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zero' _ (S none)