awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Supported
Goal:
σ : Type u_1
s : Set σ
R : Type u_2
inst : CommRing R
F : MvPolynomial σ ℤ
F' : MvPolynomial { x : σ // x ∈ s } ℤ
hF' :
  (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial { x : σ // x ∈ s } ℤ) → MvPolynomial σ ℤ) F' = F
x : σ → R
⊢ Eq.{u_2 + 1} (α := R)
    ((fun (z : (↑s : Type u_1) → R) ↦
          (((aeval (R := ℤ) z : AlgHom.{0, u_1, u_2} ℤ (MvPolynomial (↑s : Type u_1) ℤ) R) :
                (a : MvPolynomial (↑s : Type u_1) ℤ) → R)
              F' :
            R))
        (x ∘ Subtype.val (p := fun (x : σ) ↦ x ∈ s)) :
      R)
    (((aeval (R := ℤ) x : AlgHom.{0, u_1, u_2} ℤ (MvPolynomial σ ℤ) R) : (a : MvPolynomial σ ℤ) → R) F : R)

Tactic:
simp only [← hF', aeval_rename]

Premises used: MvPolynomial.aeval_rename
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
p : MvPolynomial σ R
⊢ p.degrees.toFinset = p.degrees.toFinset

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
p : MvPolynomial σ R
⊢ p.degrees.toFinset = p.degrees.toFinset

Tactic:
convert! rfl

Premises used: rfl
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
rw : Eq.{u_1 + 1} (α := Finset σ) (Multiset.toFinset (degrees.{u, u_1} (R := R) 0)) ∅
rw₁ : Eq.{u_1 + 1} (α := Finset σ) (Multiset.toFinset 0) ∅
rw₂ rw₃ : Eq.{u_1 + 1} (α := Finset σ) ∅ ∅
⊢ Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) 0) ∅

Tactic:
rw [vars_def, degrees_zero, Multiset.toFinset_zero]

Premises used: Multiset.toFinset_zero, MvPolynomial.vars_def, MvPolynomial.degrees_zero
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
classical : Eq.{u_1 + 1} (α := Finset σ) (Multiset.toFinset (degrees.{u, u_1} (R := R) 0)) ∅
classical₁ : Eq.{u_1 + 1} (α := Finset σ) (Multiset.toFinset 0) ∅
classical₂ classical₃ : Eq.{u_1 + 1} (α := Finset σ) ∅ ∅
⊢ Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) 0) ∅

Tactic:
classical rw [vars_def, degrees_zero, Multiset.toFinset_zero]

Premises used: Multiset.toFinset_zero, MvPolynomial.vars_def, MvPolynomial.degrees_zero
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
r : R
s : σ →₀ ℕ
inst : CommSemiring R
h : r ≠ 0
rw : Multiset.toFinset (degrees.{u, u_1} (R := R) ((monomial s : (a : R) → MvPolynomial σ R) r)) = s.support
rw₁ : Multiset.toFinset ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s) = s.support
rw₂ rw₃ : s.support = s.support
⊢ vars.{u, u_1} (R := R) ((monomial s : (a : R) → MvPolynomial σ R) r) = s.support

Tactic:
rw [vars_def, degrees_monomial_eq _ _ h, Finsupp.toFinset_toMultiset]

Premises used: MvPolynomial.vars_def, Finsupp.toFinset_toMultiset, MvPolynomial.degrees_monomial_eq
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
r : R
s : σ →₀ ℕ
inst : CommSemiring R
h : r ≠ 0
classical : Multiset.toFinset (degrees.{u, u_1} (R := R) ((monomial s : (a : R) → MvPolynomial σ R) r)) = s.support
classical₁ : Multiset.toFinset ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s) = s.support
classical₂ classical₃ : s.support = s.support
⊢ vars.{u, u_1} (R := R) ((monomial s : (a : R) → MvPolynomial σ R) r) = s.support

Tactic:
classical rw [vars_def, degrees_monomial_eq _ _ h, Finsupp.toFinset_toMultiset]

Premises used: MvPolynomial.vars_def, Finsupp.toFinset_toMultiset, MvPolynomial.degrees_monomial_eq
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
r : R
inst : CommSemiring R
rw : Eq.{u_1 + 1} (α := Finset σ) (Multiset.toFinset (degrees.{u, u_1} (R := R) ((C : (a : R) → MvPolynomial σ R) r))) ∅
rw₁ : Eq.{u_1 + 1} (α := Finset σ) (Multiset.toFinset 0) ∅
rw₂ rw₃ : Eq.{u_1 + 1} (α := Finset σ) ∅ ∅
⊢ Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) ((C : (a : R) → MvPolynomial σ R) r)) ∅

