awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq R
r : R
⊢ Eq (α := Finset R) (coeffs.{u, u_1} (σ := σ) ((C : (a : R) → MvPolynomial σ R) r)) (if r = 0 then ∅ else {r})

Tactic:
aesop (add simp mem_coeffs_iff)

Premises used: MvPolynomial.mem_coeffs_iff
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq R
r : R
⊢ Eq (α := Finset R) (coeffs.{u, u_1} (σ := σ) ((C : (a : R) → MvPolynomial σ R) r)) (if r = 0 then ∅ else {r})

Tactic:
classical
  aesop (add simp mem_coeffs_iff)

Premises used: MvPolynomial.mem_coeffs_iff
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
r : R
rw : Subset (α := Finset R) (if r = 0 then ∅ else {r}) {r}
⊢ Subset (α := Finset R) (coeffs.{u, u_1} (σ := σ) ((C : (a : R) → MvPolynomial σ R) r)) {r}

Tactic:
rw [coeffs_C]

Premises used: MvPolynomial.coeffs_C
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
r : R
isTrue : r = 0 → Subset (α := Finset R) ∅ {r}
isFalse : ¬r = 0 → Subset (α := Finset R) {r} {r}
⊢ Subset (α := Finset R) (if r = 0 then ∅ else {r}) {r}

Tactic:
split
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
r : R
h : r = 0
⊢ Subset (α := Finset R) ∅ {r}

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
r : R
h : ¬r = 0
⊢ Subset (α := Finset R) {r} {r}

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
r : R
rw rw₁ rw₂ : Subset (α := Finset R) (if r = 0 then ∅ else {r}) {r}
⊢ Subset (α := Finset R) (coeffs.{u, u_1} (σ := σ) ((C : (a : R) → MvPolynomial σ R) r)) {r}

Tactic:
classical
  rw [coeffs_C]
  split <;> simp

Premises used: MvPolynomial.coeffs_C
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
n : σ
⊢ (p * X n).coeffs = p.coeffs

Tactic:
aesop (add simp mem_coeffs_iff)

Premises used: MvPolynomial.mem_coeffs_iff
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
n : σ
⊢ (p * X n).coeffs = p.coeffs

Tactic:
classical
  aesop (add simp mem_coeffs_iff)

Premises used: MvPolynomial.mem_coeffs_iff
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
n : σ
⊢ (X n * p).coeffs = p.coeffs

Tactic:
aesop (add simp mem_coeffs_iff)

Premises used: MvPolynomial.mem_coeffs_iff
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
n : σ
⊢ (X n * p).coeffs = p.coeffs

Tactic:
classical
  aesop (add simp mem_coeffs_iff)

Premises used: MvPolynomial.mem_coeffs_iff
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq R
p q : MvPolynomial σ R
h : Disjoint p.support q.support
h₁ : ∀ (r : R), r ∈ (p + q).coeffs ↔ r ∈ p.coeffs ∪ q.coeffs
⊢ (p + q).coeffs = p.coeffs ∪ q.coeffs

Tactic:
ext r
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq R
p q : MvPolynomial σ R
h : Disjoint p.support q.support
r : R
h₁ :
  (∃ (n : σ →₀ ℕ), ¬coeff n p + coeff n q = 0 ∧ r = coeff n p + coeff n q) ↔
    (∃ (n : σ →₀ ℕ), ¬coeff n p = 0 ∧ r = coeff n p) ∨ ∃ (n : σ →₀ ℕ), ¬coeff n q = 0 ∧ r = coeff n q
⊢ r ∈ (p + q).coeffs ↔ r ∈ p.coeffs ∪ q.coeffs

Tactic:
simp only [mem_coeffs_iff, mem_support_iff, coeff_add, ne_eq, Finset.mem_union]

Premises used: MvPolynomial.mem_support_iff, ne_eq, MvPolynomial.coeff_add, Finset.mem_union, MvPolynomial.mem_coeffs_iff
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq R
p q : MvPolynomial σ R
h : Disjoint p.support q.support
r : R
⊢ ∀ (n : σ →₀ ℕ) (hne : coeff n p ≠ 0), coeff n q = 0

