awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : σ
d : σ →₀ ℕ
h : a * coeff d φ ≠ 0 ∧ i ∈ d.support ↔ coeff d φ ≠ 0 ∧ i ∈ d.support
h₁ : (a ≠ 0 ∧ coeff d φ ≠ 0) ∧ i ∈ d.support ↔ coeff d φ ≠ 0 ∧ i ∈ d.support
h₂ : (True ∧ coeff d φ ≠ 0) ∧ i ∈ d.support ↔ coeff d φ ≠ 0 ∧ i ∈ d.support
h₃ h₄ : coeff d φ ≠ 0 ∧ i ∈ d.support ↔ coeff d φ ≠ 0 ∧ i ∈ d.support
⊢ coeff d (HMul.hMul (α := MvPolynomial σ A) ((C : (a : A) → MvPolynomial σ A) a : MvPolynomial σ A) φ) ≠ 0 ∧
      i ∈ d.support ↔
    coeff d φ ≠ 0 ∧ i ∈ d.support

Tactic:
rw [coeff_C_mul, mul_ne_zero_iff, eq_true ha, true_and]

Premises used: MvPolynomial.coeff_C_mul, eq_true, true_and, mul_ne_zero_iff
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst_1 : DecidableEq σ
⊢ Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ ∅, φ i)) (Finset.biUnion ∅ fun (i : ι) ↦ (φ i).vars)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst_1 : DecidableEq σ
a : ι
s : Finset ι
has : a ∉ s
hsum : Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ s, φ i)) (s.biUnion fun (i : ι) ↦ (φ i).vars)
insert : (φ a + ∑ x ∈ s, φ x).vars ⊆ (φ a).vars ∪ s.biUnion fun (i : ι) ↦ (φ i).vars
⊢ Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ Insert.insert a s, φ i))
    ((Insert.insert a s).biUnion fun (i : ι) ↦ (φ i).vars)

Tactic:
rw [Finset.biUnion_insert, Finset.sum_insert has]

Premises used: Finset.biUnion_insert, Finset.sum_insert
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst_1 : DecidableEq σ
a : ι
s : Finset ι
has : a ∉ s
hsum : Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ s, φ i)) (s.biUnion fun (i : ι) ↦ (φ i).vars)
⊢ (φ a + ∑ x ∈ s, φ x).vars ⊆ (φ a).vars ∪ s.biUnion fun (i : ι) ↦ (φ i).vars

Tactic:
Finset.Subset.trans
      (vars_add_subset _ _) (Finset.union_subset_union (Finset.Subset.refl _) ?_)

Premises used: Finset.Subset.trans, Finset.Subset.refl, Finset.union_subset_union, MvPolynomial.vars_add_subset
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst_1 : DecidableEq σ
a : ι
s : Finset ι
has : a ∉ s
hsum insert : Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ x ∈ s, φ x)) (s.biUnion fun (i : ι) ↦ (φ i).vars)
⊢ (φ a + ∑ x ∈ s, φ x).vars ⊆ (φ a).vars ∪ s.biUnion fun (i : ι) ↦ (φ i).vars

Tactic:
refine Finset.Subset.trans
      (vars_add_subset _ _) (Finset.union_subset_union (Finset.Subset.refl _) ?_)

Premises used: Finset.Subset.trans, Finset.Subset.refl, Finset.union_subset_union, MvPolynomial.vars_add_subset
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst_1 : DecidableEq σ
a : ι
s : Finset ι
has : a ∉ s
hsum : Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ s, φ i)) (s.biUnion fun (i : ι) ↦ (φ i).vars)
⊢ Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ x ∈ s, φ x)) (s.biUnion fun (i : ι) ↦ (φ i).vars)

Tactic:
assumption
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst_1 : DecidableEq σ
empty : Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ ∅, φ i)) (Finset.biUnion ∅ fun (i : ι) ↦ (φ i).vars)
insert :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
    (hsum : Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ s, φ i)) (s.biUnion fun (i : ι) ↦ (φ i).vars)),
    Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ Insert.insert a s, φ i))
      ((Insert.insert a s).biUnion fun (i : ι) ↦ (φ i).vars)
⊢ Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ t, φ i)) (t.biUnion fun (i : ι) ↦ (φ i).vars)

Tactic:
induction t using Finset.induction_on with
  | empty => simp
  | insert _ _ has hsum =>
    rw [Finset.biUnion_insert, Finset.sum_insert has]
    refine Finset.Subset.trans
      (vars_add_subset _ _) (Finset.union_subset_union (Finset.Subset.refl _) ?_)
    assumption

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