Tactic:
rw [vars_def, degrees_C, Multiset.toFinset_zero]

Premises used: MvPolynomial.degrees_C, Multiset.toFinset_zero, MvPolynomial.vars_def
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
r : R
inst : CommSemiring R
classical :
  Eq.{u_1 + 1} (α := Finset σ) (Multiset.toFinset (degrees.{u, u_1} (R := R) ((C : (a : R) → MvPolynomial σ R) r))) ∅
classical₁ : Eq.{u_1 + 1} (α := Finset σ) (Multiset.toFinset 0) ∅
classical₂ classical₃ : Eq.{u_1 + 1} (α := Finset σ) ∅ ∅
⊢ Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) ((C : (a : R) → MvPolynomial σ R) r)) ∅

Tactic:
classical rw [vars_def, degrees_C, Multiset.toFinset_zero]

Premises used: MvPolynomial.degrees_C, Multiset.toFinset_zero, MvPolynomial.vars_def
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
n : σ
inst : CommSemiring R
inst_1 : Nontrivial R
rw : Eq (α := Finset σ) (vars.{u, u_1} (R := R) ((monomial (Finsupp.single n 1) : (a : R) → MvPolynomial σ R) 1)) {n}
rw₁ : Finsupp.support (M := ℕ) (Finsupp.single n 1) = {n}
rw₂ rw₃ : Eq (α := Finset σ) {n} {n}
⊢ vars.{u, u_1} (R := R) (X n) = {n}

Tactic:
rw [X, vars_monomial (one_ne_zero' R), Finsupp.support_single _ (one_ne_zero' ℕ)]

Premises used: Finsupp.support_single, one_ne_zero', MvPolynomial.X, MvPolynomial.vars_monomial, Nat
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i : σ
⊢ i ∈ p.vars ↔ ∃ d ∈ p.support, i ∈ d.support

Tactic:
simp only [vars_def, Multiset.mem_toFinset, mem_degrees, mem_support_iff]

Premises used: MvPolynomial.mem_support_iff, MvPolynomial.vars_def, MvPolynomial.mem_degrees, Multiset.mem_toFinset
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i : σ
⊢ i ∈ p.vars ↔ ∃ d ∈ p.support, i ∈ d.support

Tactic:
classical simp only [vars_def, Multiset.mem_toFinset, mem_degrees, mem_support_iff]

Premises used: MvPolynomial.mem_support_iff, MvPolynomial.vars_def, MvPolynomial.mem_degrees, Multiset.mem_toFinset
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i : σ
⊢ i ∈ p.vars ↔ degreeOf i p ≠ 0

Tactic:
simp [degreeOf, vars_def]

Premises used: MvPolynomial.vars_def, MvPolynomial.degreeOf
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i : σ
⊢ i ∈ p.vars ↔ degreeOf i p ≠ 0

Tactic:
classical simp [degreeOf, vars_def]

Premises used: MvPolynomial.vars_def, MvPolynomial.degreeOf
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
f : MvPolynomial σ R
x : σ →₀ ℕ
H : x ∈ f.support
v : σ
h : v ∉ f.vars
contrapose! : ∀ (h : Ne (α := ℕ) ((x : (a : σ) → ℕ) v : ℕ) (0 : ℕ)), v ∈ f.vars
⊢ Eq (α := ℕ) ((x : (a : σ) → ℕ) v : ℕ) (0 : ℕ)

Tactic:
contrapose! h
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
f : MvPolynomial σ R
x : σ →₀ ℕ
H : x ∈ f.support
v : σ
h : Ne (α := ℕ) ((x : (a : σ) → ℕ) v : ℕ) (0 : ℕ)
⊢ v ∈ f.vars

Tactic:
(mem_vars_iff_mem_support v).mpr ⟨x, H, Finsupp.mem_support_iff.mpr h⟩

Premises used: Iff.mpr, Finsupp.mem_support_iff, And.intro, Exists.intro, MvPolynomial.mem_vars_iff_mem_support
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
f : MvPolynomial σ R
x : σ →₀ ℕ
H : x ∈ f.support
v : σ
h : Ne (α := ℕ) ((x : (a : σ) → ℕ) v : ℕ) (0 : ℕ)
⊢ v ∈ f.vars

