awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : IsEmpty σ
p : MvPolynomial σ R
obtain :
  ∀ (x : R),
    Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) x : MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) (coeff.{u, u_1} (σ := σ) 0 ((C : (a : R) → MvPolynomial σ R) x)) :
        MvPolynomial σ R)
⊢ p = (C : (a : R) → MvPolynomial σ R) (coeff 0 p)

Tactic:
obtain ⟨x, rfl⟩ := C_surjective σ p

Premises used: MvPolynomial.C_surjective, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : IsEmpty σ
x : R
⊢ Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) x : MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) (coeff.{u, u_1} (σ := σ) 0 ((C : (a : R) → MvPolynomial σ R) x)) :
      MvPolynomial σ R)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
m : σ →₀ ℕ
⊢ Eq.{u + 1} (α := R) (coeff m 1) (if 0 = m then 1 else 0)

Tactic:
coeff_C m 1

Premises used: MvPolynomial.coeff_C, OfNat.ofNat, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
a : R
⊢ coeff.{u, u_1} (σ := σ) 0 ((C : (a : R) → MvPolynomial σ R) a) = a

Tactic:
single_eq_same

Premises used: Finsupp.single_eq_same, MvPolynomial.coeff
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
⊢ Eq.{u + 1} (α := R) (coeff.{u, u_1} (σ := σ) 0 1) 1

Tactic:
coeff_zero_C 1

Premises used: MvPolynomial.coeff_zero_C, OfNat.ofNat, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
i : σ
m : σ →₀ ℕ
k : ℕ
⊢ Eq.{u + 1} (α := R) (coeff m ((monomial (Finsupp.single i k) : (a : R) → MvPolynomial σ R) 1))
    (if Finsupp.single i k = m then 1 else 0)

Tactic:
have := coeff_monomial m (Finsupp.single i k) (1 : R)
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
i : σ
m : σ →₀ ℕ
k : ℕ
this :
  Eq.{u + 1} (α := R) (coeff m ((monomial (Finsupp.single i k) : (a : R) → MvPolynomial σ R) 1))
    (if Finsupp.single i k = m then 1 else 0)
rwa :
  ∀
    (this :
      Eq.{u + 1} (α := R)
        (coeff m (Finsupp.prod (Finsupp.single i k) fun (n : σ) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial σ R) (X n) e))
        (if Finsupp.single i k = m then 1 else 0)),
    HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X i) 0 = 1
⊢ coeff m (HPow.hPow (α := MvPolynomial σ R) (X i) k) = if Finsupp.single i k = m then 1 else 0

Tactic:
rwa [@monomial_eq _ _ (1 : R) (Finsupp.single i k) _, C_1, one_mul, Finsupp.prod_single_index]
    at this

Premises used: MvPolynomial.C_1, MvPolynomial.monomial_eq, Finsupp.prod_single_index, one_mul
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
i : σ
m : σ →₀ ℕ
k : ℕ
this :
  Eq.{u + 1} (α := R)
    (coeff m (Finsupp.prod (Finsupp.single i k) fun (n : σ) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial σ R) (X n) e))
    (if Finsupp.single i k = m then 1 else 0)
⊢ HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X i) 0 = 1

Tactic:
pow_zero _

Premises used: pow_zero
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
i : σ
m : σ →₀ ℕ
k : ℕ
this :
  Eq.{u + 1} (α := R)
    (coeff m (Finsupp.prod (Finsupp.single i k) fun (n : σ) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial σ R) (X n) e))
    (if Finsupp.single i k = m then 1 else 0)
⊢ HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X i) 0 = 1

Tactic:
exact pow_zero _

Premises used: pow_zero
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
i : σ
m : σ →₀ ℕ
rw : coeff m (X i) = coeff m (HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X i) 1)
rw₁ rw₂ : Eq.{u + 1} (α := R) (coeff m (X i)) (coeff m (X i))
⊢ Eq.{u + 1} (α := R) (coeff m (X i)) (if Finsupp.single i 1 = m then 1 else 0)

Tactic:
rw [← coeff_X_pow, pow_one]

Premises used: MvPolynomial.coeff_X_pow, pow_one
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
i : σ
rw : Eq.{u + 1} (α := R) (if Eq (α := σ →₀ ℕ) (Finsupp.single i 1) (Finsupp.single i 1) then 1 else 0) 1
rw₁ rw₂ : Eq.{u + 1} (α := R) 1 1
⊢ Eq.{u + 1} (α := R) (coeff (Finsupp.single i 1) (X i)) 1

