-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : DecidableEq M
φ : MvPolynomial σ R
conv_rhs :
  (DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w) :
        (a : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
      (decompose' R w φ) =
    φ
conv_rhs₁ conv_rhs₂ :
  Eq (α := MvPolynomial σ R)
    ((DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w) :
          (a : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
        (decompose' R w φ) :
      MvPolynomial σ R)
    (∑ᶠ (m : M), (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
conv_rhs₃ :
  Eq (α := MvPolynomial σ R)
    ((DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w) :
        (a : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
      (∑ i ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) (decompose' R w φ),
        ((DirectSum.of (fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) i :
              ↥(weightedHomogeneousSubmodule R w i) →+
                DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) :
            (a : ↥(weightedHomogeneousSubmodule R w i)) →
              DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i))
          ((decompose' R w φ : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) i)))
    (∑ᶠ (m : M), (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
conv_rhs₄ :
  Eq (α := MvPolynomial σ R)
    (∑ x ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) (decompose' R w φ),
      (↑((decompose' R w φ : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) x) : MvPolynomial σ R))
    (∑
      m ∈
        Finite.toFinset (s :=
          Function.support (M := MvPolynomial σ R) fun (m : M) ↦
            (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
          ⋯,
      (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
conv_rhs₅ :
  DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) (decompose' R w φ) =
    Finite.toFinset (s :=
      Function.support (M := MvPolynomial σ R) fun (m : M) ↦
        (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
      ⋯
h :
  ∀ (m : M),
    m ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) (decompose' R w φ) ↔
      Membership.mem (γ := Finset M)
        (Finite.toFinset (s :=
          Function.support (M := MvPolynomial σ R) fun (m : M) ↦
            (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
          ⋯)
        m
h₁ :
  ∀ (m : M),
    (decompose' R w φ : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m = 0 ↔
      Eq (α := MvPolynomial σ R)
        ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
        (0 : MvPolynomial σ R)
h₂ :
  ∀ (m : M),
    (↑((decompose' R w φ : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R) =
        (↑0 : MvPolynomial σ R) ↔
      Eq (α := MvPolynomial σ R)
        ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
        (0 : MvPolynomial σ R)
⊢ (DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w) :
        (a : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
      (decompose' R w φ) =
    φ

Tactic:
classical
    conv_rhs => rw [← sum_weightedHomogeneousComponent w φ]
    rw [← DirectSum.sum_support_of (decompose' R w φ)]
    simp only [DirectSum.coeAddMonoidHom_of, map_sum,
      finsum_eq_sum _ (weightedHomogeneousComponent_finsupp φ)]
    apply Finset.sum_congr _ (fun m _ ↦ by rw [decompose'_apply])
    ext m
    simp only [DFinsupp.mem_support_toFun, ne_eq, Set.Finite.mem_toFinset, Function.mem_support,
      not_iff_not]
    conv_lhs => rw [← Subtype.coe_inj]
    rw [decompose'_apply, Submodule.coe_zero]

Premises used: not_iff_not, DFinsupp.mem_support_toFun, Set.Finite.mem_toFinset, finsum_eq_sum, Subtype.coe_inj, MvPolynomial.sum_weightedHomogeneousComponent, MvPolynomial.decompose'_apply, map_sum, ne_eq, Submodule.coe_zero, DirectSum.coeAddMonoidHom_of, MvPolynomial.weightedHomogeneousComponent_finsupp, Function.mem_support, Finset.sum_congr