-- Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean
theorem decompose'_apply [DecidableEq M] (φ : MvPolynomial σ R) (m : M) :
    (decompose' R w φ m : MvPolynomial σ R) = weightedHomogeneousComponent w m φ

Proof state:
case neg
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
m : M
hm : m ∉ Finset.image (⇑(weight w)) φ.support
⊢ ↑(((DirectSum.mk (fun i => ↥(weightedHomogeneousSubmodule R w i)) (Finset.image (⇑(weight w)) φ.support)) fun m =>
          ⟨(weightedHomogeneousComponent w ↑m) φ, ⋯⟩)
        m) =
    (weightedHomogeneousComponent w m) φ

Tactic:
rw [DirectSum.mk_apply_of_not_mem hm, Submodule.coe_zero,
  weightedHomogeneousComponent_eq_zero_of_not_mem w φ m hm]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
m : M
⊢ ↑(((DirectSum.mk (fun i => ↥(weightedHomogeneousSubmodule R w i)) (Finset.image (⇑(weight w)) φ.support)) fun m =>
          ⟨(weightedHomogeneousComponent w ↑m) φ, ⋯⟩)
        m) =
    (weightedHomogeneousComponent w m) φ

Tactic:
by_cases hm : m ∈ Finset.image (weight w) φ.support

Result:
case pos
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
m : M
hm : m ∈ Finset.image (⇑(weight w)) φ.support
⊢ ↑(((DirectSum.mk (fun i => ↥(weightedHomogeneousSubmodule R w i)) (Finset.image (⇑(weight w)) φ.support)) fun m =>
          ⟨(weightedHomogeneousComponent w ↑m) φ, ⋯⟩)
        m) =
    (weightedHomogeneousComponent w m) φ

case neg
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
m : M
hm : m ∉ Finset.image (⇑(weight w)) φ.support
⊢ ↑(((DirectSum.mk (fun i => ↥(weightedHomogeneousSubmodule R w i)) (Finset.image (⇑(weight w)) φ.support)) fun m =>
          ⟨(weightedHomogeneousComponent w ↑m) φ, ⋯⟩)
        m) =
    (weightedHomogeneousComponent w m) φ

Proof state:
case pos
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
m : M
hm : m ∈ Finset.image (⇑(weight w)) φ.support
⊢ ↑(((DirectSum.mk (fun i => ↥(weightedHomogeneousSubmodule R w i)) (Finset.image (⇑(weight w)) φ.support)) fun m =>
          ⟨(weightedHomogeneousComponent w ↑m) φ, ⋯⟩)
        m) =
    (weightedHomogeneousComponent w m) φ

Tactic:
simp only [DirectSum.mk_apply_of_mem hm, Subtype.coe_mk]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
m : M
⊢ ↑((decompose' R w φ) m) = (weightedHomogeneousComponent w m) φ

Tactic:
rw [decompose']

Result:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
m : M
⊢ ↑(((DirectSum.mk (fun i => ↥(weightedHomogeneousSubmodule R w i)) (Finset.image (⇑(weight w)) φ.support)) fun m =>
          ⟨(weightedHomogeneousComponent w ↑m) φ, ⋯⟩)
        m) =
    (weightedHomogeneousComponent w m) φ