∀ (R : Type u_2) {M : Type u_1} [inst : CommSemiring R] {σ : Type u_3} (w : σ → M) [inst_1 : AddCommMonoid M]
  [inst_2 : DecidableEq M] (x : DirectSum M fun i => ↥(MvPolynomial.weightedHomogeneousSubmodule R w i)),
  MvPolynomial.decompose' R w ((DirectSum.coeAddMonoidHom (MvPolynomial.weightedHomogeneousSubmodule R w)) x) = x