awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
w : σ → M
inst_2 : DecidableEq M
m n : M
p : MvPolynomial σ R
h : IsWeightedHomogeneous w p n
x : σ →₀ ℕ
pos :
  ∀ (zero_coeff : coeff x p = 0),
    (if (weight w : (a : σ →₀ ℕ) → M) x = m then coeff x p else 0) = coeff x (if m = n then p else 0)
⊢ (if (weight w : (a : σ →₀ ℕ) → M) x = m then coeff x p else 0) = coeff x (if m = n then p else 0)
have neg : ∀ (zero_coeff : ¬coeff x p = 0),
  (if (weight w : (a : σ →₀ ℕ) → M) x = m then coeff x p else 0) = coeff x (if m = n then p else 0)
Tactic: by_cases zero_coeff : coeff x p = 0
-- 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
w : σ → M
inst_2 : DecidableEq M
m n : M
p : MvPolynomial σ R
h : IsWeightedHomogeneous w p n
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
⊢ (if (weight w : (a : σ →₀ ℕ) → M) x = m then coeff x p else 0) = coeff x (if m = n then p else 0)
have pos : (weight w : (a : σ →₀ ℕ) → M) x = m → m = n → coeff x p = coeff x p
Tactic: split_ifs
-- 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
w : σ → M
inst_2 : DecidableEq M
m n : M
p : MvPolynomial σ R
h : IsWeightedHomogeneous w p n
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
pos : (weight w : (a : σ →₀ ℕ) → M) x = m → m = n → coeff x p = coeff x p
⊢ (if (weight w : (a : σ →₀ ℕ) → M) x = m then coeff x p else 0) = coeff x (if m = n then p else 0)
have neg : (weight w : (a : σ →₀ ℕ) → M) x = m → ¬m = n → coeff x p = coeff x 0
Tactic: split_ifs
-- 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
w : σ → M
inst_2 : DecidableEq M
m n : M
p : MvPolynomial σ R
h : IsWeightedHomogeneous w p n
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
pos : (weight w : (a : σ →₀ ℕ) → M) x = m → m = n → coeff x p = coeff x p
neg : (weight w : (a : σ →₀ ℕ) → M) x = m → ¬m = n → coeff x p = coeff x 0
⊢ (if (weight w : (a : σ →₀ ℕ) → M) x = m then coeff x p else 0) = coeff x (if m = n then p else 0)
have pos₁ : ¬(weight w : (a : σ →₀ ℕ) → M) x = m → m = n → 0 = coeff x p
Tactic: split_ifs
-- 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
w : σ → M
inst_2 : DecidableEq M
m n : M
p : MvPolynomial σ R
h : IsWeightedHomogeneous w p n
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
pos : (weight w : (a : σ →₀ ℕ) → M) x = m → m = n → coeff x p = coeff x p
neg : (weight w : (a : σ →₀ ℕ) → M) x = m → ¬m = n → coeff x p = coeff x 0
pos₁ : ¬(weight w : (a : σ →₀ ℕ) → M) x = m → m = n → 0 = coeff x p
⊢ (if (weight w : (a : σ →₀ ℕ) → M) x = m then coeff x p else 0) = coeff x (if m = n then p else 0)
have neg₁ : ¬(weight w : (a : σ →₀ ℕ) → M) x = m → ¬m = n → Eq.{u_1 + 1} (α := R) 0 (coeff x 0)
Tactic: split_ifs
-- 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
w : σ → M
inst_2 : DecidableEq M
m n : M
p : MvPolynomial σ R
h : IsWeightedHomogeneous w p n
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ (if (weight w : (a : σ →₀ ℕ) → M) x = m then coeff x p else 0) = coeff x (if m = n then p else 0)
have neg : (if n = m then coeff x p else 0) = coeff x (if m = n then p else 0)
Tactic: rw [h zero_coeff]
-- 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
w : σ → M
inst_2 : DecidableEq M
m n : M
p : MvPolynomial σ R
h : IsWeightedHomogeneous w p n
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ (if n = m then coeff x p else 0) = coeff x (if m = n then p else 0)
have neg : (if m = n then coeff x p else 0) = coeff x (if m = n then p else 0)
Tactic: simp only [show n = m ↔ m = n from eq_comm]
-- 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
w : σ → M
inst_2 : DecidableEq M
m n : M
p : MvPolynomial σ R
h : IsWeightedHomogeneous w p n
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ (if m = n then coeff x p else 0) = coeff x (if m = n then p else 0)
have pos : ∀ (h1 : m = n), coeff x p = coeff x p
Tactic: split_ifs with h1
-- 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
w : σ → M
inst_2 : DecidableEq M
m n : M
p : MvPolynomial σ R
h : IsWeightedHomogeneous w p n
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
pos : ∀ (h1 : m = n), coeff x p = coeff x p
⊢ (if m = n then coeff x p else 0) = coeff x (if m = n then p else 0)
have neg : ∀ (h1 : ¬m = n), Eq.{u_1 + 1} (α := R) 0 (coeff x 0)
Tactic: split_ifs with h1
-- 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
w : σ → M
inst_2 : DecidableEq M
n : M
p : MvPolynomial σ R
⊢ support.{u_1, u_3} (R := R) ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) p) =
    {c ∈ p.support | (weight w : (a : σ →₀ ℕ) → M) c = n}
