awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
M : Type u_2
σ : Type u_3
inst : AddCommMonoid M
inst_1 : PartialOrder M
w : σ → M
inst_2 : CanonicallyOrderedAdd M
hw : NonTorsionWeight w
m : σ →₀ ℕ
rw :
  (∀ i ∈ m.support, HSMul.hSMul (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (w i) = 0) ↔
    ∀ (x : σ), Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)
⊢ Eq.{u_2 + 1} (α := M) (m.sum fun (i : σ) (c : ℕ) ↦ c • w i) 0 ↔
    ∀ (x : σ), Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)

Tactic:
rw [Finsupp.sum, Finset.sum_eq_zero_iff]

Premises used: Finsupp.sum, Finset.sum_eq_zero_iff
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
M : Type u_2
σ : Type u_3
inst : AddCommMonoid M
inst_1 : PartialOrder M
w : σ → M
inst_2 : CanonicallyOrderedAdd M
hw : NonTorsionWeight w
m : σ →₀ ℕ
h :
  ∀ (a : σ),
    a ∈ m.support → HSMul.hSMul (α := ℕ) ((m : (a : σ) → ℕ) a : ℕ) (w a) = 0 ↔
      Eq (α := ℕ) ((m : (a : σ) → ℕ) a : ℕ) (0 : ℕ)
⊢ (∀ i ∈ m.support, HSMul.hSMul (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (w i) = 0) ↔
    ∀ (x : σ), Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)

Tactic:
apply forall_congr'

Premises used: forall_congr'
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
M : Type u_2
σ : Type u_3
inst : AddCommMonoid M
inst_1 : PartialOrder M
w : σ → M
inst_2 : CanonicallyOrderedAdd M
hw : NonTorsionWeight w
m : σ →₀ ℕ
x : σ
h :
  Ne (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ) → HSMul.hSMul (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (w x) = 0 ↔
    Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)
⊢ x ∈ m.support → HSMul.hSMul (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (w x) = 0 ↔
    Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)

Tactic:
rw [Finsupp.mem_support_iff]

Premises used: Finsupp.mem_support_iff
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
M : Type u_2
σ : Type u_3
inst : AddCommMonoid M
inst_1 : PartialOrder M
w : σ → M
inst_2 : CanonicallyOrderedAdd M
hw : NonTorsionWeight w
m : σ →₀ ℕ
x : σ
h :
  (Ne (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ) → HSMul.hSMul (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (w x) = 0) →
    Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)