Tactic:
classical
  induction t using Finset.induction_on with
  | empty => simp
  | insert _ _ has hsum =>
    rw [Finset.biUnion_insert, Finset.sum_insert has]
    refine Finset.Subset.trans
      (vars_add_subset _ _) (Finset.union_subset_union (Finset.Subset.refl _) ?_)
    assumption

Premises used: Finset.Subset.trans, Finset.Subset.refl, Finset.union_subset_union, Insert.insert, Finset.biUnion_insert, MvPolynomial.vars_add_subset
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst_1 : DecidableEq σ
h : Pairwise.{u_3} (α := ι) (onFun.{u_3 + 1, u_1 + 1, 1} (β := Finset σ) Disjoint fun (i : ι) ↦ (φ i).vars)
⊢ Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ ∅, φ i)) (Finset.biUnion ∅ fun (i : ι) ↦ (φ i).vars)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst_1 : DecidableEq σ
h : Pairwise.{u_3} (α := ι) (onFun.{u_3 + 1, u_1 + 1, 1} (β := Finset σ) Disjoint fun (i : ι) ↦ (φ i).vars)
a : ι
s : Finset ι
has : a ∉ s
hsum : Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ s, φ i)) (s.biUnion fun (i : ι) ↦ (φ i).vars)
insert : Disjoint (φ a).vars (vars.{u, u_1} (R := R) (∑ x ∈ s, φ x))
⊢ Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ Insert.insert a s, φ i))
    ((Insert.insert a s).biUnion fun (i : ι) ↦ (φ i).vars)

Tactic:
rw [Finset.biUnion_insert, Finset.sum_insert has, vars_add_of_disjoint, hsum]

Premises used: Finset.biUnion_insert, Finset.sum_insert, MvPolynomial.vars_add_of_disjoint
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst_1 : DecidableEq σ
h : ∀ ⦃i j : ι⦄, i ≠ j → Disjoint.{u_1} (α := Finset σ) ((fun (i : ι) ↦ (φ i).vars) i) ((fun (i : ι) ↦ (φ i).vars) j)
a : ι
s : Finset ι
has : a ∉ s
hsum : Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ s, φ i)) (s.biUnion fun (i : ι) ↦ (φ i).vars)
insert :
  ∀ (h : ∀ ⦃i j : ι⦄, i ≠ j → ∀ a ∈ (φ i).vars, ∀ b ∈ (φ j).vars, a ≠ b),
    ∀ a_1 ∈ (φ a).vars, ∀ (b : σ), Membership.mem (γ := Finset σ) (vars.{u, u_1} (R := R) (∑ x ∈ s, φ x)) b → a_1 ≠ b
⊢ Disjoint (φ a).vars (vars.{u, u_1} (R := R) (∑ x ∈ s, φ x))

Tactic:
simp only [Finset.disjoint_iff_ne] at h ⊢

Premises used: Finset.disjoint_iff_ne
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst_1 : DecidableEq σ
a : ι
s : Finset ι
has : a ∉ s
hsum : Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ s, φ i)) (s.biUnion fun (i : ι) ↦ (φ i).vars)
h : ∀ ⦃i j : ι⦄, i ≠ j → ∀ a ∈ (φ i).vars, ∀ b ∈ (φ j).vars, a ≠ b
⊢ ∀ a_1 ∈ (φ a).vars, ∀ (b : σ), Membership.mem (γ := Finset σ) (vars.{u, u_1} (R := R) (∑ x ∈ s, φ x)) b → a_1 ≠ b

Tactic:
grind
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst_1 : DecidableEq σ
h : Pairwise.{u_3} (α := ι) (onFun.{u_3 + 1, u_1 + 1, 1} (β := Finset σ) Disjoint fun (i : ι) ↦ (φ i).vars)
empty : Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ ∅, φ i)) (Finset.biUnion ∅ fun (i : ι) ↦ (φ i).vars)
insert :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
    (hsum : Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ s, φ i)) (s.biUnion fun (i : ι) ↦ (φ i).vars)),
    Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ Insert.insert a s, φ i))
      ((Insert.insert a s).biUnion fun (i : ι) ↦ (φ i).vars)
⊢ Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ t, φ i)) (t.biUnion fun (i : ι) ↦ (φ i).vars)

Tactic:
induction t using Finset.induction_on with
  | empty => simp
  | insert _ _ has hsum =>
    rw [Finset.biUnion_insert, Finset.sum_insert has, vars_add_of_disjoint, hsum]
    unfold Pairwise onFun at h
    simp only [Finset.disjoint_iff_ne] at h ⊢
    grind