Tactic:
have hl (n : σ →₀ ℕ) (hne : p.coeff n ≠ 0) : q.coeff n = 0 :=
    notMem_support_iff.mp <| h.notMem_of_mem_left_finset (mem_support_iff.mpr hne)
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq R
p q : MvPolynomial σ R
h : Disjoint p.support q.support
r : R
hl : ∀ (n : σ →₀ ℕ) (hne : coeff n p ≠ 0), coeff n q = 0
⊢ ∀ (n : σ →₀ ℕ) (hne : coeff n q ≠ 0), coeff n p = 0

Tactic:
have hr (n : σ →₀ ℕ) (hne : q.coeff n ≠ 0) : p.coeff n = 0 :=
    notMem_support_iff.mp <| h.notMem_of_mem_right_finset (mem_support_iff.mpr hne)
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq R
p q : MvPolynomial σ R
h_1 : Disjoint p.support q.support
r : R
hl : ∀ (n : σ →₀ ℕ) (hne : coeff n p ≠ 0), coeff n q = 0
hr : ∀ (n : σ →₀ ℕ) (hne : coeff n q ≠ 0), coeff n p = 0
n : σ →₀ ℕ
h : ¬coeff n p + coeff n q = 0
pos : ∀ (hp : coeff n p = 0), coeff n p ≠ 0 ∨ coeff n q ≠ 0
neg : ∀ (hp : ¬coeff n p = 0), coeff n p ≠ 0 ∨ coeff n q ≠ 0
⊢ coeff n p ≠ 0 ∨ coeff n q ≠ 0

Tactic:
by_cases hp : coeff n p = 0

Premises used: MvPolynomial.coeff
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq R
p q : MvPolynomial σ R
h_1 : Disjoint p.support q.support
r : R
hl : ∀ (n : σ →₀ ℕ) (hne : coeff n p ≠ 0), coeff n q = 0
hr : ∀ (n : σ →₀ ℕ) (hne : coeff n q ≠ 0), coeff n p = 0
n : σ →₀ ℕ
h : ¬coeff n p + coeff n q = 0
hp : coeff n p = 0
⊢ coeff n p ≠ 0 ∨ coeff n q ≠ 0

Tactic:
simp_all
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq R
p q : MvPolynomial σ R
h_1 : Disjoint p.support q.support
r : R
hl : ∀ (n : σ →₀ ℕ) (hne : coeff n p ≠ 0), coeff n q = 0
hr : ∀ (n : σ →₀ ℕ) (hne : coeff n q ≠ 0), coeff n p = 0
n : σ →₀ ℕ
h : ¬coeff n p + coeff n q = 0
hp : ¬coeff n p = 0
⊢ coeff n p ≠ 0 ∨ coeff n q ≠ 0

Tactic:
simp_all
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq R
p q : MvPolynomial σ R
h : Disjoint p.support q.support
r : R
hl : ∀ (n : σ →₀ ℕ) (hne : coeff n p ≠ 0), coeff n q = 0
hr : ∀ (n : σ →₀ ℕ) (hne : coeff n q ≠ 0), coeff n p = 0
⊢ ∀ (n : σ →₀ ℕ) (h : ¬coeff n p + coeff n q = 0), coeff n p ≠ 0 ∨ coeff n q ≠ 0

Tactic:
have hor (n) (h : ¬coeff n p + coeff n q = 0) : coeff n p ≠ 0 ∨ coeff n q ≠ 0 := by
    by_cases hp : coeff n p = 0 <;> simp_all
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq R
p q : MvPolynomial σ R
h : Disjoint p.support q.support
r : R
hl : ∀ (n : σ →₀ ℕ) (hne : coeff n p ≠ 0), coeff n q = 0
hr : ∀ (n : σ →₀ ℕ) (hne : coeff n q ≠ 0), coeff n p = 0
hor : ∀ (n : σ →₀ ℕ) (h : ¬coeff n p + coeff n q = 0), coeff n p ≠ 0 ∨ coeff n q ≠ 0
⊢ (∃ (n : σ →₀ ℕ), ¬coeff n p + coeff n q = 0 ∧ r = coeff n p + coeff n q) ↔
    (∃ (n : σ →₀ ℕ), ¬coeff n p = 0 ∧ r = coeff n p) ∨ ∃ (n : σ →₀ ℕ), ¬coeff n q = 0 ∧ r = coeff n q

Tactic:
⟨fun ⟨n, hn1, hn2⟩ ↦ ?_, ?_⟩