Tactic:
exact (mem_vars_iff_mem_support v).mpr ⟨x, H, Finsupp.mem_support_iff.mpr h⟩

Premises used: Iff.mpr, Finsupp.mem_support_iff, And.intro, Exists.intro, MvPolynomial.mem_vars_iff_mem_support
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
s : σ →₀ ℕ
h : s ∈ p.support
i : σ
hi : i ∈ s.support
contrapose! : ∀ (hi : i ∉ p.vars), i ∉ s.support
⊢ i ∈ p.vars

Tactic:
contrapose! hi
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
s : σ →₀ ℕ
h : s ∈ p.support
i : σ
hi : i ∉ p.vars
⊢ i ∉ s.support

Tactic:
simp [mem_support_notMem_vars_zero h hi]

Premises used: MvPolynomial.mem_support_notMem_vars_zero
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
h : p = (C : (a : R) → MvPolynomial σ R) (coeff 0 p)
rw : Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) ((C : (a : R) → MvPolynomial σ R) (coeff 0 p))) ∅
⊢ p.vars = ∅

Tactic:
rw [h]
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
h : p = (C : (a : R) → MvPolynomial σ R) (coeff 0 p)
⊢ Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) ((C : (a : R) → MvPolynomial σ R) (coeff 0 p))) ∅

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
refine : ∀ (h : p.vars = ∅), p = (C : (a : R) → MvPolynomial σ R) (coeff 0 p)
⊢ p.vars = ∅ ↔ p = (C : (a : R) → MvPolynomial σ R) (coeff 0 p)

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by rw [h]; simp⟩
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
h : p.vars = ∅
rw : p.totalDegree = 0
⊢ p = (C : (a : R) → MvPolynomial σ R) (coeff 0 p)

Tactic:
rw [← totalDegree_eq_zero_iff_eq_C]

Premises used: MvPolynomial.totalDegree_eq_zero_iff_eq_C
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
h : p.vars = ∅
this : p.degrees.card = 0
⊢ p.totalDegree = 0

Tactic:
grind [totalDegree_le_degrees_card p]

Premises used: MvPolynomial.totalDegree_le_degrees_card
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
h : p.vars = ∅
suffices : p.degrees.card = 0
⊢ p.totalDegree = 0

Tactic:
suffices p.degrees.card = 0 by grind [totalDegree_le_degrees_card p]
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
h : p.vars = ∅
⊢ p.degrees = 0

Tactic:
rw [vars_def, Multiset.toFinset_eq_empty] at h

Premises used: Multiset.toFinset_eq_empty, MvPolynomial.vars_def
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
h : p.vars = ∅
⊢ p.degrees = 0

Tactic:
classical rw [vars_def, Multiset.toFinset_eq_empty] at h

Premises used: Multiset.toFinset_eq_empty, MvPolynomial.vars_def
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
h : p.degrees = 0
⊢ p.degrees.card = 0

Tactic:
simp_all
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
p q : MvPolynomial σ R
x : σ
hx : x ∈ (p + q).vars
simp : ∀ (hx : x ∈ (p + q).degrees), x ∈ p.degrees ∨ x ∈ q.degrees
⊢ x ∈ p.vars ∪ q.vars

Tactic:
simp only [vars_def, Finset.mem_union, Multiset.mem_toFinset] at hx ⊢

Premises used: MvPolynomial.vars_def, Finset.mem_union, Multiset.mem_toFinset
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
p q : MvPolynomial σ R
x : σ
hx : x ∈ (p + q).degrees
⊢ x ∈ p.degrees ∨ x ∈ q.degrees

Tactic:
simpa using Multiset.mem_of_le degrees_add_le hx

Premises used: Multiset.mem_of_le, MvPolynomial.degrees_add_le
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
inst_1 : DecidableEq σ
h : Disjoint p.vars q.vars
⊢ (p + q).vars = p.vars ∪ q.vars

Tactic:
(vars_add_subset p q).antisymm fun x hx => ?_

Premises used: HasSubset.Subset.antisymm, MvPolynomial.vars_add_subset
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
inst_1 : DecidableEq σ
h : Disjoint p.vars q.vars
refine : ∀ (x : σ) (hx : x ∈ p.vars ∪ q.vars), x ∈ (p + q).vars
⊢ (p + q).vars = p.vars ∪ q.vars

