Theorem: MvPolynomial.weightedHomogeneousComponent_weightedHomogeneousPolynomial' (DividedPowers/ForMathlib/WeightedHomogeneous.lean)

State before:
R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
σ : Type u_1
inst✝³ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
m : M
x : ↥(weightedHomogeneousSubmodule R w m)
⊢ (weightedHomogeneousComponent w m) ↑x = ↑x
Tactic:
rw [weightedHomogeneousComponent_weighted_homogeneous_polynomial m m _ x.prop,
  if_pos rfl]
State after:
no goals