Premises used: _private.0.MvPolynomial.coeffs_add.match_1, Exists, MvPolynomial.coeff, And, Iff.intro, Or, OfNat.ofNat, Eq, Not
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq R
p q : MvPolynomial σ R
h : Disjoint p.support q.support
r : R
hl : ∀ (n : σ →₀ ℕ) (hne : coeff n p ≠ 0), coeff n q = 0
hr : ∀ (n : σ →₀ ℕ) (hne : coeff n q ≠ 0), coeff n p = 0
hor : ∀ (n : σ →₀ ℕ) (h : ¬coeff n p + coeff n q = 0), coeff n p ≠ 0 ∨ coeff n q ≠ 0
h₁ :
  (∃ (n : σ →₀ ℕ), ¬coeff n p + coeff n q = 0 ∧ r = coeff n p + coeff n q) →
    ∀ (n : σ →₀ ℕ) (hn1 : ¬coeff n p + coeff n q = 0) (hn2 : r = coeff n p + coeff n q),
      (∃ (n : σ →₀ ℕ), ¬coeff n p = 0 ∧ r = coeff n p) ∨ ∃ (n : σ →₀ ℕ), ¬coeff n q = 0 ∧ r = coeff n q
h₂ :
  ((∃ (n : σ →₀ ℕ), ¬coeff n p = 0 ∧ r = coeff n p) ∨ ∃ (n : σ →₀ ℕ), ¬coeff n q = 0 ∧ r = coeff n q) →
    ∃ (n : σ →₀ ℕ), ¬coeff n p + coeff n q = 0 ∧ r = coeff n p + coeff n q
⊢ (∃ (n : σ →₀ ℕ), ¬coeff n p + coeff n q = 0 ∧ r = coeff n p + coeff n q) ↔
    (∃ (n : σ →₀ ℕ), ¬coeff n p = 0 ∧ r = coeff n p) ∨ ∃ (n : σ →₀ ℕ), ¬coeff n q = 0 ∧ r = coeff n q

Tactic:
refine ⟨fun ⟨n, hn1, hn2⟩ ↦ ?_, ?_⟩
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq R
p q : MvPolynomial σ R
h : Disjoint p.support q.support
r : R
hl : ∀ (n : σ →₀ ℕ) (hne : coeff n p ≠ 0), coeff n q = 0
hr : ∀ (n : σ →₀ ℕ) (hne : coeff n q ≠ 0), coeff n p = 0
hor : ∀ (n : σ →₀ ℕ) (h : ¬coeff n p + coeff n q = 0), coeff n p ≠ 0 ∨ coeff n q ≠ 0
h_1 : ∃ (n : σ →₀ ℕ), ¬coeff n p + coeff n q = 0 ∧ r = coeff n p + coeff n q
n : σ →₀ ℕ
hn1 : ¬coeff n p + coeff n q = 0
hn2 : r = coeff n p + coeff n q
h₁ :
  ∀ (h : coeff n p ≠ 0),
    (∃ (n : σ →₀ ℕ), ¬coeff n p = 0 ∧ r = coeff n p) ∨ ∃ (n : σ →₀ ℕ), ¬coeff n q = 0 ∧ r = coeff n q
h₂ :
  ∀ (h : coeff n q ≠ 0),
    (∃ (n : σ →₀ ℕ), ¬coeff n p = 0 ∧ r = coeff n p) ∨ ∃ (n : σ →₀ ℕ), ¬coeff n q = 0 ∧ r = coeff n q
⊢ (∃ (n : σ →₀ ℕ), ¬coeff n p = 0 ∧ r = coeff n p) ∨ ∃ (n : σ →₀ ℕ), ¬coeff n q = 0 ∧ r = coeff n q

Tactic:
obtain (h | h) := hor n hn1
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq R
p q : MvPolynomial σ R
h_1 : Disjoint p.support q.support
r : R
hl : ∀ (n : σ →₀ ℕ) (hne : coeff n p ≠ 0), coeff n q = 0
hr : ∀ (n : σ →₀ ℕ) (hne : coeff n q ≠ 0), coeff n p = 0
hor : ∀ (n : σ →₀ ℕ) (h : ¬coeff n p + coeff n q = 0), coeff n p ≠ 0 ∨ coeff n q ≠ 0
h_2 : ∃ (n : σ →₀ ℕ), ¬coeff n p + coeff n q = 0 ∧ r = coeff n p + coeff n q
n : σ →₀ ℕ
hn1 : ¬coeff n p + coeff n q = 0
hn2 : r = coeff n p + coeff n q
h : coeff n p ≠ 0
⊢ ¬coeff n p = 0 ∧ r = coeff n p