have h : ∀ (c : σ →₀ ℕ),
  Membership.mem (γ := Finset (σ →₀ ℕ))
      (support.{u_1, u_3} (R := R) ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) p))
      c ↔
    c ∈ {c ∈ p.support | (weight w : (a : σ →₀ ℕ) → M) c = n}
Tactic: ext c
-- 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
w : σ → M
inst_2 : DecidableEq σ
inst_3 : DecidableEq R
inst_4 : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
⊢ Eq (α := MvPolynomial σ R)
    ((coeLinearMap fun (i : M) ↦ weightedHomogeneousSubmodule R w i :
          (a : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
        x :
      MvPolynomial σ R)
    (DFinsupp.sum (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x
        fun (x : M) (x_1 : ↥(weightedHomogeneousSubmodule R w x)) ↦ (↑x_1 : MvPolynomial σ R) :
      MvPolynomial σ R)
have rw : Eq (α := MvPolynomial σ R)
  (DFinsupp.sum (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x
    fun (i : M) (x : ↥(weightedHomogeneousSubmodule R w i)) ↦ (↑x : MvPolynomial σ R))
  (DFinsupp.sum (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x
    fun (x : M) (x_1 : ↥(weightedHomogeneousSubmodule R w x)) ↦ (↑x_1 : MvPolynomial σ R))
Tactic: rw [_root_.DirectSum.coeLinearMap_eq_dfinsuppSum]
-- 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
w : σ → M
inst_2 : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
⊢ Eq (α := MvPolynomial σ R)
    ((coeLinearMap fun (i : M) ↦ weightedHomogeneousSubmodule R w i :
          (a : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
        x :
      MvPolynomial σ R)
    (∑ᶠ (m : M), (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R) : MvPolynomial σ R)
have h : (Function.support (M := MvPolynomial σ R) fun (m : M) ↦
    (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)) ⊆
  (↑(DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x) : Set M)
Tactic: rw [DirectSum.coeLinearMap_eq_dfinsuppSum, DFinsupp.sum, finsum_eq_sum_of_support_subset]
-- 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
w : σ → M
inst_2 : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
⊢ Eq (α := MvPolynomial σ R)
    ((coeLinearMap fun (i : M) ↦ weightedHomogeneousSubmodule R w i :
          (a : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
        x :
      MvPolynomial σ R)
    (∑ᶠ (m : M), (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R) : MvPolynomial σ R)
have rw : Eq (α := MvPolynomial σ R)
  (DFinsupp.sum (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x
    fun (x : M) (x_1 : ↥(weightedHomogeneousSubmodule R w x)) ↦ (↑x_1 : MvPolynomial σ R))
  (∑ᶠ (m : M), (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R))
Tactic: classical
  rw [DirectSum.coeLinearMap_eq_dfinsuppSum, DFinsupp.sum, finsum_eq_sum_of_support_subset]
  apply DirectSum.support_subset
-- 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
w : σ → M
inst_2 : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
rw :
  Eq (α := MvPolynomial σ R)
    (DFinsupp.sum (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x
      fun (x : M) (x_1 : ↥(weightedHomogeneousSubmodule R w x)) ↦ (↑x_1 : MvPolynomial σ R))
    (∑ᶠ (m : M), (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R))
⊢ Eq (α := MvPolynomial σ R)
    ((coeLinearMap fun (i : M) ↦ weightedHomogeneousSubmodule R w i :
          (a : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
        x :
      MvPolynomial σ R)
    (∑ᶠ (m : M), (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R) : MvPolynomial σ R)
have rw₁ : Eq (α := MvPolynomial σ R)
  (∑ i ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x,
    (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) i) : MvPolynomial σ R))
  (∑ᶠ (m : M), (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R))
Tactic: classical
  rw [DirectSum.coeLinearMap_eq_dfinsuppSum, DFinsupp.sum, finsum_eq_sum_of_support_subset]
  apply DirectSum.support_subset
-- 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
w : σ → M
inst_2 : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
rw :
  Eq (α := MvPolynomial σ R)
    (DFinsupp.sum (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x
      fun (x : M) (x_1 : ↥(weightedHomogeneousSubmodule R w x)) ↦ (↑x_1 : MvPolynomial σ R))
    (∑ᶠ (m : M), (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R))
rw₁ :
  Eq (α := MvPolynomial σ R)
    (∑ i ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x,
      (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) i) : MvPolynomial σ R))
    (∑ᶠ (m : M), (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R))
⊢ Eq (α := MvPolynomial σ R)
    ((coeLinearMap fun (i : M) ↦ weightedHomogeneousSubmodule R w i :
          (a : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
        x :
      MvPolynomial σ R)
    (∑ᶠ (m : M), (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R) : MvPolynomial σ R)
have rw₂ : Eq (α := MvPolynomial σ R)
  (∑ i ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x,
    (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) i) : MvPolynomial σ R))
  (∑ i ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x,
    (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) i) : MvPolynomial σ R))
Tactic: classical
  rw [DirectSum.coeLinearMap_eq_dfinsuppSum, DFinsupp.sum, finsum_eq_sum_of_support_subset]
  apply DirectSum.support_subset
-- 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
w : σ → M
inst_2 : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
rw :
  Eq (α := MvPolynomial σ R)
    (DFinsupp.sum (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x
      fun (x : M) (x_1 : ↥(weightedHomogeneousSubmodule R w x)) ↦ (↑x_1 : MvPolynomial σ R))
    (∑ᶠ (m : M), (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R))
rw₁ :
  Eq (α := MvPolynomial σ R)
    (∑ i ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x,
      (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) i) : MvPolynomial σ R))
    (∑ᶠ (m : M), (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R))
rw₂ :
  Eq (α := MvPolynomial σ R)
    (∑ i ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x,
      (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) i) : MvPolynomial σ R))
    (∑ i ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x,
      (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) i) : MvPolynomial σ R))
⊢ Eq (α := MvPolynomial σ R)
    ((coeLinearMap fun (i : M) ↦ weightedHomogeneousSubmodule R w i :
          (a : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
        x :
      MvPolynomial σ R)
    (∑ᶠ (m : M), (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R) : MvPolynomial σ R)
have s : Finset M
Tactic: classical
  rw [DirectSum.coeLinearMap_eq_dfinsuppSum, DFinsupp.sum, finsum_eq_sum_of_support_subset]
  apply DirectSum.support_subset
-- 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
w : σ → M
inst_2 : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
rw :
  Eq (α := MvPolynomial σ R)
    (DFinsupp.sum (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x
      fun (x : M) (x_1 : ↥(weightedHomogeneousSubmodule R w x)) ↦ (↑x_1 : MvPolynomial σ R))
    (∑ᶠ (m : M), (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R))
rw₁ :
  Eq (α := MvPolynomial σ R)
    (∑ i ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x,
      (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) i) : MvPolynomial σ R))
    (∑ᶠ (m : M), (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R))
rw₂ :
  Eq (α := MvPolynomial σ R)
    (∑ i ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x,
      (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) i) : MvPolynomial σ R))
    (∑ i ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x,
      (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) i) : MvPolynomial σ R))