Tactic:
refine (vars_add_subset p q).antisymm fun x hx => ?_

Premises used: HasSubset.Subset.antisymm, MvPolynomial.vars_add_subset
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
inst_1 : DecidableEq σ
h : Disjoint p.vars q.vars
x : σ
hx : x ∈ p.vars ∪ q.vars
simp :
  ∀ (h : Disjoint p.degrees q.degrees) (hx : x ∈ p.degrees.toFinset ∪ q.degrees.toFinset), x ∈ (p + q).degrees.toFinset
⊢ x ∈ (p + q).vars

Tactic:
simp only [vars_def, Multiset.disjoint_toFinset] at h hx ⊢

Premises used: MvPolynomial.vars_def, Multiset.disjoint_toFinset
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
inst_1 : DecidableEq σ
x : σ
h : Disjoint p.degrees q.degrees
hx : x ∈ p.degrees.toFinset ∪ q.degrees.toFinset
rwa : x ∈ (p.degrees ∪ q.degrees).toFinset
rwa₁ rwa₂ rwa₃ rwa₄ : x ∈ p.degrees.toFinset ∪ q.degrees.toFinset
⊢ x ∈ (p + q).degrees.toFinset

Tactic:
rwa [degrees_add_of_disjoint h, Multiset.toFinset_union]

Premises used: Multiset.toFinset_union, MvPolynomial.degrees_add_of_disjoint
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
φ ψ : MvPolynomial σ R
simp_rw : (φ * ψ).degrees ⊆ φ.degrees + ψ.degrees
⊢ (φ * ψ).vars ⊆ φ.vars ∪ ψ.vars

Tactic:
simp_rw [vars_def, ← Multiset.toFinset_add, Multiset.toFinset_subset]

Premises used: Multiset.toFinset_add, MvPolynomial.vars_def, Multiset.toFinset_subset
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
φ ψ : MvPolynomial σ R
⊢ (φ * ψ).degrees ⊆ φ.degrees + ψ.degrees

Tactic:
Multiset.subset_of_le degrees_mul_le

Premises used: Multiset.subset_of_le, MvPolynomial.degrees_mul_le
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
φ ψ : MvPolynomial σ R
⊢ (φ * ψ).degrees ⊆ φ.degrees + ψ.degrees

Tactic:
exact Multiset.subset_of_le degrees_mul_le

Premises used: Multiset.subset_of_le, MvPolynomial.degrees_mul_le
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
⊢ Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) 1) ∅

Tactic:
vars_C

Premises used: MvPolynomial.vars_C, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
φ : MvPolynomial σ R
⊢ (HPow.hPow (β := ℕ) φ 0).vars ⊆ φ.vars

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
ih : (φ ^ n).vars ⊆ φ.vars
succ : (φ * φ ^ n).vars ⊆ φ.vars
⊢ (φ ^ (n + 1)).vars ⊆ φ.vars

