awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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 : σ →₀ ℕ
⊢ Eq.{u_2 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) m : M) (0 : M) ↔
    ∀ (x : σ), Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)
have simp : Eq.{u_2 + 1} (α := M) (m.sum fun (i : σ) (c : ℕ) ↦ c • w i) 0 ↔ ∀ (x : σ), Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)
Tactic: simp only [weight, Finsupp.linearCombination, LinearMap.toAddMonoidHom_coe, coe_lsum,
    LinearMap.coe_smulRight, LinearMap.id_coe, id_eq]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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 : σ →₀ ℕ
⊢ Eq.{u_2 + 1} (α := M) (m.sum fun (i : σ) (c : ℕ) ↦ c • w i) 0 ↔
    ∀ (x : σ), Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)
have rw : (∀ i ∈ m.support, HSMul.hSMul (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (w i) = 0) ↔
  ∀ (x : σ), Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)
Tactic: rw [Finsupp.sum, Finset.sum_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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 : σ →₀ ℕ
⊢ (∀ i ∈ m.support, HSMul.hSMul (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (w i) = 0) ↔
    ∀ (x : σ), Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)
have h : ∀ (a : σ),
  a ∈ m.support → HSMul.hSMul (α := ℕ) ((m : (a : σ) → ℕ) a : ℕ) (w a) = 0 ↔
    Eq (α := ℕ) ((m : (a : σ) → ℕ) a : ℕ) (0 : ℕ)
Tactic: apply forall_congr'
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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 : σ
⊢ x ∈ m.support → HSMul.hSMul (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (w x) = 0 ↔
    Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)
have h : Ne (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ) → HSMul.hSMul (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (w x) = 0 ↔
  Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)
Tactic: rw [Finsupp.mem_support_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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 : σ
⊢ Ne (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ) → HSMul.hSMul (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (w x) = 0 ↔
    Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)
have h : (Ne (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ) → HSMul.hSMul (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (w x) = 0) →
  Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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 : ℕ)
⊢ Ne (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ) → HSMul.hSMul (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (w x) = 0 ↔
    Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)
have h₁ : Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ) →
  Ne (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ) → HSMul.hSMul (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (w x) = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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
⊢ Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)
have h : ∀ (hx' : ¬Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)), False
Tactic: by_contra hx'
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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
⊢ Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ) →
    Ne (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ) → HSMul.hSMul (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (w x) = 0
have h₂ : Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ) →
  Ne (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ) → HSMul.hSMul (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (w x) ≠ 0 → False
Tactic: order
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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
⊢ IsWeightedHomogeneous w p 0 ↔ weightedTotalDegree w p = 0
have 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)
Tactic: rw [weightedTotalDegree, ← bot_eq_zero, Finset.sup_eq_bot_iff, bot_eq_zero, IsWeightedHomogeneous]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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
⊢ (∀ ⦃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)
have 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)
Tactic: apply forall_congr'
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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 : σ →₀ ℕ
⊢ 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)
have 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)
Tactic: rw [mem_support_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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
⊢ weightedTotalDegree w p = 0 ↔ ∀ m ∈ p.support, ∀ (x : σ), Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)
have 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 : ℕ)
Tactic: rw [← isWeightedHomogeneous_zero_iff_weightedTotalDegree_eq_zero, IsWeightedHomogeneous]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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
⊢ (∀ ⦃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 : ℕ)
have 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 : ℕ)
Tactic: apply forall_congr'
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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 : σ →₀ ℕ
⊢ 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 : ℕ)
have 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 : ℕ)
Tactic: rw [mem_support_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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 : σ →₀ ℕ
⊢ 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 : ℕ)
have 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 : ℕ)
Tactic: apply forall_congr'
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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
⊢ Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
have h : ∀ d ∈ φ.support, (weight w : (a : σ →₀ ℕ) → M) d ≠ i
Tactic: apply weightedHomogeneousComponent_eq_zero'
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (hypothesis)
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
⊢ ∀ d ∈ φ.support, (weight w : (a : σ →₀ ℕ) → M) d ≠ i
have hi₁ : ∀ (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
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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
⊢ (↑((((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) φ
have pos : ∀ (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) φ) sorry :
            (a : M) → ↥(weightedHomogeneousSubmodule R w a))
          m) :
      MvPolynomial σ R) =
    (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ
Tactic: by_cases hm : m ∈ Finset.image (weight w) φ.support
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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
⊢ (↑((((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) φ
have neg : Eq (α := MvPolynomial σ R) ((↑0 : MvPolynomial σ R) : MvPolynomial σ R)
  ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
Tactic: rw [DirectSum.mk_apply_of_notMem hm, Submodule.coe_zero,
      weightedHomogeneousComponent_eq_zero_of_notMem w φ m hm]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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)
⊢ (↑((((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) φ
have neg₁ : Eq (α := MvPolynomial σ R) (0 : MvPolynomial σ R)
  ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
Tactic: rw [DirectSum.mk_apply_of_notMem hm, Submodule.coe_zero,
      weightedHomogeneousComponent_eq_zero_of_notMem w φ m hm]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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)
⊢ (↑((((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) φ
have neg₂ : Eq (α := MvPolynomial σ R) 0 0
Tactic: rw [DirectSum.mk_apply_of_notMem hm, Submodule.coe_zero,
      weightedHomogeneousComponent_eq_zero_of_notMem w φ m hm]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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
| φ
have rw : ∑ᶠ (m : M), (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ
Tactic: rw [← sum_weightedHomogeneousComponent w φ]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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
⊢ (DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w) :
        (a : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
      (decompose' R w φ) =
    φ
have 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)
Tactic: conv_rhs => rw [← sum_weightedHomogeneousComponent w φ]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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
⊢ 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)
have 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) φ)
Tactic: rw [← DirectSum.sum_support_of (decompose' R w φ)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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
⊢ 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) φ)
have 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) φ)
        sorry,
    (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
Tactic: simp only [DirectSum.coeAddMonoidHom_of, map_sum,
      finsum_eq_sum _ (weightedHomogeneousComponent_finsupp φ)]