Premises used: Function.onFun, Insert.insert, Finset.disjoint_iff_ne, Finset.biUnion_insert, Pairwise, MvPolynomial.vars_add_of_disjoint
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst_1 : DecidableEq σ
h : Pairwise.{u_3} (α := ι) (onFun.{u_3 + 1, u_1 + 1, 1} (β := Finset σ) Disjoint fun (i : ι) ↦ (φ i).vars)
empty : Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ ∅, φ i)) (Finset.biUnion ∅ fun (i : ι) ↦ (φ i).vars)
insert :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
    (hsum : Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ s, φ i)) (s.biUnion fun (i : ι) ↦ (φ i).vars)),
    Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ Insert.insert a s, φ i))
      ((Insert.insert a s).biUnion fun (i : ι) ↦ (φ i).vars)
⊢ Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ t, φ i)) (t.biUnion fun (i : ι) ↦ (φ i).vars)

Tactic:
classical
  induction t using Finset.induction_on with
  | empty => simp
  | insert _ _ has hsum =>
    rw [Finset.biUnion_insert, Finset.sum_insert has, vars_add_of_disjoint, hsum]
    unfold Pairwise onFun at h
    simp only [Finset.disjoint_iff_ne] at h ⊢
    grind

Premises used: Function.onFun, Insert.insert, Finset.disjoint_iff_ne, Finset.biUnion_insert, Pairwise, MvPolynomial.vars_add_of_disjoint
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
inst_1 : CommSemiring S
f : R →+* S
⊢ vars.{v, u_1} (R := S) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S) p) ⊆ p.vars

Tactic:
simp [vars_def, Multiset.subset_of_le degrees_map_le]

Premises used: Multiset.subset_of_le, MvPolynomial.degrees_map_le, MvPolynomial.vars_def
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
inst_1 : CommSemiring S
f : R →+* S
⊢ vars.{v, u_1} (R := S) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S) p) ⊆ p.vars

Tactic:
classical simp [vars_def, Multiset.subset_of_le degrees_map_le]

Premises used: Multiset.subset_of_le, MvPolynomial.degrees_map_le, MvPolynomial.vars_def
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
inst_1 : CommSemiring S
f : R →+* S
hf : Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ vars.{v, u_1} (R := S) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S) p) = p.vars

Tactic:
simp [vars, degrees_map_of_injective _ hf]

Premises used: MvPolynomial.degrees_map_of_injective, MvPolynomial.vars
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
i : σ
e : ℕ
r : R
he : e ≠ 0
hr : r ≠ 0
rw : Finsupp.support (Finsupp.single i e) = {i}
rw₁ rw₂ : Eq (α := Finset σ) {i} {i}
⊢ Eq (α := Finset σ) (vars.{u, u_1} (R := R) ((monomial (Finsupp.single i e) : (a : R) → MvPolynomial σ R) r)) {i}

Tactic:
rw [vars_monomial hr, Finsupp.support_single _ he]

Premises used: Finsupp.support_single, MvPolynomial.vars_monomial
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
inst_1 : DecidableEq σ
h : ∀ (i : σ), i ∈ p.vars ↔ i ∈ p.support.biUnion Finsupp.support
⊢ p.vars = p.support.biUnion Finsupp.support

Tactic:
ext i
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
inst_1 : DecidableEq σ
i : σ
h : (∃ d ∈ p.support, i ∈ d.support) ↔ i ∈ p.support.biUnion Finsupp.support
h₁ h₂ : (∃ d ∈ p.support, i ∈ d.support) ↔ ∃ a ∈ p.support, i ∈ a.support
⊢ i ∈ p.vars ↔ i ∈ p.support.biUnion Finsupp.support

Tactic:
rw [mem_vars_iff_mem_support, Finset.mem_biUnion]

Premises used: Finset.mem_biUnion, MvPolynomial.mem_vars_iff_mem_support
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
rw :
  ((eval₂Hom f g : (a : MvPolynomial σ R) → S)
      (∑ v ∈ p.support, (monomial v : (a : R) → MvPolynomial σ R) (coeff v p)) :
    S)
| ((eval₂Hom f g : (a : MvPolynomial σ R) → S) p : S)

Tactic:
rw [p.as_sum]

Premises used: MvPolynomial.as_sum
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
conv_lhs :
  Eq.{v + 1} (α := S)
    ((eval₂Hom f g : (a : MvPolynomial σ R) → S)
        (∑ v ∈ p.support, (monomial v : (a : R) → MvPolynomial σ R) (coeff v p)) :
      S)
    ((f : (a : R) → S) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) : S)
