-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
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
rw :
  (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → 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)) =
    (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)
rw₁ :
  (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
      (∑ i ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x,
        (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) i) : MvPolynomial σ R)) =
    (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)
rw₂ rw₃ 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)
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)
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)
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)
convert_3₁ 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)
⊢ (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)

Tactic:
classical
  rw [DirectSum.coeLinearMap_eq_dfinsuppSum, DFinsupp.sum, map_sum]
  convert! @Finset.sum_eq_single M (MvPolynomial σ R) _ (DFinsupp.support x) _ m _ _
  · rw [IsWeightedHomogeneous.weightedHomogeneousComponent_same (x m).prop]
  · intro n _ hmn
    exact IsWeightedHomogeneous.weightedHomogeneousComponent_ne m (x n).prop hmn.symm
  · rw [DFinsupp.notMem_support_iff]
    intro hm; rw [hm, Submodule.coe_zero, map_zero]

Premises used: MvPolynomial.DirectSum.coeLinearMap_eq_dfinsuppSum, MvPolynomial.IsWeightedHomogeneous.weightedHomogeneousComponent_same, DFinsupp.notMem_support_iff, map_zero, DFinsupp.sum, map_sum, Submodule.coe_zero, Subtype.prop, DFunLike.coe