Tactic:
simp [h, hn2, hl n h]
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq R
p q : MvPolynomial σ R
h_1 : Disjoint p.support q.support
r : R
hl : ∀ (n : σ →₀ ℕ) (hne : coeff n p ≠ 0), coeff n q = 0
hr : ∀ (n : σ →₀ ℕ) (hne : coeff n q ≠ 0), coeff n p = 0
hor : ∀ (n : σ →₀ ℕ) (h : ¬coeff n p + coeff n q = 0), coeff n p ≠ 0 ∨ coeff n q ≠ 0
h_2 : ∃ (n : σ →₀ ℕ), ¬coeff n p + coeff n q = 0 ∧ r = coeff n p + coeff n q
n : σ →₀ ℕ
hn1 : ¬coeff n p + coeff n q = 0
hn2 : r = coeff n p + coeff n q
h : coeff n p ≠ 0
⊢ (∃ (n : σ →₀ ℕ), ¬coeff n p = 0 ∧ r = coeff n p) ∨ ∃ (n : σ →₀ ℕ), ¬coeff n q = 0 ∧ r = coeff n q

Tactic:
exact Or.inl ⟨n, by simp [h, hn2, hl n h]⟩

Premises used: Or.inl
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq R
p q : MvPolynomial σ R
h_1 : Disjoint p.support q.support
r : R
hl : ∀ (n : σ →₀ ℕ) (hne : coeff n p ≠ 0), coeff n q = 0
hr : ∀ (n : σ →₀ ℕ) (hne : coeff n q ≠ 0), coeff n p = 0
hor : ∀ (n : σ →₀ ℕ) (h : ¬coeff n p + coeff n q = 0), coeff n p ≠ 0 ∨ coeff n q ≠ 0
h_2 : ∃ (n : σ →₀ ℕ), ¬coeff n p + coeff n q = 0 ∧ r = coeff n p + coeff n q
n : σ →₀ ℕ
hn1 : ¬coeff n p + coeff n q = 0
hn2 : r = coeff n p + coeff n q
h : coeff n q ≠ 0
⊢ ¬coeff n q = 0 ∧ r = coeff n q

Tactic:
simp [h, hn2, hr n h]
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq R
p q : MvPolynomial σ R
h_1 : Disjoint p.support q.support
r : R
hl : ∀ (n : σ →₀ ℕ) (hne : coeff n p ≠ 0), coeff n q = 0
hr : ∀ (n : σ →₀ ℕ) (hne : coeff n q ≠ 0), coeff n p = 0
hor : ∀ (n : σ →₀ ℕ) (h : ¬coeff n p + coeff n q = 0), coeff n p ≠ 0 ∨ coeff n q ≠ 0
h_2 : ∃ (n : σ →₀ ℕ), ¬coeff n p + coeff n q = 0 ∧ r = coeff n p + coeff n q
n : σ →₀ ℕ
hn1 : ¬coeff n p + coeff n q = 0
hn2 : r = coeff n p + coeff n q
h : coeff n q ≠ 0
⊢ (∃ (n : σ →₀ ℕ), ¬coeff n p = 0 ∧ r = coeff n p) ∨ ∃ (n : σ →₀ ℕ), ¬coeff n q = 0 ∧ r = coeff n q

Tactic:
exact Or.inr ⟨n, by simp [h, hn2, hr n h]⟩

Premises used: Or.inr
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq R
p q : MvPolynomial σ R
h : Disjoint p.support q.support
hl : ∀ (n : σ →₀ ℕ) (hne : coeff n p ≠ 0), coeff n q = 0
hr : ∀ (n : σ →₀ ℕ) (hne : coeff n q ≠ 0), coeff n p = 0
hor : ∀ (n : σ →₀ ℕ) (h : ¬coeff n p + coeff n q = 0), coeff n p ≠ 0 ∨ coeff n q ≠ 0
n : σ →₀ ℕ
hn : ¬coeff n p = 0
⊢ ¬coeff n p + coeff n q = 0 ∧ coeff n p = coeff n p + coeff n q