⊢ Eq.{v + 1} (α := S) ((eval₂Hom f g : (a : MvPolynomial σ R) → S) p : S)
    ((f : (a : R) → S) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) : S)

Tactic:
conv_lhs => rw [p.as_sum]

Premises used: MvPolynomial.as_sum
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
simp :
  Eq.{v + 1} (α := S)
    (∑ x ∈ p.support,
        HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff x p) : S) (x.prod fun (i : σ) (k : ℕ) ↦ g i ^ k : S) :
      S)
    ((f : (a : R) → S) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) : S)
⊢ Eq.{v + 1} (α := S)
    ((eval₂Hom f g : (a : MvPolynomial σ R) → S)
        (∑ v ∈ p.support, (monomial v : (a : R) → MvPolynomial σ R) (coeff v p)) :
      S)
    ((f : (a : R) → S) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) : S)

Tactic:
simp only [map_sum, eval₂Hom_monomial]

Premises used: MvPolynomial.eval₂Hom_monomial, map_sum
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
pos :
  ∀ (h0 : Eq.{u + 1} (α := R) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) (0 : R)),
    Eq.{v + 1} (α := S)
      (∑ x ∈ p.support,
          HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff x p) : S) (x.prod fun (i : σ) (k : ℕ) ↦ g i ^ k : S) :
        S)
      ((f : (a : R) → S) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) : S)
neg :
  ∀ (h0 : ¬Eq.{u + 1} (α := R) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) (0 : R)),
    Eq.{v + 1} (α := S)
      (∑ x ∈ p.support,
          HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff x p) : S) (x.prod fun (i : σ) (k : ℕ) ↦ g i ^ k : S) :
        S)
      ((f : (a : R) → S) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) : S)
⊢ Eq.{v + 1} (α := S)
    (∑ x ∈ p.support,
        HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff x p) : S) (x.prod fun (i : σ) (k : ℕ) ↦ g i ^ k : S) :
      S)
    ((f : (a : R) → S) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) : S)

Tactic:
by_cases h0 : constantCoeff p = 0

Premises used: MvPolynomial.constantCoeff, DFunLike.coe
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : Eq.{u + 1} (α := R) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) (0 : R)
pos :
  ∀ x ∈ p.support,
    HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff x p) : S) (x.prod fun (i : σ) (k : ℕ) ↦ g i ^ k : S) = 0
⊢ Eq.{v + 1} (α := S)
    (∑ x ∈ p.support,
        HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff x p) : S) (x.prod fun (i : σ) (k : ℕ) ↦ g i ^ k : S) :
      S)
    ((f : (a : R) → S) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) : S)

Tactic:
rw [h0, f.map_zero, Finset.sum_eq_zero]

Premises used: Finset.sum_eq_zero, RingHom.map_zero
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : Eq.{u + 1} (α := R) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) (0 : R)
pos :
  ∀ (d : σ →₀ ℕ) (hd : d ∈ p.support),
    HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff d p) : S) (d.prod fun (i : σ) (k : ℕ) ↦ g i ^ k : S) = 0
⊢ Eq.{v + 1} (α := S)
    (∑ x ∈ p.support,
        HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff x p) : S) (x.prod fun (i : σ) (k : ℕ) ↦ g i ^ k : S) :
      S)
    ((f : (a : R) → S) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) : S)

Tactic:
on_goal 1 =>
    rw [h0, f.map_zero, Finset.sum_eq_zero]
    intro d hd

Premises used: Finset.sum_eq_zero, RingHom.map_zero
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬Eq.{u + 1} (α := R) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) (0 : R)
neg :
  HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff 0 p) : S) (Finsupp.prod 0 fun (i : σ) (k : ℕ) ↦ g i ^ k : S) =
    (f : (a : R) → S) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R)
neg₁ :
  ∀ b ∈ p.support,
    b ≠ 0 →
      HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff b p) : S) (b.prod fun (i : σ) (k : ℕ) ↦ g i ^ k : S) = 0
neg₂ :
  0 ∉ p.support →
    HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff 0 p) : S) (Finsupp.prod 0 fun (i : σ) (k : ℕ) ↦ g i ^ k : S) =
      0
⊢ Eq.{v + 1} (α := S)
    (∑ x ∈ p.support,
        HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff x p) : S) (x.prod fun (i : σ) (k : ℕ) ↦ g i ^ k : S) :
      S)
    ((f : (a : R) → S) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) : S)