Tactic:
rw [coeff_X', if_pos rfl]

Premises used: if_pos, MvPolynomial.coeff_X', rfl
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
i : σ
classical : Eq.{u + 1} (α := R) (if Eq (α := σ →₀ ℕ) (Finsupp.single i 1) (Finsupp.single i 1) then 1 else 0) 1
classical₁ classical₂ : Eq.{u + 1} (α := R) 1 1
⊢ Eq.{u + 1} (α := R) (coeff (Finsupp.single i 1) (X i)) 1

Tactic:
classical rw [coeff_X', if_pos rfl]

Premises used: if_pos, MvPolynomial.coeff_X', rfl
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m : σ →₀ ℕ
a : R
p : MvPolynomial σ R
rw : coeff m (sum p fun (n : σ →₀ ℕ) (b : R) ↦ (monomial (0 + n) : (a : R) → MvPolynomial σ R) (a * b)) = a * coeff m p
rw₁ :
  Eq (α := MvPolynomial σ R) (sum p fun (n : σ →₀ ℕ) (b : R) ↦ (monomial (0 + n) : (a : R) → MvPolynomial σ R) (0 * b))
    0
⊢ coeff m (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) p) = a * coeff m p

Tactic:
rw [mul_def, sum_C]

Premises used: MvPolynomial.mul_def, MvPolynomial.sum_C
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m : σ →₀ ℕ
a : R
p : MvPolynomial σ R
⊢ coeff m (sum p fun (n : σ →₀ ℕ) (b : R) ↦ (monomial (0 + n) : (a : R) → MvPolynomial σ R) (a * b)) = a * coeff m p

Tactic:
simp +contextual [sum_def, coeff_sum]

Premises used: MvPolynomial.sum_def, MvPolynomial.coeff_sum
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m : σ →₀ ℕ
a : R
p : MvPolynomial σ R
⊢ Eq (α := MvPolynomial σ R) (sum p fun (n : σ →₀ ℕ) (b : R) ↦ (monomial (0 + n) : (a : R) → MvPolynomial σ R) (0 * b))
    0

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m : σ →₀ ℕ
a : R
p : MvPolynomial σ R
rw :
  coeff m
      (sum ((C : (a : R) → MvPolynomial σ R) a) fun (m : σ →₀ ℕ) (a : R) ↦
        sum p fun (n : σ →₀ ℕ) (b : R) ↦ (monomial (m + n) : (a : R) → MvPolynomial σ R) (a * b)) =
    a * coeff m p
rw₁ : coeff m (sum p fun (n : σ →₀ ℕ) (b : R) ↦ (monomial (0 + n) : (a : R) → MvPolynomial σ R) (a * b)) = a * coeff m p
rw₂ :
  Eq (α := MvPolynomial σ R) (sum p fun (n : σ →₀ ℕ) (b : R) ↦ (monomial (0 + n) : (a : R) → MvPolynomial σ R) (0 * b))
    0
rw₃ : coeff m (sum p fun (n : σ →₀ ℕ) (b : R) ↦ (monomial (0 + n) : (a : R) → MvPolynomial σ R) (a * b)) = a * coeff m p
rw₄ :
  Eq (α := MvPolynomial σ R) (sum p fun (n : σ →₀ ℕ) (b : R) ↦ (monomial (0 + n) : (a : R) → MvPolynomial σ R) (0 * b))
    0
rw₅ : coeff m (sum p fun (n : σ →₀ ℕ) (b : R) ↦ (monomial (0 + n) : (a : R) → MvPolynomial σ R) (a * b)) = a * coeff m p
rw₆ rw₇ :
  Eq (α := MvPolynomial σ R) (sum p fun (n : σ →₀ ℕ) (b : R) ↦ (monomial (0 + n) : (a : R) → MvPolynomial σ R) (0 * b))
    0
⊢ coeff m (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) p) = a * coeff m p

Tactic:
classical
  rw [mul_def, sum_C]
  · simp +contextual [sum_def, coeff_sum]
  simp

Premises used: MvPolynomial.sum_def, MvPolynomial.mul_def, MvPolynomial.sum_C, MvPolynomial.coeff_sum
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
p q : MvPolynomial σ R
n : σ →₀ ℕ
⊢ coeff n (p * q) = ∑ x ∈ @Finset.antidiagonal _ instAddMonoid _ n, coeff x.1 p * coeff x.2 q

