Theorem: MvPolynomial.decomposition.decompose'_eq (DividedPowers/ForMathlib/Homogeneous.lean)

State before:
σ : Type u_1
τ : Type ?u.73574
R : Type u_2
inst✝² : CommSemiring R
S : Type ?u.73583
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq R
⊢ DirectSum.Decomposition.decompose' = fun φ =>
    (DirectSum.mk (fun i => ↥(homogeneousSubmodule σ R i)) (Finset.image (⇑degree) φ.support)) fun m =>
      ⟨(homogeneousComponent ↑m) φ, ⋯⟩
Tactic:
rfl
State after:
no goals