s : Finset M
⊢ Eq (α := MvPolynomial σ R)
    ((coeLinearMap fun (i : M) ↦ weightedHomogeneousSubmodule R w i :
          (a : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
        x :
      MvPolynomial σ R)
    (∑ᶠ (m : M), (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R) : MvPolynomial σ R)
have h : (Function.support (M := MvPolynomial σ R) fun (m : M) ↦
    (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)) ⊆
  (↑(DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x) : Set M)
Tactic: classical
  rw [DirectSum.coeLinearMap_eq_dfinsuppSum, DFinsupp.sum, finsum_eq_sum_of_support_subset]
  apply DirectSum.support_subset
-- 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
w : σ → M
inst_2 : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m : M
⊢ (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((coeLinearMap fun (i : M) ↦ weightedHomogeneousSubmodule R w i :
          (a : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
        x) =
    (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)
have rw : ∑ x_1 ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x,
    (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
      (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) x_1) : MvPolynomial σ R) =
  (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)
Tactic: rw [DirectSum.coeLinearMap_eq_dfinsuppSum, DFinsupp.sum, map_sum]
-- 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
w : σ → M
inst_2 : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m : M
⊢ ∑ x_1 ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x,
      (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
        (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) x_1) : MvPolynomial σ R) =
    (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)
have h : (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R) =
  (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
    (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)
Tactic: convert! @Finset.sum_eq_single M (MvPolynomial σ R) _ (DFinsupp.support x) _ m _ _
-- 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
w : σ → M
inst_2 : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m : M
h :
  (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R) =
    (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
      (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)
⊢ ∑ x_1 ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x,
      (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
        (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) x_1) : MvPolynomial σ R) =
    (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)
have convert_2 : ∀ b ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x,
  b ≠ m →
    Eq (α := MvPolynomial σ R)
      ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
          (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) b) : MvPolynomial σ R) :
        MvPolynomial σ R)
      (0 : MvPolynomial σ R)
Tactic: convert! @Finset.sum_eq_single M (MvPolynomial σ R) _ (DFinsupp.support x) _ m _ _
-- 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
w : σ → M
inst_2 : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m : M
h :
  (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R) =
    (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
      (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)
convert_2 :
  ∀ b ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x,
    b ≠ m →
      Eq (α := MvPolynomial σ R)
        ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
            (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) b) : MvPolynomial σ R) :
          MvPolynomial σ R)
        (0 : MvPolynomial σ R)