Tactic:
AddMonoidAlgebra.mul_apply_antidiagonal p q _ _ Finset.mem_antidiagonal

Premises used: MvPolynomial.coeff, Finset.HasAntidiagonal.mem_antidiagonal, AddMonoidAlgebra.mul_apply_antidiagonal
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
⊢ coeff (m + s) (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)) =
    coeff m p * r

Tactic:
AddMonoidAlgebra.mul_single_apply_aux fun _a _ => add_left_inj _

Premises used: add_left_inj, MvPolynomial.coeff, AddMonoidAlgebra.mul_single_apply_aux, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
⊢ coeff (s + m) (HMul.hMul (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) p) =
    r * coeff m p

Tactic:
AddMonoidAlgebra.single_mul_apply_aux fun _a _ => add_right_inj _

Premises used: MvPolynomial.coeff, AddMonoidAlgebra.single_mul_apply_aux, add_right_inj, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
⊢ coeff (m + Finsupp.single s 1) (p * X s) = coeff m p

Tactic:
(coeff_mul_monomial _ _ _ _).trans (mul_one _)

Premises used: MvPolynomial.X, MvPolynomial.coeff_mul_monomial, mul_one, Eq.trans
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
⊢ coeff (Finsupp.single s 1 + m) (X s * p) = coeff m p

Tactic:
(coeff_monomial_mul _ _ _ _).trans (one_mul _)

Premises used: MvPolynomial.X, MvPolynomial.coeff_monomial_mul, one_mul, Eq.trans
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
s s' : σ
n n' : ℕ
⊢ coeff (Finsupp.single s' n') (HPow.hPow (α := MvPolynomial σ R) (X s) n) =
    if s = s' ∧ n = n' ∨ n = 0 ∧ n' = 0 then 1 else 0

Tactic:
simp only [coeff_X_pow, single_eq_single_iff]

Premises used: Finsupp.single_eq_single_iff, MvPolynomial.coeff_X_pow
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
s s' : σ
n : ℕ
⊢ Eq.{u + 1} (α := R) (coeff (Finsupp.single s' n) (X s)) (if n = 1 ∧ s = s' then 1 else 0)

Tactic:
simpa [eq_comm, and_comm] using coeff_single_X_pow s s' 1 n

Premises used: MvPolynomial.coeff_single_X_pow, and_comm, eq_comm, OfNat.ofNat
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
d : σ →₀ ℕ
x : σ → ℕ
s : Finset σ
simp_rw :
  Eq.{u + 1} (α := R)
    (coeff d ((monomial (Finsupp.indicator s fun (i : σ) (x_1 : i ∈ s) ↦ x i) : (a : R) → MvPolynomial σ R) 1))
    (if d = Finsupp.indicator s fun (i : σ) (x_1 : i ∈ s) ↦ x i then 1 else 0)
simp_rw₁ :
  Eq.{u + 1} (α := R) (if (Finsupp.indicator s fun (i : σ) (x_1 : i ∈ s) ↦ x i) = d then 1 else 0)
    (if d = Finsupp.indicator s fun (i : σ) (x_1 : i ∈ s) ↦ x i then 1 else 0)
⊢ Eq.{u + 1} (α := R) (coeff d (∏ y ∈ s, HPow.hPow (α := MvPolynomial σ R) (X y) (x y)))
    (if d = Finsupp.indicator s fun (i : σ) (x_1 : i ∈ s) ↦ x i then 1 else 0)

Tactic:
simp_rw [prod_X_pow x s, coeff_monomial, eq_comm]

Premises used: eq_comm, MvPolynomial.coeff_monomial, MvPolynomial.prod_X_pow
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ
p : MvPolynomial σ R
⊢ ∀ (y : R), y * 1 = 0 ↔ y = 0

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ
p : MvPolynomial σ R
⊢ ∀ (y : R), 1 * y = 0 ↔ y = 0

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Semiring S
inst_2 : IsDomain S
inst_3 : Module S R
inst_4 : Module.IsTorsionFree S R
a : S
h : a ≠ 0
p : MvPolynomial σ R
⊢ (a • p).support = p.support

Tactic:
Finsupp.support_smul_eq h

Premises used: MvPolynomial.support, Finsupp.support_smul_eq
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
p q : MvPolynomial σ R
m : σ →₀ ℕ
hm : m ∈ p.support \ q.support
⊢ ¬coeff m p = 0 ∧ coeff m q = 0

Tactic:
simp only [Classical.not_not, mem_support_iff, Finset.mem_sdiff, Ne] at hm

Premises used: MvPolynomial.mem_support_iff, Classical.not_not, Ne, Finset.mem_sdiff
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
p q : MvPolynomial σ R
m : σ →₀ ℕ
hm : ¬coeff m p = 0 ∧ coeff m q = 0
⊢ m ∈ (p + q).support

Tactic:
simp [hm.2, hm.1]

Premises used: And.right, And.left
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
p q : MvPolynomial σ R
hs : p.support \ q.support ⊆ (p + q).support
a : q.support \ p.support ⊆ (p + q).support
⊢ p.support \ q.support ∪ q.support \ p.support ⊆ (p + q).support

Tactic:
apply Finset.union_subset

Premises used: Finset.union_subset
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
p q : MvPolynomial σ R
⊢ p.support \ q.support ⊆ (p + q).support

Tactic:
support_sdiff_support_subset_support_add p q

Premises used: MvPolynomial.support_sdiff_support_subset_support_add
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
p q : MvPolynomial σ R
⊢ p.support \ q.support ⊆ (p + q).support

Tactic:
exact support_sdiff_support_subset_support_add p q

Premises used: MvPolynomial.support_sdiff_support_subset_support_add
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
p q : MvPolynomial σ R
a : q.support \ p.support ⊆ (q + p).support
⊢ q.support \ p.support ⊆ (p + q).support

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
p q : MvPolynomial σ R
⊢ q.support \ p.support ⊆ (q + p).support

Tactic:
support_sdiff_support_subset_support_add q p

Premises used: MvPolynomial.support_sdiff_support_subset_support_add, Set.Mem, setOf
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
p q : MvPolynomial σ R
⊢ q.support \ p.support ⊆ (q + p).support

Tactic:
exact support_sdiff_support_subset_support_add q p

Premises used: MvPolynomial.support_sdiff_support_subset_support_add
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
pos :
  ∀ (h : s ≤ m),
    coeff m (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)) =
      coeff (m - s) p * r
