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
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)
this :
  Eq (α := MvPolynomial σ R)
    ((rename (⇑e.symm : (a : τ) → σ) : (a : MvPolynomial τ R) → MvPolynomial σ R) P : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
⊢ Injective (α := MvPolynomial τ R) (β := MvPolynomial σ R)
    (⇑(rename (⇑e.symm : (a : τ) → σ)) : (a : MvPolynomial τ R) → MvPolynomial σ R)

Tactic:
have that := MvPolynomial.rename_injective (R := R) e.symm (e.symm.injective)
-- 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
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)
this :
  Eq (α := MvPolynomial σ R)
    ((rename (⇑e.symm : (a : τ) → σ) : (a : MvPolynomial τ R) → MvPolynomial σ R) P : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
that :
  Injective (α := MvPolynomial τ R) (β := MvPolynomial σ R)
    (⇑(rename (⇑e.symm : (a : τ) → σ)) : (a : MvPolynomial τ R) → MvPolynomial σ R)
⊢ Eq (α := Ideal (MvPolynomial τ R))
    (RingHom.ker (F := MvPolynomial τ R →ₐ[R] MvPolynomial σ R) (rename (⇑e.symm : (a : τ) → σ))) ⊥

Tactic:
rw [RingHom.injective_iff_ker_eq_bot] at that

Premises used: RingHom.injective_iff_ker_eq_bot
-- 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
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)
this :
  Eq (α := MvPolynomial σ R)
    ((rename (⇑e.symm : (a : τ) → σ) : (a : MvPolynomial τ R) → MvPolynomial σ R) P : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
that :
  Eq (α := Ideal (MvPolynomial τ R))
    (RingHom.ker (F := MvPolynomial τ R →ₐ[R] MvPolynomial σ R) (rename (⇑e.symm : (a : τ) → σ))) ⊥
rwa :
  ∀
    (this :
      Membership.mem (γ := Ideal (MvPolynomial τ R))
        (RingHom.ker (F := MvPolynomial τ R →ₐ[R] MvPolynomial σ R) (rename (⇑e.symm : (a : τ) → σ))) P)
    (that :
      Eq (α := Ideal (MvPolynomial τ R))
        (RingHom.ker (F := MvPolynomial τ R →ₐ[R] MvPolynomial σ R) (rename (⇑e.symm : (a : τ) → σ))) ⊥),
    P = 0
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (this : Membership.mem (γ := Ideal (MvPolynomial τ R)) ⊥ P)
    (that :
      Eq (α := Ideal (MvPolynomial τ R))
        (RingHom.ker (F := MvPolynomial τ R →ₐ[R] MvPolynomial σ R) (rename (⇑e.symm : (a : τ) → σ))) ⊥),
    P = 0
⊢ P = 0

Tactic:
rwa [← RingHom.mem_ker, that] at this

Premises used: RingHom.mem_ker
-- 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
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)
of_equiv :
  Eq (α := MvPolynomial σ R)
    ((rename (⇑e.symm : (a : τ) → σ) : (a : MvPolynomial τ R) → MvPolynomial σ R) P : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
⊢ P = 0

Tactic:
suffices MvPolynomial.rename e.symm P = 0 by
      have that := MvPolynomial.rename_injective (R := R) e.symm (e.symm.injective)
      rw [RingHom.injective_iff_ker_eq_bot] at that
      rwa [← RingHom.mem_ker, that] at this
-- 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
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)
of_equiv :
  ∀ (i : σ),
    degreeOf.{u_1, u_2} (R := R) i ((rename (⇑e.symm : (a : τ) → σ) : (a : MvPolynomial τ R) → MvPolynomial σ R) P) <
      #(S ((e : (a : σ) → τ) i))
of_equiv₁ :
  ∀ (x : σ → R),
    (∀ (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)
⊢ Eq (α := MvPolynomial σ R)
    ((rename (⇑e.symm : (a : τ) → σ) : (a : MvPolynomial τ R) → MvPolynomial σ R) P : MvPolynomial σ R)
    (0 : MvPolynomial σ R)

Tactic:
apply h _ (fun i ↦ S (e i))

Premises used: DFunLike.coe
-- 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
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 ((e : (a : σ) → τ) i) P < #(S ((e : (a : σ) → τ) i))

Tactic:
Hdeg (e i)

Premises used: DFunLike.coe
-- 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
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 : σ
h₁ :
  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) <
    #(S ((e : (a : σ) → τ) i))

Tactic:
convert! Hdeg (e i)

Premises used: DFunLike.coe
-- 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
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 : σ
rw : degreeOf ((e : (a : σ) → τ) i) P
| degreeOf.{u_1, u_2} (R := R) i ((rename (⇑e.symm : (a : τ) → σ) : (a : MvPolynomial τ R) → MvPolynomial σ R) P)

Tactic:
rw [← e.symm_apply_apply i, degreeOf_rename_of_injective e.symm.injective]

Premises used: Equiv.symm_apply_apply, MvPolynomial.degreeOf_rename_of_injective, Equiv.injective, Equiv.symm
-- 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
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
h₁ : degreeOf ((e : (a : σ) → τ) i) 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

Tactic:
conv_lhs => rw [← e.symm_apply_apply i, degreeOf_rename_of_injective e.symm.injective]