Tactic:
rw [Finset.sum_eq_single (0 : σ →₀ ℕ)]

Premises used: Finset.sum_eq_single, OfNat.ofNat
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬Eq.{u + 1} (α := R) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) (0 : R)
neg :
  Eq.{v + 1} (α := S) ((f : (a : R) → S) (coeff 0 p) : S)
    ((f : (a : R) → S) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) : S)
⊢ HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff 0 p) : S) (Finsupp.prod 0 fun (i : σ) (k : ℕ) ↦ g i ^ k : S) =
    (f : (a : R) → S) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R)

Tactic:
rw [Finsupp.prod_zero_index, mul_one]

Premises used: mul_one, Finsupp.prod_zero_index
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬Eq.{u + 1} (α := R) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) (0 : R)
⊢ Eq.{v + 1} (α := S) ((f : (a : R) → S) (coeff 0 p) : S)
    ((f : (a : R) → S) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) : S)

Tactic:
rfl
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬Eq.{u + 1} (α := R) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) (0 : R)
neg :
  ∀ (d : σ →₀ ℕ) (hd : d ∈ p.support) (hd0 : d ≠ 0),
    HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff d p) : S) (d.prod fun (i : σ) (k : ℕ) ↦ g i ^ k : S) = 0
⊢ ∀ b ∈ p.support,
    b ≠ 0 →
      HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff b p) : S) (b.prod fun (i : σ) (k : ℕ) ↦ g i ^ k : S) = 0

Tactic:
on_goal 1 => intro d hd hd0
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬Eq.{u + 1} (α := R) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) (0 : R)
neg :
  ∀ (d : σ →₀ ℕ) (hd : d ∈ p.support) (hd0 : d ≠ 0),
    HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff d p) : S) (d.prod fun (i : σ) (k : ℕ) ↦ g i ^ k : S) = 0
neg₁ :
  0 ∉ p.support →
    HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff 0 p) : S) (Finsupp.prod 0 fun (i : σ) (k : ℕ) ↦ g i ^ k : S) =
      0
⊢ Eq.{v + 1} (α := S)
    (∑ x ∈ p.support,
        HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff x p) : S) (x.prod fun (i : σ) (k : ℕ) ↦ g i ^ k : S) :
      S)
    ((f : (a : R) → S) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) : S)

Tactic:
on_goal 2 =>
    rw [Finset.sum_eq_single (0 : σ →₀ ℕ)]
    · rw [Finsupp.prod_zero_index, mul_one]
      rfl
    on_goal 1 => intro d hd hd0

Premises used: Finset.sum_eq_single, mul_one, OfNat.ofNat, Finsupp.prod_zero_index
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬Eq.{u + 1} (α := R) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) (0 : R)
⊢ 0 ∈ p.support

Tactic:
rw [constantCoeff_eq, coeff, ← Ne, ← Finsupp.mem_support_iff] at h0

Premises used: Finsupp.mem_support_iff, Ne, MvPolynomial.coeff, MvPolynomial.constantCoeff_eq
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : 0 ∈ p.support
h : 0 ∉ p.support
⊢ HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff 0 p) : S) (Finsupp.prod 0 fun (i : σ) (k : ℕ) ↦ g i ^ k : S) = 0

Tactic:
contradiction
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬Eq.{u + 1} (α := R) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) (0 : R)
⊢ 0 ∉ p.support →
    HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff 0 p) : S) (Finsupp.prod 0 fun (i : σ) (k : ℕ) ↦ g i ^ k : S) =
      0

Tactic:
on_goal 3 =>
    rw [constantCoeff_eq, coeff, ← Ne, ← Finsupp.mem_support_iff] at h0
    intro
    contradiction

Premises used: Finsupp.mem_support_iff, Ne, MvPolynomial.coeff, MvPolynomial.constantCoeff_eq
-- Module: Mathlib.Algebra.MvPolynomial.Variables
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : Eq.{u + 1} (α := R) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) (0 : R)
d : σ →₀ ℕ
hd : d ∈ p.support
rw : ∀ (h0 : 0 ∉ p.support) (d : σ →₀ ℕ) (hd : d ∈ p.support), d.support.Nonempty
⊢ d.support.Nonempty

Tactic:
rw [constantCoeff_eq, coeff, ← Finsupp.notMem_support_iff] at h0

Premises used: Finsupp.notMem_support_iff, MvPolynomial.coeff, MvPolynomial.constantCoeff_eq