neg :
  ∀ (h : ¬s ≤ m),
    coeff m (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)) = 0
⊢ coeff m (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)) =
    if s ≤ m then coeff (m - s) p * r else 0

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
h : s ≤ m
rw :
  coeff (m - s + s)
    (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R))
| coeff (m - s) p * r

Tactic:
rw [← coeff_mul_monomial _ s]

Premises used: MvPolynomial.coeff_mul_monomial
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
h : s ≤ m
pos :
  coeff m (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)) =
    coeff (m - s + s)
      (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R))
⊢ coeff m (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)) =
    coeff (m - s) p * r

Tactic:
conv_rhs => rw [← coeff_mul_monomial _ s]

Premises used: MvPolynomial.coeff_mul_monomial
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
h : s ≤ m
pos pos₁ :
  coeff m (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)) =
    coeff m (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R))
⊢ coeff m (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)) =
    coeff (m - s + s)
      (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R))

Tactic:
rw [tsub_add_cancel_of_le h]

Premises used: tsub_add_cancel_of_le
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
h : ¬s ≤ m
neg :
  ∀
    (h :
      coeff m (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)) ≠
        0),
    s ≤ m
⊢ coeff m (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)) = 0

Tactic:
contrapose! h
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
h : coeff m (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)) ≠ 0
⊢ m ∈ (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)).support

Tactic:
rw [← mem_support_iff] at h

Premises used: MvPolynomial.mem_support_iff
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
h : m ∈ (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)).support
⊢ ∃ j ∈ p.support, j + s = m

Tactic:
simpa [Finset.mem_add]
        using Finset.add_subset_add_left support_monomial_subset <| support_mul _ _ h

Premises used: MvPolynomial.support_mul, MvPolynomial.support_monomial_subset, Finset.mem_add, Finset.add_subset_add_left
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
h : m ∈ (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)).support
neg :
  ∀ (j : σ →₀ ℕ)
    (h :
      j + s ∈
        (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)).support),
    s ≤ j + s
⊢ s ≤ m

Tactic:
obtain ⟨j, -, rfl⟩ : ∃ j ∈ support p, j + s = m := by
      simpa [Finset.mem_add]
        using Finset.add_subset_add_left support_monomial_subset <| support_mul _ _ h