Tactic:
simp [hl n hn, hn]
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq R
p q : MvPolynomial σ R
h : Disjoint p.support q.support
hl : ∀ (n : σ →₀ ℕ) (hne : coeff n p ≠ 0), coeff n q = 0
hr : ∀ (n : σ →₀ ℕ) (hne : coeff n q ≠ 0), coeff n p = 0
hor : ∀ (n : σ →₀ ℕ) (h : ¬coeff n p + coeff n q = 0), coeff n p ≠ 0 ∨ coeff n q ≠ 0
n : σ →₀ ℕ
hn : ¬coeff n p = 0
⊢ ∃ (n_1 : σ →₀ ℕ), ¬coeff n_1 p + coeff n_1 q = 0 ∧ coeff n p = coeff n_1 p + coeff n_1 q

Tactic:
exact ⟨n, by simp [hl n hn, hn]⟩
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq R
p q : MvPolynomial σ R
h : Disjoint p.support q.support
hl : ∀ (n : σ →₀ ℕ) (hne : coeff n p ≠ 0), coeff n q = 0
hr : ∀ (n : σ →₀ ℕ) (hne : coeff n q ≠ 0), coeff n p = 0
hor : ∀ (n : σ →₀ ℕ) (h : ¬coeff n p + coeff n q = 0), coeff n p ≠ 0 ∨ coeff n q ≠ 0
n : σ →₀ ℕ
hn : ¬coeff n q = 0
⊢ ¬coeff n p + coeff n q = 0 ∧ coeff n q = coeff n p + coeff n q

Tactic:
simp [hr n hn, hn]
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq R
p q : MvPolynomial σ R
h : Disjoint p.support q.support
hl : ∀ (n : σ →₀ ℕ) (hne : coeff n p ≠ 0), coeff n q = 0
hr : ∀ (n : σ →₀ ℕ) (hne : coeff n q ≠ 0), coeff n p = 0
hor : ∀ (n : σ →₀ ℕ) (h : ¬coeff n p + coeff n q = 0), coeff n p ≠ 0 ∨ coeff n q ≠ 0
n : σ →₀ ℕ
hn : ¬coeff n q = 0
⊢ ∃ (n_1 : σ →₀ ℕ), ¬coeff n_1 p + coeff n_1 q = 0 ∧ coeff n q = coeff n_1 p + coeff n_1 q

Tactic:
exact ⟨n, by simp [hr n hn, hn]⟩
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst : CommSemiring R
inst_1 : CommSemiring S₁
p q : MvPolynomial σ R
⊢ Eq.{u + 1} (α := R) (coeff.{u, u_1} (σ := σ) 0 1) 1

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst : CommSemiring R
inst_1 : CommSemiring S₁
p q : MvPolynomial σ R
⊢ ∀ (x y : MvPolynomial σ R), coeff 0 (x * y) = coeff 0 x * coeff 0 y

Tactic:
simp [coeff_mul]

Premises used: MvPolynomial.coeff_mul
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst : CommSemiring R
inst_1 : CommSemiring S₁
p q : MvPolynomial σ R
⊢ ∀ (x y : MvPolynomial σ R), coeff 0 (x * y) = coeff 0 x * coeff 0 y

Tactic:
classical simp [coeff_mul]

Premises used: MvPolynomial.coeff_mul
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
⊢ Eq (α := (a : MvPolynomial σ R) → R) (⇑constantCoeff : (a : MvPolynomial σ R) → R) (coeff 0)

Tactic:
rfl

Premises used: MvPolynomial.coeff, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
r : R
⊢ (constantCoeff : (a : MvPolynomial σ R) → R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) = r

Tactic:
simp [constantCoeff_eq]

Premises used: MvPolynomial.constantCoeff_eq
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
r : R
⊢ (constantCoeff : (a : MvPolynomial σ R) → R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) = r

Tactic:
classical simp [constantCoeff_eq]

Premises used: MvPolynomial.constantCoeff_eq
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
i : σ
⊢ Eq.{u + 1} (α := R) ((constantCoeff : (a : MvPolynomial σ R) → R) (X i) : R) (0 : R)

Tactic:
simp [constantCoeff_eq]

