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

State before:
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
m : M
⊢ ↑((MvPolynomial.decompose'_toFun R w φ) m) = (weightedHomogeneousComponent w m) φ
Tactic:
rw [decompose'_toFun]
State after:
R : Type u_2
M : Type u_1
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 (⇑(weightedDegree w)) φ.support))
          fun m => ⟨(weightedHomogeneousComponent w ↑m) φ, ⋯⟩)
        m) =
    (weightedHomogeneousComponent w m) φ

State before:
R : Type u_2
M : Type u_1
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 (⇑(weightedDegree w)) φ.support))
          fun m => ⟨(weightedHomogeneousComponent w ↑m) φ, ⋯⟩)
        m) =
    (weightedHomogeneousComponent w m) φ
Tactic:
by_cases hm : m ∈ Finset.image (weightedDegree w) φ.support
State after:
case pos
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
m : M
hm : m ∈ Finset.image (⇑(weightedDegree w)) φ.support
⊢ ↑(((DirectSum.mk (fun i => ↥(weightedHomogeneousSubmodule R w i)) (Finset.image (⇑(weightedDegree w)) φ.support))
          fun m => ⟨(weightedHomogeneousComponent w ↑m) φ, ⋯⟩)
        m) =
    (weightedHomogeneousComponent w m) φ

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

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

case neg
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
m : M
hm : m ∉ Finset.image (⇑(weightedDegree w)) φ.support
⊢ ↑(((DirectSum.mk (fun i => ↥(weightedHomogeneousSubmodule R w i)) (Finset.image (⇑(weightedDegree w)) φ.support))
          fun m => ⟨(weightedHomogeneousComponent w ↑m) φ, ⋯⟩)
        m) =
    (weightedHomogeneousComponent w m) φ
Tactic:
simp only [DirectSum.mk_apply_of_mem hm, Subtype.coe_mk]
State after:
case neg
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
m : M
hm : m ∉ Finset.image (⇑(weightedDegree w)) φ.support
⊢ ↑(((DirectSum.mk (fun i => ↥(weightedHomogeneousSubmodule R w i)) (Finset.image (⇑(weightedDegree w)) φ.support))
          fun m => ⟨(weightedHomogeneousComponent w ↑m) φ, ⋯⟩)
        m) =
    (weightedHomogeneousComponent w m) φ

State before:
case neg
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
m : M
hm : m ∉ Finset.image (⇑(weightedDegree w)) φ.support
⊢ ↑(((DirectSum.mk (fun i => ↥(weightedHomogeneousSubmodule R w i)) (Finset.image (⇑(weightedDegree w)) φ.support))
          fun m => ⟨(weightedHomogeneousComponent w ↑m) φ, ⋯⟩)
        m) =
    (weightedHomogeneousComponent w m) φ
Tactic:
rw [DirectSum.mk_apply_of_not_mem hm, Submodule.coe_zero, decompose'_aux w φ m hm]
State after:
no goals