Premises used: MvPolynomial.support, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
j : σ →₀ ℕ
h :
  j + s ∈ (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)).support
⊢ s ≤ j + s

Tactic:
le_add_left le_rfl

Premises used: le_rfl, le_add_left
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
j : σ →₀ ℕ
h :
  j + s ∈ (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)).support
⊢ s ≤ j + s

Tactic:
exact le_add_left le_rfl

Premises used: le_rfl, le_add_left
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
pos :
  ∀ (h : s ≤ m),
    coeff m (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)) =
      coeff (m - s) p * r
neg neg₁ :
  ∀ (h : ¬s ≤ m),
    coeff m (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)) = 0
⊢ coeff m (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)) =
    if s ≤ m then coeff (m - s) p * r else 0

Tactic:
classical
  split_ifs with h
  · conv_rhs => rw [← coeff_mul_monomial _ s]
    rw [tsub_add_cancel_of_le h]
  · contrapose! h
    rw [← mem_support_iff] at h
    obtain ⟨j, -, rfl⟩ : ∃ j ∈ support p, j + s = m := by
      simpa [Finset.mem_add]
        using Finset.add_subset_add_left support_monomial_subset <| support_mul _ _ h
    exact le_add_left le_rfl

Premises used: le_rfl, MvPolynomial.mem_support_iff, MvPolynomial.support, MvPolynomial.coeff_mul_monomial, rfl, le_add_left
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
rw :
  coeff m (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)) =
    if s ≤ m then coeff (m - s) p * r else 0
⊢ coeff m (HMul.hMul (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) p) =
    if s ≤ m then r * coeff (m - s) p else 0

Tactic:
rw [mul_comm, mul_comm r]

Premises used: mul_comm
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
⊢ coeff m (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)) =
    if s ≤ m then coeff (m - s) p * r else 0

Tactic:
coeff_mul_monomial' _ _ _ _

Premises used: MvPolynomial.coeff_mul_monomial'
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
⊢ coeff m (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)) =
    if s ≤ m then coeff (m - s) p * r else 0

Tactic:
exact coeff_mul_monomial' _ _ _ _

Premises used: MvPolynomial.coeff_mul_monomial'
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
⊢ coeff m (p * X s) = if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0

Tactic:
(coeff_mul_monomial' _ _ _ _).trans ?_

Premises used: MvPolynomial.X, MvPolynomial.coeff_mul_monomial', Eq.trans
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
refine :
  (if Finsupp.single s 1 ≤ m then coeff (m - Finsupp.single s 1) p * 1 else 0) =
    if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0
⊢ coeff m (p * X s) = if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0

Tactic:
refine (coeff_mul_monomial' _ _ _ _).trans ?_

Premises used: MvPolynomial.coeff_mul_monomial', Eq.trans
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
simp_rw :
  (if LE.le (α := ℕ) (1 : ℕ) ((m : (a : σ) → ℕ) s : ℕ) then coeff (m - Finsupp.single s 1) p * 1 else 0) =
    if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0
simp_rw₁ :
  (if LE.le (α := ℕ) (1 : ℕ) ((m : (a : σ) → ℕ) s : ℕ) then coeff (m - Finsupp.single s 1) p * 1 else 0) =
    if Ne (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (0 : ℕ) then coeff (m - Finsupp.single s 1) p else 0
simp_rw₂ :
  (if LT.lt (α := ℕ) (0 : ℕ) ((m : (a : σ) → ℕ) s : ℕ) then coeff (m - Finsupp.single s 1) p * 1 else 0) =
    if Ne (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (0 : ℕ) then coeff (m - Finsupp.single s 1) p else 0
simp_rw₃ :
  (if Ne (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (0 : ℕ) then coeff (m - Finsupp.single s 1) p * 1 else 0) =
    if Ne (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (0 : ℕ) then coeff (m - Finsupp.single s 1) p else 0
⊢ (if Finsupp.single s 1 ≤ m then coeff (m - Finsupp.single s 1) p * 1 else 0) =
    if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0

Tactic:
simp_rw [Finsupp.single_le_iff, Finsupp.mem_support_iff, Nat.succ_le_iff, pos_iff_ne_zero,
    mul_one]

Premises used: Finsupp.mem_support_iff, Finsupp.single_le_iff, mul_one, Nat.succ_le_iff, pos_iff_ne_zero