h₁ :
  Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ) →
    Ne (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ) → HSMul.hSMul (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (w x) = 0
⊢ Ne (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ) → HSMul.hSMul (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (w x) = 0 ↔
    Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)

Tactic:
constructor
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
M : Type u_2
σ : Type u_3
inst : AddCommMonoid M
inst_1 : PartialOrder M
w : σ → M
inst_2 : CanonicallyOrderedAdd M
hw : NonTorsionWeight w
m : σ →₀ ℕ
x : σ
hx : Ne (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ) → HSMul.hSMul (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (w x) = 0
h : ∀ (hx' : ¬Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)), False
⊢ Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)

Tactic:
by_contra hx'
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
M : Type u_2
σ : Type u_3
inst : AddCommMonoid M
inst_1 : PartialOrder M
w : σ → M
inst_2 : CanonicallyOrderedAdd M
hw : NonTorsionWeight w
m : σ →₀ ℕ
x : σ
hx : Ne (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ) → HSMul.hSMul (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (w x) = 0
hx' : ¬Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)
⊢ False

Tactic:
absurd (hw _ _ (hx hx')) hx'

Premises used: absurd
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
M : Type u_2
σ : Type u_3
inst : AddCommMonoid M
inst_1 : PartialOrder M
w : σ → M
inst_2 : CanonicallyOrderedAdd M
hw : NonTorsionWeight w
m : σ →₀ ℕ
x : σ
hx : Ne (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ) → HSMul.hSMul (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (w x) = 0
hx' : ¬Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)
⊢ False

Tactic:
exact absurd (hw _ _ (hx hx')) hx'

Premises used: absurd
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
M : Type u_2
σ : Type u_3
inst : AddCommMonoid M
inst_1 : PartialOrder M
w : σ → M
inst_2 : CanonicallyOrderedAdd M
hw : NonTorsionWeight w
m : σ →₀ ℕ
x : σ
h h₁ :
  Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ) →
    Ne (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ) → HSMul.hSMul (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (w x) = 0
h₂ h₃ :
  Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ) →
    Ne (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ) → HSMul.hSMul (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (w x) ≠ 0 → False
⊢ Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ) →
    Ne (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ) → HSMul.hSMul (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (w x) = 0

Tactic:
order
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
inst_2 : LinearOrder M
inst_3 : OrderBot M
inst_4 : CanonicallyOrderedAdd M
w : σ → M
p : MvPolynomial σ R
rw :
  (∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → Eq.{u_2 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) d : M) (0 : M)) ↔
    ∀ s ∈ p.support, Eq.{u_2 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) s : M) (0 : M)
⊢ IsWeightedHomogeneous w p 0 ↔ weightedTotalDegree w p = 0

Tactic:
rw [weightedTotalDegree, ← bot_eq_zero, Finset.sup_eq_bot_iff, bot_eq_zero, IsWeightedHomogeneous]

Premises used: MvPolynomial.weightedTotalDegree, MvPolynomial.IsWeightedHomogeneous, bot_eq_zero, Finset.sup_eq_bot_iff
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
inst_2 : LinearOrder M
inst_3 : OrderBot M
inst_4 : CanonicallyOrderedAdd M
w : σ → M
p : MvPolynomial σ R
h :
  ∀ (a : σ →₀ ℕ),
    coeff a p ≠ 0 → Eq.{u_2 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) a : M) (0 : M) ↔
      a ∈ p.support → Eq.{u_2 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) a : M) (0 : M)
⊢ (∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → Eq.{u_2 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) d : M) (0 : M)) ↔
    ∀ s ∈ p.support, Eq.{u_2 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) s : M) (0 : M)

Tactic:
apply forall_congr'

Premises used: forall_congr'
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
inst_2 : LinearOrder M
inst_3 : OrderBot M
inst_4 : CanonicallyOrderedAdd M
w : σ → M
p : MvPolynomial σ R
m : σ →₀ ℕ
h h₁ :
  coeff m p ≠ 0 → Eq.{u_2 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) m : M) (0 : M) ↔
    coeff m p ≠ 0 → Eq.{u_2 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) m : M) (0 : M)
⊢ coeff m p ≠ 0 → Eq.{u_2 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) m : M) (0 : M) ↔
    m ∈ p.support → Eq.{u_2 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) m : M) (0 : M)

Tactic:
rw [mem_support_iff]

Premises used: MvPolynomial.mem_support_iff
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
inst_2 : LinearOrder M
inst_3 : OrderBot M
inst_4 : CanonicallyOrderedAdd M
w : σ → M
hw : NonTorsionWeight w
p : MvPolynomial σ R
rw :
  (∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → Eq.{u_2 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) d : M) (0 : M)) ↔
    ∀ m ∈ p.support, ∀ (x : σ), Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)
⊢ weightedTotalDegree w p = 0 ↔ ∀ m ∈ p.support, ∀ (x : σ), Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)

Tactic:
rw [← isWeightedHomogeneous_zero_iff_weightedTotalDegree_eq_zero, IsWeightedHomogeneous]

Premises used: MvPolynomial.isWeightedHomogeneous_zero_iff_weightedTotalDegree_eq_zero, MvPolynomial.IsWeightedHomogeneous
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
inst_2 : LinearOrder M
inst_3 : OrderBot M
inst_4 : CanonicallyOrderedAdd M
w : σ → M
hw : NonTorsionWeight w
p : MvPolynomial σ R
h :
  ∀ (a : σ →₀ ℕ),
    coeff a p ≠ 0 → Eq.{u_2 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) a : M) (0 : M) ↔
      a ∈ p.support → ∀ (x : σ), Eq (α := ℕ) ((a : (a : σ) → ℕ) x : ℕ) (0 : ℕ)
⊢ (∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → Eq.{u_2 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) d : M) (0 : M)) ↔
    ∀ m ∈ p.support, ∀ (x : σ), Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)