⊢ ∑ x_1 ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x,
      (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
        (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) x_1) : MvPolynomial σ R) =
    (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)
have convert_3 : m ∉ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x →
  Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
        (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R) :
      MvPolynomial σ R)
    (0 : MvPolynomial σ R)
Tactic: convert! @Finset.sum_eq_single M (MvPolynomial σ R) _ (DFinsupp.support x) _ m _ _
-- 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
w : σ → M
inst_2 : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m : M
⊢ (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R) =
    (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
      (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)
have h : (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R) =
  (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)
Tactic: rw [IsWeightedHomogeneous.weightedHomogeneousComponent_same (x m).prop]
-- 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
w : σ → M
inst_2 : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m : M
⊢ m ∉ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x →
    Eq (α := MvPolynomial σ R)
      ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
          (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R) :
        MvPolynomial σ R)
      (0 : MvPolynomial σ R)
have convert_3 : (x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m = 0 →
  Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
        (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R) :
      MvPolynomial σ R)
    (0 : MvPolynomial σ R)
Tactic: rw [DFinsupp.notMem_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
w : σ → M
inst_2 : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m : M
hm : (x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m = 0
⊢ Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
        (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R) :
      MvPolynomial σ R)
    (0 : MvPolynomial σ R)
have convert_3 : Eq (α := MvPolynomial σ R)
  ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) (↑0 : MvPolynomial σ R)) 0
Tactic: rw [hm, Submodule.coe_zero, map_zero]
-- 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
w : σ → M
inst_2 : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m : M
hm : (x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m = 0
convert_3 :
  Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) (↑0 : MvPolynomial σ R)) 0
⊢ Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
        (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R) :
      MvPolynomial σ R)
    (0 : MvPolynomial σ R)
have convert_3₁ : Eq (α := MvPolynomial σ R) ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) 0) 0
Tactic: rw [hm, Submodule.coe_zero, map_zero]