Tactic:
rw [pow_succ']

Premises used: pow_succ'
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
ih : (φ ^ n).vars ⊆ φ.vars
succ : φ.vars ∪ (φ ^ n).vars ⊆ φ.vars
⊢ (φ * φ ^ n).vars ⊆ φ.vars

Tactic:
apply Finset.Subset.trans (vars_mul _ _)

Premises used: Finset.Subset.trans, MvPolynomial.vars_mul
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
ih : (φ ^ n).vars ⊆ φ.vars
⊢ φ.vars ∪ (φ ^ n).vars ⊆ φ.vars

Tactic:
Finset.union_subset (Finset.Subset.refl _) ih

Premises used: Finset.union_subset, Finset.Subset.refl
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
ih : (φ ^ n).vars ⊆ φ.vars
⊢ φ.vars ∪ (φ ^ n).vars ⊆ φ.vars

Tactic:
exact Finset.union_subset (Finset.Subset.refl _) ih

Premises used: Finset.union_subset, Finset.Subset.refl
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
zero : (HPow.hPow (β := ℕ) φ 0).vars ⊆ φ.vars
succ : ∀ (n : ℕ) (ih : (φ ^ n).vars ⊆ φ.vars), (φ ^ (n + 1)).vars ⊆ φ.vars
⊢ (φ ^ n).vars ⊆ φ.vars

Tactic:
induction n with
  | zero => simp
  | succ n ih =>
    rw [pow_succ']
    apply Finset.Subset.trans (vars_mul _ _)
    exact Finset.union_subset (Finset.Subset.refl _) ih

Premises used: Finset.Subset.trans, AddMonoidAlgebra.zero, MvPolynomial.vars_mul, pow_succ'
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
zero : (HPow.hPow (β := ℕ) φ 0).vars ⊆ φ.vars
succ : ∀ (n : ℕ) (ih : (φ ^ n).vars ⊆ φ.vars), (φ ^ (n + 1)).vars ⊆ φ.vars
⊢ (φ ^ n).vars ⊆ φ.vars

Tactic:
classical
  induction n with
  | zero => simp
  | succ n ih =>
    rw [pow_succ']
    apply Finset.Subset.trans (vars_mul _ _)
    exact Finset.union_subset (Finset.Subset.refl _) ih

Premises used: Finset.Subset.trans, AddMonoidAlgebra.zero, MvPolynomial.vars_mul, pow_succ'
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
inst_1 : DecidableEq σ
f : ι → MvPolynomial σ R
⊢ Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∏ i ∈ ∅, f i)) (Finset.biUnion ∅ fun (i : ι) ↦ (f i).vars)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
inst_1 : DecidableEq σ
f : ι → MvPolynomial σ R
a : ι
s : Finset ι
hs : a ∉ s
hsub : Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∏ i ∈ s, f i)) (s.biUnion fun (i : ι) ↦ (f i).vars)
insert : (f a * ∏ i ∈ s, f i).vars ⊆ (f a).vars ∪ s.biUnion fun (i : ι) ↦ (f i).vars
⊢ Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∏ i ∈ Insert.insert a s, f i))
    ((Insert.insert a s).biUnion fun (i : ι) ↦ (f i).vars)

Tactic:
simp only [hs, Finset.biUnion_insert, Finset.prod_insert, not_false_iff]

Premises used: Finset.prod_insert, Finset.biUnion_insert, not_false_iff
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
inst_1 : DecidableEq σ
f : ι → MvPolynomial σ R
a : ι
s : Finset ι
hs : a ∉ s
hsub : Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∏ i ∈ s, f i)) (s.biUnion fun (i : ι) ↦ (f i).vars)
insert : (f a).vars ∪ vars.{u, u_1} (R := R) (∏ i ∈ s, f i) ⊆ (f a).vars ∪ s.biUnion fun (i : ι) ↦ (f i).vars
⊢ (f a * ∏ i ∈ s, f i).vars ⊆ (f a).vars ∪ s.biUnion fun (i : ι) ↦ (f i).vars

Tactic:
apply Finset.Subset.trans (vars_mul _ _)

Premises used: Finset.Subset.trans, MvPolynomial.vars_mul
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
inst_1 : DecidableEq σ
f : ι → MvPolynomial σ R
a : ι
s : Finset ι
hs : a ∉ s
hsub : Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∏ i ∈ s, f i)) (s.biUnion fun (i : ι) ↦ (f i).vars)
⊢ (f a).vars ∪ vars.{u, u_1} (R := R) (∏ i ∈ s, f i) ⊆ (f a).vars ∪ s.biUnion fun (i : ι) ↦ (f i).vars

Tactic:
Finset.union_subset_union (Finset.Subset.refl _) hsub

Premises used: Finset.Subset.refl, Finset.union_subset_union
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
inst_1 : DecidableEq σ
f : ι → MvPolynomial σ R
a : ι
s : Finset ι
hs : a ∉ s
hsub : Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∏ i ∈ s, f i)) (s.biUnion fun (i : ι) ↦ (f i).vars)
⊢ (f a).vars ∪ vars.{u, u_1} (R := R) (∏ i ∈ s, f i) ⊆ (f a).vars ∪ s.biUnion fun (i : ι) ↦ (f i).vars

Tactic:
exact Finset.union_subset_union (Finset.Subset.refl _) hsub

Premises used: Finset.Subset.refl, Finset.union_subset_union
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
inst_1 : DecidableEq σ
s : Finset ι
f : ι → MvPolynomial σ R
empty : Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∏ i ∈ ∅, f i)) (Finset.biUnion ∅ fun (i : ι) ↦ (f i).vars)
insert :
  ∀ (a : ι) (s : Finset ι) (hs : a ∉ s)
    (hsub : Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∏ i ∈ s, f i)) (s.biUnion fun (i : ι) ↦ (f i).vars)),
    Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∏ i ∈ Insert.insert a s, f i))
      ((Insert.insert a s).biUnion fun (i : ι) ↦ (f i).vars)