Tactic:
apply forall_congr'

Premises used: forall_congr'
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
inst_2 : LinearOrder M
inst_3 : OrderBot M
inst_4 : CanonicallyOrderedAdd M
w : σ → M
hw : NonTorsionWeight w
p : MvPolynomial σ R
m : σ →₀ ℕ
h :
  coeff m p ≠ 0 → Eq.{u_2 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) m : M) (0 : M) ↔
    coeff m p ≠ 0 → ∀ (x : σ), Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)
⊢ coeff m p ≠ 0 → Eq.{u_2 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) m : M) (0 : M) ↔
    m ∈ p.support → ∀ (x : σ), Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)

Tactic:
rw [mem_support_iff]

Premises used: MvPolynomial.mem_support_iff
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
inst_2 : LinearOrder M
inst_3 : OrderBot M
inst_4 : CanonicallyOrderedAdd M
w : σ → M
hw : NonTorsionWeight w
p : MvPolynomial σ R
m : σ →₀ ℕ
h :
  ∀ (a : coeff m p ≠ 0),
    Eq.{u_2 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) m : M) (0 : M) ↔
      ∀ (x : σ), Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)
⊢ coeff m p ≠ 0 → Eq.{u_2 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) m : M) (0 : M) ↔
    coeff m p ≠ 0 → ∀ (x : σ), Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)

Tactic:
apply forall_congr'

Premises used: forall_congr'
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
inst_2 : LinearOrder M
inst_3 : OrderBot M
inst_4 : CanonicallyOrderedAdd M
w : σ → M
hw : NonTorsionWeight w
p : MvPolynomial σ R
m : σ →₀ ℕ
h : coeff m p ≠ 0
⊢ Eq.{u_2 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) m : M) (0 : M) ↔
    ∀ (x : σ), Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)

Tactic:
weightedDegree_eq_zero_iff hw

Premises used: MvPolynomial.weightedDegree_eq_zero_iff
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
inst_2 : LinearOrder M
inst_3 : OrderBot M
inst_4 : CanonicallyOrderedAdd M
w : σ → M
hw : NonTorsionWeight w
p : MvPolynomial σ R
m : σ →₀ ℕ
h : coeff m p ≠ 0
⊢ Eq.{u_2 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) m : M) (0 : M) ↔
    ∀ (x : σ), Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)

Tactic:
exact weightedDegree_eq_zero_iff hw

Premises used: MvPolynomial.weightedDegree_eq_zero_iff
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : DecidableEq M
φ : MvPolynomial σ R
i : M
hi : i ∉ Finset.image (⇑(weight w) : (a : σ →₀ ℕ) → M) φ.support
h : ∀ d ∈ φ.support, (weight w : (a : σ →₀ ℕ) → M) d ≠ i
⊢ Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
    (0 : MvPolynomial σ R)

Tactic:
apply weightedHomogeneousComponent_eq_zero'

Premises used: MvPolynomial.weightedHomogeneousComponent_eq_zero'
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : DecidableEq M
φ : MvPolynomial σ R
i : M
hi : i ∉ Finset.image (⇑(weight w) : (a : σ →₀ ℕ) → M) φ.support
⊢ ∀ (x : σ →₀ ℕ), ¬coeff x φ = 0 → ¬(weight w : (a : σ →₀ ℕ) → M) x = i

Tactic:
simp only [Finset.mem_image, mem_support_iff, ne_eq, not_exists, not_and] at hi

Premises used: MvPolynomial.mem_support_iff, Finset.mem_image, not_exists, ne_eq, not_and
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : DecidableEq M
φ : MvPolynomial σ R
i : M
hi : ∀ (x : σ →₀ ℕ), ¬coeff x φ = 0 → ¬(weight w : (a : σ →₀ ℕ) → M) x = i
⊢ ∀ d ∈ φ.support, (weight w : (a : σ →₀ ℕ) → M) d ≠ i

Tactic:
fun m hm ↦ hi m (mem_support_iff.mp hm)