Premises used: MvPolynomial.constantCoeff_eq
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
S₁ : Type v
σ : Type u_1
inst : CommSemiring S₁
R : Type u_2
inst_1 : SMulZeroClass R S₁
a : R
f : MvPolynomial σ S₁
⊢ (constantCoeff : (a : MvPolynomial σ S₁) → S₁) (a • f) =
    HSMul.hSMul (β := S₁) a ((constantCoeff : (a : MvPolynomial σ S₁) → S₁) f : S₁)

Tactic:
rfl

Premises used: MvPolynomial.coeff, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
d : σ →₀ ℕ
r : R
rw : coeff.{u, u_1} (σ := σ) 0 ((monomial d : (a : R) → MvPolynomial σ R) r) = if d = 0 then r else 0
rw₁ rw₂ : (if d = 0 then r else 0) = if d = 0 then r else 0
⊢ (constantCoeff : (a : MvPolynomial σ R) → R) ((monomial d : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) =
    if d = 0 then r else 0

Tactic:
rw [constantCoeff_eq, coeff_monomial]

Premises used: MvPolynomial.constantCoeff_eq, MvPolynomial.coeff_monomial
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
a :
  ∀ (x : R),
    Eq (α := R) ((RingHom.comp (β := MvPolynomial σ R) constantCoeff C : (a : R) → R) x : R)
      ((RingHom.id R : (a : R) → R) x : R)
⊢ Eq (α := R →+* R) (RingHom.comp (β := MvPolynomial σ R) constantCoeff C) (RingHom.id R)

Tactic:
ext x
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
x : R
⊢ Eq (α := R) ((RingHom.comp (β := MvPolynomial σ R) constantCoeff C : (a : R) → R) x : R)
    ((RingHom.id R : (a : R) → R) x : R)

Tactic:
constantCoeff_C σ x

Premises used: Function.update, MvPolynomial.constantCoeff_C, Pi.single, dite, MvPolynomial.coeff
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
x : R
⊢ Eq (α := R) ((RingHom.comp (β := MvPolynomial σ R) constantCoeff C : (a : R) → R) x : R)
    ((RingHom.id R : (a : R) → R) x : R)

Tactic:
exact constantCoeff_C σ x

Premises used: MvPolynomial.constantCoeff_C
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
⊢ Eq (α := R →+* R) (RingHom.comp (β := MvPolynomial σ R) constantCoeff (algebraMap R (MvPolynomial σ R)))
    (RingHom.id R)

Tactic:
constantCoeff_comp_C _ _

Premises used: MvPolynomial.constantCoeff_comp_C, MvPolynomial.C
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
⊢ ∑ v ∈ p.support, (monomial v : (a : R) → MvPolynomial σ R) (coeff v p) = p

Tactic:
Finsupp.sum_single p

Premises used: Finsupp.sum, MvPolynomial.support, MvPolynomial.coeff, AddMonoidAlgebra, Finsupp.sum_single, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
⊢ p = ∑ v ∈ p.support, (monomial v : (a : R) → MvPolynomial σ R) (coeff v p)

Tactic:
(support_sum_monomial_coeff p).symm

Premises used: MvPolynomial.support_sum_monomial_coeff, Eq.symm
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R_1 : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ_1 : Type u_1
a a' a₁ a₂ : R_1
e : ℕ
n_1 m : σ_1
s_1 : σ_1 →₀ ℕ
inst : CommSemiring R_1
inst_1 : CommSemiring S₁
p_1 q : MvPolynomial σ_1 R_1
R : Type u_2
S : Type u_3
σ : Type u_4
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Module R S
M N : Submodule R S
p : MvPolynomial σ S
s : σ
i : σ →₀ ℕ
x : S
n : ℕ
⊢ ∀ {a b : MvPolynomial σ S},
    Membership.mem (γ := Set (MvPolynomial σ S)) {p : MvPolynomial σ S | ∀ (i : σ →₀ ℕ), coeff i p ∈ M} a →
      Membership.mem (γ := Set (MvPolynomial σ S)) {p : MvPolynomial σ S | ∀ (i : σ →₀ ℕ), coeff i p ∈ M} b →
        Membership.mem (γ := Set (MvPolynomial σ S)) {p : MvPolynomial σ S | ∀ (i : σ →₀ ℕ), coeff i p ∈ M} (a + b)

Tactic:
simp +contextual [add_mem]

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R_1 : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ_1 : Type u_1
a a' a₁ a₂ : R_1
e : ℕ
n_1 m : σ_1
s_1 : σ_1 →₀ ℕ
inst : CommSemiring R_1
inst_1 : CommSemiring S₁
p_1 q : MvPolynomial σ_1 R_1
R : Type u_2
S : Type u_3
σ : Type u_4
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Module R S
M N : Submodule R S
p : MvPolynomial σ S
s : σ
i : σ →₀ ℕ
x : S
n : ℕ
⊢ Membership.mem (γ := Set (MvPolynomial σ S)) {p : MvPolynomial σ S | ∀ (i : σ →₀ ℕ), coeff i p ∈ M} 0

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R_1 : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ_1 : Type u_1
a a' a₁ a₂ : R_1
e : ℕ
n_1 m : σ_1
s_1 : σ_1 →₀ ℕ
inst : CommSemiring R_1
inst_1 : CommSemiring S₁
p_1 q : MvPolynomial σ_1 R_1
R : Type u_2
S : Type u_3
σ : Type u_4
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Module R S
M N : Submodule R S
p : MvPolynomial σ S
s : σ
i : σ →₀ ℕ
x : S
n : ℕ
⊢ ∀ (c : R) {x : MvPolynomial σ S},
    Membership.mem (γ := Set (MvPolynomial σ S)) {p : MvPolynomial σ S | ∀ (i : σ →₀ ℕ), coeff i p ∈ M} x →
      Membership.mem (γ := Set (MvPolynomial σ S)) {p : MvPolynomial σ S | ∀ (i : σ →₀ ℕ), coeff i p ∈ M} (c • x)

Tactic:
simp +contextual [Submodule.smul_mem]

Premises used: Submodule.smul_mem
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
p : MvPolynomial σ S
⊢ p ∈ coeffsIn σ M ↔ ∀ (i : σ →₀ ℕ), coeff i p ∈ M

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
i : σ →₀ ℕ
x : S
simp : (∀ (i_1 : σ →₀ ℕ), (if i = i_1 then x else 0) ∈ M) ↔ x ∈ M
⊢ Membership.mem (α := MvPolynomial σ S) (coeffsIn σ M)
      ((monomial i : (a : S) → MvPolynomial σ S) x : MvPolynomial σ S) ↔
    x ∈ M

Tactic:
simp only [mem_coeffsIn, coeff_monomial]

Premises used: MvPolynomial.mem_coeffsIn, MvPolynomial.coeff_monomial
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
i : σ →₀ ℕ
x : S
h : ∀ (i_1 : σ →₀ ℕ), (if i = i_1 then x else 0) ∈ M
⊢ x ∈ M

Tactic:
simpa using h i
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
i : σ →₀ ℕ
x : S
hs : x ∈ M
j : σ →₀ ℕ
isTrue : i = j → x ∈ M
isFalse : ¬i = j → 0 ∈ M
⊢ (if i = j then x else 0) ∈ M

Tactic:
split
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
i : σ →₀ ℕ
x : S
hs : x ∈ M
j : σ →₀ ℕ
h : i = j
⊢ x ∈ M

Tactic:
simp [hs]
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
i : σ →₀ ℕ
x : S
hs : x ∈ M
j : σ →₀ ℕ
h : ¬i = j
⊢ 0 ∈ M

Tactic:
simp [hs]
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
i : σ →₀ ℕ
x : S
⊢ (∀ (i_1 : σ →₀ ℕ), (if i = i_1 then x else 0) ∈ M) ↔ x ∈ M

Tactic:
exact ⟨fun h ↦ by simpa using h i, fun hs j ↦ by split <;> simp [hs]⟩
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
i : σ →₀ ℕ
x : S
simp : (∀ (i_1 : σ →₀ ℕ), (if i = i_1 then x else 0) ∈ M) ↔ x ∈ M
⊢ Membership.mem (α := MvPolynomial σ S) (coeffsIn σ M)
      ((monomial i : (a : S) → MvPolynomial σ S) x : MvPolynomial σ S) ↔
    x ∈ M

Tactic:
classical
  simp only [mem_coeffsIn, coeff_monomial]
  exact ⟨fun h ↦ by simpa using h i, fun hs j ↦ by split <;> simp [hs]⟩

Premises used: MvPolynomial.mem_coeffsIn, MvPolynomial.coeff_monomial