Premises used: Equiv.symm_apply_apply, MvPolynomial.degreeOf_rename_of_injective, Equiv.injective, Equiv.symm
-- 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
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 : σ
h₁ :
  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) <
    #(S ((e : (a : σ) → τ) i))

Tactic:
classical
      convert! Hdeg (e i)
      conv_lhs => rw [← e.symm_apply_apply i, degreeOf_rename_of_injective e.symm.injective]

Premises used: Equiv.symm_apply_apply, MvPolynomial.degreeOf_rename_of_injective, Equiv.injective, Equiv.symm, DFunLike.coe
-- 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
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)
of_equiv : Eq.{u_1 + 1} (α := R) ((eval (x ∘ (⇑e.symm : (a : τ) → σ)) : (a : MvPolynomial τ R) → R) P : R) (0 : R)
⊢ 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)

Tactic:
simp only [MvPolynomial.eval_rename]

Premises used: MvPolynomial.eval_rename
-- 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
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)
of_equiv : ∀ (i : τ), (x ∘ (⇑e.symm : (a : τ) → σ)) i ∈ S i
⊢ Eq.{u_1 + 1} (α := R) ((eval (x ∘ (⇑e.symm : (a : τ) → σ)) : (a : MvPolynomial τ R) → R) P : R) (0 : R)

Tactic:
apply Heval
-- 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
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 : τ
of_equiv : x ((e.symm : (a : τ) → σ) s) ∈ S s
⊢ (x ∘ (⇑e.symm : (a : τ) → σ)) s ∈ S s

Tactic:
simp only [Function.comp_apply]

Premises used: Function.comp_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
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 ((e : (a : σ) → τ) ((e.symm : (a : τ) → σ) s : σ))

Tactic:
hx (e.symm s)

Premises used: Equiv.symm, DFunLike.coe
-- 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
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 : τ
h₁ : s = (e : (a : σ) → τ) ((e.symm : (a : τ) → σ) s : σ)
⊢ x ((e.symm : (a : τ) → σ) s) ∈ S s

Tactic:
convert! hx (e.symm s)

Premises used: Equiv.symm, DFunLike.coe
-- 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
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 : τ
⊢ s = (e : (a : σ) → τ) ((e.symm : (a : τ) → σ) s : σ)

Tactic:
simp only [Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Combinatorics.Nullstellensatz
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)
⊢ 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)

Premises used: Inhabited.default, PEmpty.elim
-- Module: Mathlib.Combinatorics.Nullstellensatz
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)
⊢ 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

Premises used: MvPolynomial.eval_C
-- Module: Mathlib.Combinatorics.Nullstellensatz
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
rw₂ rw₃ : Eq (α := MvPolynomial PEmpty.{u_2 + 1} R) 0 0
⊢ P = 0

Tactic:
rw [this, Heval, C_0]

Premises used: MvPolynomial.C_0
-- Module: Mathlib.Combinatorics.Nullstellensatz
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)
h_empty :
  P = (C : (a : R) → MvPolynomial PEmpty.{u_2 + 1} R) ((constantCoeff : (a : MvPolynomial PEmpty.{u_2 + 1} R) → R) P)
⊢ P = 0

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]
-- Module: Mathlib.Combinatorics.Nullstellensatz
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)
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))
⊢ P = (C : (a : R) → MvPolynomial PEmpty.{u_2 + 1} R) ((constantCoeff : (a : MvPolynomial PEmpty.{u_2 + 1} R) → R) P)

Tactic:
ext m
-- Module: Mathlib.Combinatorics.Nullstellensatz
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} →₀ ℕ
this : m = 0
⊢ 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:
simp [this, ← constantCoeff_eq]

Premises used: MvPolynomial.constantCoeff_eq
-- Module: Mathlib.Combinatorics.Nullstellensatz
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} →₀ ℕ
h_empty : m = 0
⊢ 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:
suffices m = 0 by simp [this, ← constantCoeff_eq]
-- Module: Mathlib.Combinatorics.Nullstellensatz
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} →₀ ℕ
h_empty :
  ∀ (d : PEmpty.{u_2 + 1}),
    Eq (α := ℕ) ((m : (a : PEmpty.{u_2 + 1}) → ℕ) d : ℕ) ((0 : (a : PEmpty.{u_2 + 1}) → ℕ) d : ℕ)
⊢ m = 0

Tactic:
ext d
-- Module: Mathlib.Combinatorics.Nullstellensatz
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} →₀ ℕ
d : PEmpty.{u_2 + 1}
⊢ Eq (α := ℕ) ((m : (a : PEmpty.{u_2 + 1}) → ℕ) d : ℕ) ((0 : (a : PEmpty.{u_2 + 1}) → ℕ) d : ℕ)

Tactic:
PEmpty.elim d

Premises used: PEmpty.elim
-- Module: Mathlib.Combinatorics.Nullstellensatz
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} →₀ ℕ
d : PEmpty.{u_2 + 1}
⊢ Eq (α := ℕ) ((m : (a : PEmpty.{u_2 + 1}) → ℕ) d : ℕ) ((0 : (a : PEmpty.{u_2 + 1}) → ℕ) d : ℕ)

Tactic:
exact PEmpty.elim d

Premises used: PEmpty.elim