⊢ Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∏ i ∈ s, f i)) (s.biUnion fun (i : ι) ↦ (f i).vars)

Tactic:
induction s using Finset.induction_on with
  | empty => simp
  | insert _ _ hs hsub =>
    simp only [hs, Finset.biUnion_insert, Finset.prod_insert, not_false_iff]
    apply Finset.Subset.trans (vars_mul _ _)
    exact Finset.union_subset_union (Finset.Subset.refl _) hsub

Premises used: Finset.prod_insert, Finset.Subset.trans, Insert.insert, Finset.biUnion_insert, MvPolynomial.vars_mul, not_false_iff
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
inst_1 : DecidableEq σ
s : Finset ι
f : ι → MvPolynomial σ R
empty : Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∏ i ∈ ∅, f i)) (Finset.biUnion ∅ fun (i : ι) ↦ (f i).vars)
insert :
  ∀ (a : ι) (s : Finset ι) (hs : a ∉ s)
    (hsub : Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∏ i ∈ s, f i)) (s.biUnion fun (i : ι) ↦ (f i).vars)),
    Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∏ i ∈ Insert.insert a s, f i))
      ((Insert.insert a s).biUnion fun (i : ι) ↦ (f i).vars)
⊢ Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∏ i ∈ s, f i)) (s.biUnion fun (i : ι) ↦ (f i).vars)

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert _ _ hs hsub =>
    simp only [hs, Finset.biUnion_insert, Finset.prod_insert, not_false_iff]
    apply Finset.Subset.trans (vars_mul _ _)
    exact Finset.union_subset_union (Finset.Subset.refl _) hsub

Premises used: Finset.prod_insert, Finset.Subset.trans, Insert.insert, Finset.biUnion_insert, MvPolynomial.vars_mul, not_false_iff
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
σ : Type u_1
A : Type u_3
inst : CommRing A
inst_1 : NoZeroDivisors A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
h :
  ∀ (i : σ),
    i ∈ (HMul.hMul (α := MvPolynomial σ A) ((C : (a : A) → MvPolynomial σ A) a : MvPolynomial σ A) φ).vars ↔ i ∈ φ.vars
⊢ (HMul.hMul (α := MvPolynomial σ A) ((C : (a : A) → MvPolynomial σ A) a : MvPolynomial σ A) φ).vars = φ.vars

Tactic:
ext1 i
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
σ : Type u_1
A : Type u_3
inst : CommRing A
inst_1 : NoZeroDivisors A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
i : σ
h :
  (∃ (d : σ →₀ ℕ),
      coeff d (HMul.hMul (α := MvPolynomial σ A) ((C : (a : A) → MvPolynomial σ A) a : MvPolynomial σ A) φ) ≠ 0 ∧
        i ∈ d.support) ↔
    ∃ (d : σ →₀ ℕ), coeff d φ ≠ 0 ∧ i ∈ d.support
⊢ i ∈ (HMul.hMul (α := MvPolynomial σ A) ((C : (a : A) → MvPolynomial σ A) a : MvPolynomial σ A) φ).vars ↔ i ∈ φ.vars

Tactic:
simp only [mem_vars_iff_mem_support, mem_support_iff]

Premises used: MvPolynomial.mem_support_iff, MvPolynomial.mem_vars_iff_mem_support
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
σ : Type u_1
A : Type u_3
inst : CommRing A
inst_1 : NoZeroDivisors A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
i : σ
h :
  ∀ (a_1 : σ →₀ ℕ),
    coeff a_1 (HMul.hMul (α := MvPolynomial σ A) ((C : (a : A) → MvPolynomial σ A) a : MvPolynomial σ A) φ) ≠ 0 ∧
        i ∈ a_1.support ↔
      coeff a_1 φ ≠ 0 ∧ i ∈ a_1.support
⊢ (∃ (d : σ →₀ ℕ),
      coeff d (HMul.hMul (α := MvPolynomial σ A) ((C : (a : A) → MvPolynomial σ A) a : MvPolynomial σ A) φ) ≠ 0 ∧
        i ∈ d.support) ↔
    ∃ (d : σ →₀ ℕ), coeff d φ ≠ 0 ∧ i ∈ d.support

Tactic:
apply exists_congr

Premises used: exists_congr