Premises used: MvPolynomial.mem_support_iff, Iff.mp
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : DecidableEq M
φ : MvPolynomial σ R
i : M
hi : ∀ (x : σ →₀ ℕ), ¬coeff x φ = 0 → ¬(weight w : (a : σ →₀ ℕ) → M) x = i
⊢ ∀ d ∈ φ.support, (weight w : (a : σ →₀ ℕ) → M) d ≠ i

Tactic:
exact fun m hm ↦ hi m (mem_support_iff.mp hm)

Premises used: MvPolynomial.mem_support_iff, Iff.mp
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : DecidableEq M
φ : MvPolynomial σ R
m : M
hm : Membership.mem (γ := Finset M) (Finset.image (⇑(weight w) : (a : σ →₀ ℕ) → M) φ.support) m
⊢ (↑((((DirectSum.mk (fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i))
                    (Finset.image (⇑(weight w) : (a : σ →₀ ℕ) → M) φ.support) :
                  ((i : (↑(↑(Finset.image (⇑(weight w) : (a : σ →₀ ℕ) → M) φ.support) : Set M) : Type u_2)) →
                      ↥(weightedHomogeneousSubmodule R w (↑i : M))) →+
                    DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) :
                (a :
                    (i : (↑(↑(Finset.image (⇑(weight w) : (a : σ →₀ ℕ) → M) φ.support) : Set M) : Type u_2)) →
                      ↥(weightedHomogeneousSubmodule R w (↑i : M))) →
                  DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i))
              fun (m : (↑(↑(Finset.image (⇑(weight w) : (a : σ →₀ ℕ) → M) φ.support) : Set M) : Type u_2)) ↦
              Subtype.mk (p := fun (x : MvPolynomial σ R) ↦
                Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w (↑m : M)) x)
                ((weightedHomogeneousComponent w (↑m : M) : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) ⋯ :
            (a : M) → ↥(weightedHomogeneousSubmodule R w a))
          m) :
      MvPolynomial σ R) =
    (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ

Tactic:
simp only [DirectSum.mk_apply_of_mem hm, Subtype.coe_mk]

Premises used: Subtype.coe_mk, DirectSum.mk_apply_of_mem
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : DecidableEq M
φ : MvPolynomial σ R
m : M
hm : m ∉ Finset.image (⇑(weight w) : (a : σ →₀ ℕ) → M) φ.support
neg :
  Eq (α := MvPolynomial σ R) ((↑0 : MvPolynomial σ R) : MvPolynomial σ R)
    ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
neg₁ :
  Eq (α := MvPolynomial σ R) (0 : MvPolynomial σ R)
    ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
neg₂ neg₃ : Eq (α := MvPolynomial σ R) 0 0
⊢ (↑((((DirectSum.mk (fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i))
                    (Finset.image (⇑(weight w) : (a : σ →₀ ℕ) → M) φ.support) :
                  ((i : (↑(↑(Finset.image (⇑(weight w) : (a : σ →₀ ℕ) → M) φ.support) : Set M) : Type u_2)) →
                      ↥(weightedHomogeneousSubmodule R w (↑i : M))) →+
                    DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) :
                (a :
                    (i : (↑(↑(Finset.image (⇑(weight w) : (a : σ →₀ ℕ) → M) φ.support) : Set M) : Type u_2)) →
                      ↥(weightedHomogeneousSubmodule R w (↑i : M))) →
                  DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i))
              fun (m : (↑(↑(Finset.image (⇑(weight w) : (a : σ →₀ ℕ) → M) φ.support) : Set M) : Type u_2)) ↦
              Subtype.mk (p := fun (x : MvPolynomial σ R) ↦
                Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w (↑m : M)) x)
                ((weightedHomogeneousComponent w (↑m : M) : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) ⋯ :
            (a : M) → ↥(weightedHomogeneousSubmodule R w a))
          m) :
      MvPolynomial σ R) =
    (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ

Tactic:
rw [DirectSum.mk_apply_of_notMem hm, Submodule.coe_zero,
      weightedHomogeneousComponent_eq_zero_of_notMem w φ m hm]

Premises used: DirectSum.mk_apply_of_notMem, Submodule.coe_zero, MvPolynomial.weightedHomogeneousComponent_eq_zero_of_notMem
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : DecidableEq M
φ : MvPolynomial σ R
rw : ∑ᶠ (m : M), (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ
| φ

Tactic:
rw [← sum_weightedHomogeneousComponent w φ]

Premises used: MvPolynomial.sum_weightedHomogeneousComponent
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : DecidableEq M
φ : MvPolynomial σ R
conv_rhs :
  Eq (α := MvPolynomial σ R)
    ((DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w) :
          (a : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
        (decompose' R w φ) :
      MvPolynomial σ R)
    (∑ᶠ (m : M), (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
⊢ (DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w) :
        (a : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
      (decompose' R w φ) =
    φ

Tactic:
conv_rhs => rw [← sum_weightedHomogeneousComponent w φ]

Premises used: MvPolynomial.sum_weightedHomogeneousComponent
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : DecidableEq M
φ : MvPolynomial σ R
rw :
  Eq (α := MvPolynomial σ R)
    ((DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w) :
        (a : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
      (∑ i ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) (decompose' R w φ),
        ((DirectSum.of (fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) i :
              ↥(weightedHomogeneousSubmodule R w i) →+
                DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) :
            (a : ↥(weightedHomogeneousSubmodule R w i)) →
              DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i))
          ((decompose' R w φ : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) i)))
    (∑ᶠ (m : M), (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
⊢ Eq (α := MvPolynomial σ R)
    ((DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w) :
          (a : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
        (decompose' R w φ) :
      MvPolynomial σ R)
    (∑ᶠ (m : M), (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)

Tactic:
rw [← DirectSum.sum_support_of (decompose' R w φ)]

Premises used: MvPolynomial.decompose', DirectSum.sum_support_of
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : DecidableEq M
φ : MvPolynomial σ R
simp :
  Eq (α := MvPolynomial σ R)
    (∑ x ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) (decompose' R w φ),
      (↑((decompose' R w φ : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) x) : MvPolynomial σ R))
    (∑
      m ∈
        Finite.toFinset (s :=
          Function.support (M := MvPolynomial σ R) fun (m : M) ↦
            (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
          ⋯,
      (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
⊢ Eq (α := MvPolynomial σ R)
    ((DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w) :
        (a : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
      (∑ i ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) (decompose' R w φ),
        ((DirectSum.of (fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) i :
              ↥(weightedHomogeneousSubmodule R w i) →+
                DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) :
            (a : ↥(weightedHomogeneousSubmodule R w i)) →
              DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i))
          ((decompose' R w φ : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) i)))
    (∑ᶠ (m : M), (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)

Tactic:
simp only [DirectSum.coeAddMonoidHom_of, map_sum,
      finsum_eq_sum _ (weightedHomogeneousComponent_finsupp φ)]

Premises used: finsum_eq_sum, map_sum, DirectSum.coeAddMonoidHom_of, MvPolynomial.weightedHomogeneousComponent_finsupp
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : DecidableEq M
φ : MvPolynomial σ R
m : M
h :
  Membership.mem (γ := Finset M)
    (Finite.toFinset (s :=
      Function.support (M := MvPolynomial σ R) fun (m : M) ↦
        (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
      ⋯)
    m
rw rw₁ :
  Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
    ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
⊢ (↑((decompose' R w φ : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R) =
    (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ

Tactic:
rw [decompose'_apply]

Premises used: MvPolynomial.decompose'_apply
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : DecidableEq M
φ : MvPolynomial σ R
apply :
  DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) (decompose' R w φ) =
    Finite.toFinset (s :=
      Function.support (M := MvPolynomial σ R) fun (m : M) ↦
        (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
      ⋯
⊢ Eq (α := MvPolynomial σ R)
    (∑ x ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) (decompose' R w φ),
      (↑((decompose' R w φ : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) x) : MvPolynomial σ R))
    (∑
      m ∈
        Finite.toFinset (s :=
          Function.support (M := MvPolynomial σ R) fun (m : M) ↦
            (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
          ⋯,
      (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)

Tactic:
apply Finset.sum_congr _ (fun m _ ↦ by rw [decompose'_apply])

Premises used: Finset.sum_congr