awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
hfd :
  LT.lt.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b + ∑ b ∈ B, g b)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)
h_1 :
  ∀ (hd : ∀ b_1 ∈ B, m.degree (g b_1) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0)
    (hfd :
      LT.lt.{u_4} (α := m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
hd : ∀ a ∈ B, m.degree (g a) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
b' : ι
hb' : b' ∈ B
h : g b' = 0
⊢ coeff (m.degree (g b')) (g b') = coeff (m.degree (g b)) (g b')

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
hfd :
  LT.lt.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b + ∑ b ∈ B, g b)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)
h :
  ∀ (hd : ∀ b_1 ∈ B, m.degree (g b_1) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0)
    (hfd :
      LT.lt.{u_4} (α := m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
hd : ∀ a ∈ B, m.degree (g a) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
rw : m.degree (g b) ∉ (g b + ∑ x ∈ B, g x).support
⊢ coeff (m.degree (g b)) (g b) + ∑ i ∈ B, coeff (m.degree (g b)) (g i) = 0

Tactic:
rw [← coeff_sum, ← coeff_add, ← notMem_support_iff]

Premises used: MvPolynomial.notMem_support_iff, MvPolynomial.coeff_add, MvPolynomial.coeff_sum
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
hfd :
  LT.lt.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b + ∑ b ∈ B, g b)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)
h :
  ∀ (hd : ∀ b_1 ∈ B, m.degree (g b_1) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0)
    (hfd :
      LT.lt.{u_4} (α := m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
hd : ∀ a ∈ B, m.degree (g a) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
⊢ m.degree (g b) ∉ (g b + ∑ x ∈ B, g x).support

Tactic:
m.notMem_support_of_degree_lt hfd

Premises used: MonomialOrder.notMem_support_of_degree_lt
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
hfd :
  LT.lt.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b + ∑ b ∈ B, g b)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)
h :
  ∀ (hd : ∀ b_1 ∈ B, m.degree (g b_1) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0)
    (hfd :
      LT.lt.{u_4} (α := m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
hd : ∀ a ∈ B, m.degree (g a) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
⊢ m.degree (g b) ∉ (g b + ∑ x ∈ B, g x).support

Tactic:
exact m.notMem_support_of_degree_lt hfd

Premises used: MonomialOrder.notMem_support_of_degree_lt
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
hfd :
  LT.lt.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b + ∑ b ∈ B, g b)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)
h :
  ∀ (hd : ∀ b_1 ∈ B, m.degree (g b_1) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0)
    (hfd :
      LT.lt.{u_4} (α := m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
hd : ∀ a ∈ B, m.degree (g a) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
apply :
  ∀ x ∈ B,
    g x - (m.leadingCoeff (g x) * (↑isunit_gb.unit⁻¹ : R)) • g b = (↑isunit_gb.unit⁻¹ : R) • m.sPolynomial (g x) (g b)
⊢ Eq (α := MvPolynomial σ R) (∑ b' ∈ B, (g b' - (m.leadingCoeff (g b') * (↑isunit_gb.unit⁻¹ : R)) • g b))
    (∑ x ∈ B, (↑isunit_gb.unit⁻¹ : R) • m.sPolynomial (g x) (g b))

Tactic:
apply Finset.sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
hfd :
  LT.lt.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b + ∑ b ∈ B, g b)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)
h :
  ∀ (hd : ∀ b_1 ∈ B, m.degree (g b_1) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0)
    (hfd :
      LT.lt.{u_4} (α := m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
hd : ∀ a ∈ B, m.degree (g a) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
b' : ι
hb' : b' ∈ B
inl :
  ∀ (h : m.degree (g b') = m.degree (g b)),
    g b' - (m.leadingCoeff (g b') * (↑isunit_gb.unit⁻¹ : R)) • g b =
      (↑isunit_gb.unit⁻¹ : R) •
        (HMul.hMul (α := MvPolynomial σ R)
            ((monomial (m.degree (g b) - m.degree (g b')) : (a : R) → MvPolynomial σ R) (m.leadingCoeff (g b)) :
              MvPolynomial σ R)
            (g b') -
          HMul.hMul (α := MvPolynomial σ R)
            ((monomial (m.degree (g b') - m.degree (g b)) : (a : R) → MvPolynomial σ R) (m.leadingCoeff (g b')) :
              MvPolynomial σ R)
            (g b))
inr :
  ∀ (h : g b' = 0),
    g b' - (m.leadingCoeff (g b') * (↑isunit_gb.unit⁻¹ : R)) • g b =
      (↑isunit_gb.unit⁻¹ : R) •
        (HMul.hMul (α := MvPolynomial σ R)
            ((monomial (m.degree (g b) - m.degree (g b')) : (a : R) → MvPolynomial σ R) (m.leadingCoeff (g b)) :
              MvPolynomial σ R)
            (g b') -
          HMul.hMul (α := MvPolynomial σ R)
            ((monomial (m.degree (g b') - m.degree (g b)) : (a : R) → MvPolynomial σ R) (m.leadingCoeff (g b')) :
              MvPolynomial σ R)
            (g b))
⊢ g b' - (m.leadingCoeff (g b') * (↑isunit_gb.unit⁻¹ : R)) • g b =
    (↑isunit_gb.unit⁻¹ : R) •
      (HMul.hMul (α := MvPolynomial σ R)
          ((monomial (m.degree (g b) - m.degree (g b')) : (a : R) → MvPolynomial σ R) (m.leadingCoeff (g b)) :
            MvPolynomial σ R)
          (g b') -
        HMul.hMul (α := MvPolynomial σ R)
          ((monomial (m.degree (g b') - m.degree (g b)) : (a : R) → MvPolynomial σ R) (m.leadingCoeff (g b')) :
            MvPolynomial σ R)
          (g b))

Tactic:
obtain (⟨h, -⟩ | h) := hd b' hb'
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
hfd :
  LT.lt.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b + ∑ b ∈ B, g b)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)
h_1 :
  ∀ (hd : ∀ b_1 ∈ B, m.degree (g b_1) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0)
    (hfd :
      LT.lt.{u_4} (α := m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
hd : ∀ a ∈ B, m.degree (g a) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
b' : ι
hb' : b' ∈ B
h : m.degree (g b') = m.degree (g b)
⊢ g b' - (m.leadingCoeff (g b') * (↑isunit_gb.unit⁻¹ : R)) • g b =
    (↑isunit_gb.unit⁻¹ : R) •
      (HMul.hMul (α := MvPolynomial σ R)
          ((monomial (m.degree (g b) - m.degree (g b')) : (a : R) → MvPolynomial σ R) (m.leadingCoeff (g b)) :
            MvPolynomial σ R)
          (g b') -
        HMul.hMul (α := MvPolynomial σ R)
          ((monomial (m.degree (g b') - m.degree (g b)) : (a : R) → MvPolynomial σ R) (m.leadingCoeff (g b')) :
            MvPolynomial σ R)
          (g b))

Tactic:
simp [h, ← smul_eq_C_mul, smul_sub, ← mul_smul, mul_comm (m.leadingCoeff (g b'))]

Premises used: MonomialOrder.leadingCoeff, smul_sub, mul_comm, MvPolynomial.smul_eq_C_mul, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
hfd :
  LT.lt.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b + ∑ b ∈ B, g b)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)
h_1 :
  ∀ (hd : ∀ b_1 ∈ B, m.degree (g b_1) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0)
    (hfd :
      LT.lt.{u_4} (α := m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
hd : ∀ a ∈ B, m.degree (g a) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
b' : ι
hb' : b' ∈ B
h : g b' = 0
⊢ g b' - (m.leadingCoeff (g b') * (↑isunit_gb.unit⁻¹ : R)) • g b =
    (↑isunit_gb.unit⁻¹ : R) •
      (HMul.hMul (α := MvPolynomial σ R)
          ((monomial (m.degree (g b) - m.degree (g b')) : (a : R) → MvPolynomial σ R) (m.leadingCoeff (g b)) :
            MvPolynomial σ R)
          (g b') -
        HMul.hMul (α := MvPolynomial σ R)
          ((monomial (m.degree (g b') - m.degree (g b)) : (a : R) → MvPolynomial σ R) (m.leadingCoeff (g b')) :
            MvPolynomial σ R)
          (g b))

Tactic:
simp [h, ← smul_eq_C_mul, smul_sub, ← mul_smul, mul_comm (m.leadingCoeff (g b'))]

Premises used: MonomialOrder.leadingCoeff, smul_sub, mul_comm, MvPolynomial.smul_eq_C_mul, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : Field R
f : MvPolynomial σ R
⊢ IsUnit (m.leadingCoeff f) ↔ f ≠ 0

Tactic:
simp only [isUnit_iff_ne_zero, ne_eq, leadingCoeff_eq_zero_iff]

Premises used: MonomialOrder.leadingCoeff_eq_zero_iff, isUnit_iff_ne_zero, ne_eq
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : Field R
d : m.syn
ι : Type u_3
B : Finset ι
g : ι → MvPolynomial σ R
hd : ∀ b ∈ B, (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) = d ∨ g b = 0
hfd : (m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) < d
⊢ ∃ (c : ι → ι → R),
    Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))

Tactic:
m.sPolynomial_decomposition ?_ hfd

Premises used: MonomialOrder.sPolynomial_decomposition
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : Field R
d : m.syn
ι : Type u_3
B : Finset ι
g : ι → MvPolynomial σ R
hd : ∀ b ∈ B, (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) = d ∨ g b = 0
hfd : (m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) < d
refine : ∀ b ∈ B, (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) = d ∧ IsUnit (m.leadingCoeff (g b)) ∨ g b = 0
⊢ ∃ (c : ι → ι → R),
    Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))

Tactic:
refine m.sPolynomial_decomposition ?_ hfd

Premises used: MonomialOrder.sPolynomial_decomposition
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : Field R
d : m.syn
ι : Type u_3
B : Finset ι
g : ι → MvPolynomial σ R
hd : ∀ b ∈ B, (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) = d ∨ g b = 0
hfd : (m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) < d
⊢ ∀ b ∈ B, (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) = d ∧ IsUnit (m.leadingCoeff (g b)) ∨ g b = 0

Tactic:
simpa [and_or_right, em']

Premises used: and_or_right, em'
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
R : Type u_2
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_3
m : MonomialOrder.{u_3, u_4} ι
i : ι
r : R
rw :
  LT.lt.{u_4} (α := m.syn)
    ((m.toSyn : (a : ι →₀ ℕ) → m.syn) (degree.{u_3, u_2, u_4} m (R := R) ((C : (a : R) → MvPolynomial ι R) r)) : m.syn)
    ((m.toSyn : (a : ι →₀ ℕ) → m.syn) (degree.{u_3, u_2, u_4} m (R := R) (X i)) : m.syn)
⊢ m.degree
      (HAdd.hAdd (α := MvPolynomial ι R) (β := MvPolynomial ι R) (X i)
        ((C : (a : R) → MvPolynomial ι R) r : MvPolynomial ι R)) =
    single i 1

Tactic:
rw [degree_add_of_lt, degree_X]

Premises used: MonomialOrder.degree_X, MonomialOrder.degree_add_of_lt
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
R : Type u_2
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_3
m : MonomialOrder.{u_3, u_4} ι
i : ι
r : R
simp : LT.lt.{u_4} (α := m.syn) (0 : m.syn) ((m.toSyn : (a : ι →₀ ℕ) → m.syn) (single i 1) : m.syn)
⊢ LT.lt.{u_4} (α := m.syn)
    ((m.toSyn : (a : ι →₀ ℕ) → m.syn) (degree.{u_3, u_2, u_4} m (R := R) ((C : (a : R) → MvPolynomial ι R) r)) : m.syn)
    ((m.toSyn : (a : ι →₀ ℕ) → m.syn) (degree.{u_3, u_2, u_4} m (R := R) (X i)) : m.syn)

Tactic:
simp only [degree_C, map_zero, degree_X]

Premises used: MonomialOrder.degree_X, map_zero, MonomialOrder.degree_C
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
R : Type u_2
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_3
m : MonomialOrder.{u_3, u_4} ι
i : ι
r : R
rw :
  Ne.{u_4 + 1} (α := m.syn) ((m.toSyn : (a : ι →₀ ℕ) → m.syn) (single i 1) : m.syn)
    ((m.toSyn : (a : ι →₀ ℕ) → m.syn) 0 : m.syn)
⊢ LT.lt.{u_4} (α := m.syn) (0 : m.syn) ((m.toSyn : (a : ι →₀ ℕ) → m.syn) (single i 1) : m.syn)

Tactic:
rw [← bot_eq_zero, bot_lt_iff_ne_bot, bot_eq_zero, ← map_zero m.toSyn]

Premises used: MonomialOrder.bot_eq_zero, map_zero, bot_lt_iff_ne_bot, MonomialOrder.toSyn
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
R : Type u_2
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_3
m : MonomialOrder.{u_3, u_4} ι
i : ι
r : R
⊢ Ne.{u_4 + 1} (α := m.syn) ((m.toSyn : (a : ι →₀ ℕ) → m.syn) (single i 1) : m.syn)
    ((m.toSyn : (a : ι →₀ ℕ) → m.syn) 0 : m.syn)

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
R : Type u_2
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_3
m : MonomialOrder.{u_3, u_4} ι
i : ι
r : R
rw :
  m.degree
      (HAdd.hAdd (α := MvPolynomial ι R) (β := MvPolynomial ι R) (X i)
        (-(C : (a : R) → MvPolynomial ι R) r : MvPolynomial ι R)) =
    single i 1
rw₁ :
  m.degree
      (HAdd.hAdd (α := MvPolynomial ι R) (β := MvPolynomial ι R) (X i)
        ((C : (a : R) → MvPolynomial ι R) (-r) : MvPolynomial ι R)) =
    single i 1
rw₂ rw₃ : Eq (α := ι →₀ ℕ) (single i 1) (single i 1)
⊢ m.degree
      (HSub.hSub (α := MvPolynomial ι R) (β := MvPolynomial ι R) (X i)
        ((C : (a : R) → MvPolynomial ι R) r : MvPolynomial ι R)) =
    single i 1

Tactic:
rw [sub_eq_add_neg, ← map_neg, degree_X_add_C]

Premises used: sub_eq_add_neg, map_neg, MonomialOrder.degree_X_add_C
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
R : Type u_2
inst : CommRing R
ι : Type u_3
m : MonomialOrder.{u_3, u_4} ι
i : ι
r : R
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
R : Type u_2
inst : CommRing R
ι : Type u_3
m : MonomialOrder.{u_3, u_4} ι
i : ι
r : R
h : Nontrivial R
apply :
  LT.lt.{u_4} (α := m.syn)
    ((m.toSyn : (a : ι →₀ ℕ) → m.syn) (degree.{u_3, u_2, u_4} m (R := R) ((C : (a : R) → MvPolynomial ι R) r)) : m.syn)
    ((m.toSyn : (a : ι →₀ ℕ) → m.syn) (degree.{u_3, u_2, u_4} m (R := R) (X i)) : m.syn)
⊢ m.Monic
    (HAdd.hAdd (α := MvPolynomial ι R) (β := MvPolynomial ι R) (X i)
      ((C : (a : R) → MvPolynomial ι R) r : MvPolynomial ι R))

Tactic:
apply monic_X.add_of_lt

Premises used: MonomialOrder.Monic.add_of_lt, MonomialOrder.monic_X
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
R : Type u_2
inst : CommRing R
ι : Type u_3
m : MonomialOrder.{u_3, u_4} ι
i : ι
r : R
h : Nontrivial R
⊢ LT.lt.{u_4} (α := m.syn)
    ((m.toSyn : (a : ι →₀ ℕ) → m.syn) (degree.{u_3, u_2, u_4} m (R := R) ((C : (a : R) → MvPolynomial ι R) r)) : m.syn)
    ((m.toSyn : (a : ι →₀ ℕ) → m.syn) (degree.{u_3, u_2, u_4} m (R := R) (X i)) : m.syn)

Tactic:
simp [degree_C, degree_X, ← not_le, ← eq_zero_iff]

Premises used: not_le, MonomialOrder.degree_X, MonomialOrder.degree_C, MonomialOrder.eq_zero_iff
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
R : Type u_2
inst : CommRing R
ι : Type u_3
m : MonomialOrder.{u_3, u_4} ι
i : ι
r : R
rw :
  m.Monic
    (HAdd.hAdd (α := MvPolynomial ι R) (β := MvPolynomial ι R) (X i)
      ((C : (a : R) → MvPolynomial ι R) (-r) : MvPolynomial ι R))
⊢ m.Monic
    (HSub.hSub (α := MvPolynomial ι R) (β := MvPolynomial ι R) (X i)
      ((C : (a : R) → MvPolynomial ι R) r : MvPolynomial ι R))

Tactic:
rw [sub_eq_add_neg, ← map_neg]

Premises used: sub_eq_add_neg, map_neg
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
R : Type u_2
inst : CommRing R
ι : Type u_3
m : MonomialOrder.{u_3, u_4} ι
i : ι
r : R
⊢ m.Monic
    (HAdd.hAdd (α := MvPolynomial ι R) (β := MvPolynomial ι R) (X i)
      ((C : (a : R) → MvPolynomial ι R) (-r) : MvPolynomial ι R))

Tactic:
apply monic_X_add_C

Premises used: MonomialOrder.monic_X_add_C
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
R : Type u_1
inst : CommSemiring R
σ : Type u_2
f : σ → R
s : Finset σ
n : ℕ
simp :
  Eq.{u_1 + 1} (α := R)
    (sum
      (map ((fun (x : Multiset R) ↦ x.prod) ∘ (fun (x : Multiset σ) ↦ map f x) ∘ Finset.val)
        (Finset.powersetCard n s).val))
    (∑ t ∈ Finset.powersetCard n s, t.prod f)
⊢ (map f s.val).esymm n = ∑ t ∈ Finset.powersetCard n s, t.prod f

Tactic:
simp only [esymm, powersetCard_map, ← Finset.map_val_val_powersetCard, map_map]

Premises used: Finset.map_val_val_powersetCard, Multiset.powersetCard_map, Multiset.map_map, Multiset.esymm
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
R : Type u_1
inst : CommSemiring R
σ : Type u_2
f : σ → R
s : Finset σ
n : ℕ
⊢ Eq.{u_1 + 1} (α := R)
    (sum
      (map ((fun (x : Multiset R) ↦ x.prod) ∘ (fun (x : Multiset σ) ↦ map f x) ∘ Finset.val)
        (Finset.powersetCard n s).val))
    (∑ t ∈ Finset.powersetCard n s, t.prod f)

Tactic:
simp only [Function.comp_apply, Finset.prod_map_val, Finset.sum_map_val]

Premises used: Finset.prod_map_val, Function.comp_apply, Finset.sum_map_val
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Monoid S
inst_2 : DistribMulAction S R
inst_3 : IsScalarTower S R R
inst_4 : SMulCommClass S R R
s : S
n : ℕ
m : Multiset R
rw :
  Eq (α := R) (sum (map ((fun (x : R) ↦ s ^ n • x) ∘ prod) (powersetCard n m))) (esymm (map (fun (x : R) ↦ s • x) m) n)
⊢ s ^ n • m.esymm n = esymm (map (fun (x : R) ↦ s • x) m) n

Tactic:
rw [esymm, smul_sum, map_map]

Premises used: Multiset.smul_sum, Multiset.map_map, Multiset.esymm
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Monoid S
inst_2 : DistribMulAction S R
inst_3 : IsScalarTower S R R
inst_4 : SMulCommClass S R R
s : S
n : ℕ
m : Multiset R
trans :
  Eq (α := R) (sum (map ((fun (x : R) ↦ s ^ n • x) ∘ prod) (powersetCard n m)))
    (sum (map (fun (x : Multiset R) ↦ s ^ x.card • x.prod) (powersetCard n m)))
trans₁ :
  Eq (α := R) (sum (map (fun (x : Multiset R) ↦ s ^ x.card • x.prod) (powersetCard n m)))
    (esymm (map (fun (x : R) ↦ s • x) m) n)
⊢ Eq (α := R) (sum (map ((fun (x : R) ↦ s ^ n • x) ∘ prod) (powersetCard n m))) (esymm (map (fun (x : R) ↦ s • x) m) n)

Tactic:
trans ((powersetCard n m).map (fun x : Multiset R ↦ s ^ card x • x.prod)).sum

Premises used: Multiset.sum, Multiset.map, Multiset.prod, HPow.hPow, Multiset.card, Multiset.powersetCard, HSMul.hSMul
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Monoid S
inst_2 : DistribMulAction S R
inst_3 : IsScalarTower S R R
inst_4 : SMulCommClass S R R
s : S
n : ℕ
m : Multiset R
⊢ Eq (α := R) (sum (map ((fun (x : R) ↦ s ^ n • x) ∘ prod) (powersetCard n m)))
    (sum (map (fun (x : Multiset R) ↦ s ^ x.card • x.prod) (powersetCard n m)))

Tactic:
congr_arg _ (map_congr rfl (fun x hx ↦ ?_))

Premises used: congr_arg, Multiset.map_congr, rfl
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Monoid S
inst_2 : DistribMulAction S R
inst_3 : IsScalarTower S R R
inst_4 : SMulCommClass S R R
s : S
n : ℕ
m : Multiset R
refine : ∀ (x : Multiset R) (hx : x ∈ powersetCard n m), ((fun (x : R) ↦ s ^ n • x) ∘ prod) x = s ^ x.card • x.prod
⊢ Eq (α := R) (sum (map ((fun (x : R) ↦ s ^ n • x) ∘ prod) (powersetCard n m)))
    (sum (map (fun (x : Multiset R) ↦ s ^ x.card • x.prod) (powersetCard n m)))

Tactic:
refine congr_arg _ (map_congr rfl (fun x hx ↦ ?_))

Premises used: congr_arg, Multiset.map_congr, rfl
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Monoid S
inst_2 : DistribMulAction S R
inst_3 : IsScalarTower S R R
inst_4 : SMulCommClass S R R
s : S
n : ℕ
m x : Multiset R
hx : x ∈ powersetCard n m
rw : s ^ n • x.prod = s ^ x.card • x.prod
rw₁ rw₂ : s ^ n • x.prod = s ^ n • x.prod
⊢ ((fun (x : R) ↦ s ^ n • x) ∘ prod) x = s ^ x.card • x.prod

Tactic:
rw [Function.comp_apply, (mem_powersetCard.1 hx).2]

Premises used: Multiset.mem_powersetCard, And.right, Iff.mp, Function.comp_apply