-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
rw rw₁ rw₂ :
  ∑
      i ∈
        Finite.toFinset (s :=
          Function.support (M := MvPolynomial σ R) fun (m : M) ↦
            (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
          ⋯,
      (weightedHomogeneousComponent w i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ =
    φ
a :
  ∀ (d : σ →₀ ℕ),
    coeff d
        (∑
          i ∈
            Finite.toFinset (s :=
              Function.support (M := MvPolynomial σ R) fun (m : M) ↦
                (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
              ⋯,
          (weightedHomogeneousComponent w i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) =
      coeff d φ
a₁ :
  ∀ (d : σ →₀ ℕ),
    (∑
        x ∈
          Finite.toFinset (s :=
            Function.support (M := MvPolynomial σ R) fun (m : M) ↦
              (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
            ⋯,
        if (weight w : (a : σ →₀ ℕ) → M) d = x then coeff d φ else 0) =
      coeff d φ
a₂ :
  ∀ (d : σ →₀ ℕ),
    (if Eq.{u_2 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) d : M) ((weight w : (a : σ →₀ ℕ) → M) d : M) then coeff d φ
      else 0) =
      coeff d φ
a₃ :
  ∀ (d : σ →₀ ℕ) (b : M),
    Membership.mem (γ := Finset M)
        (Finite.toFinset (s :=
          Function.support (M := MvPolynomial σ R) fun (m : M) ↦
            (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
          ⋯)
        b →
      b ≠ (weight w : (a : σ →₀ ℕ) → M) d → (if (weight w : (a : σ →₀ ℕ) → M) d = b then coeff d φ else 0) = 0
a₄ :
  ∀ (d : σ →₀ ℕ),
    ((weight w : (a : σ →₀ ℕ) → M) d : M) ∉
        Finite.toFinset (s :=
          Function.support (M := MvPolynomial σ R) fun (m : M) ↦
            (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
          ⋯ →
      (if Eq.{u_2 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) d : M) ((weight w : (a : σ →₀ ℕ) → M) d : M) then
          coeff d φ
        else 0) =
        0
a₅ :
  ∀ (d : σ →₀ ℕ) (b : M),
    Membership.mem (γ := Finset M)
        (Finite.toFinset (s :=
          Function.support (M := MvPolynomial σ R) fun (m : M) ↦
            (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
          ⋯)
        b →
      b ≠ (weight w : (a : σ →₀ ℕ) → M) d → (if (weight w : (a : σ →₀ ℕ) → M) d = b then coeff d φ else 0) = 0
a₆ a₇ :
  ∀ (d : σ →₀ ℕ),
    ((weight w : (a : σ →₀ ℕ) → M) d : M) ∉
        Finite.toFinset (s :=
          Function.support (M := MvPolynomial σ R) fun (m : M) ↦
            (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
          ⋯ →
      (if Eq.{u_2 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) d : M) ((weight w : (a : σ →₀ ℕ) → M) d : M) then
          coeff d φ
        else 0) =
        0
⊢ ∑ᶠ (m : M), (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ = φ

Tactic:
classical
  rw [finsum_eq_sum _ (weightedHomogeneousComponent_finsupp φ)]
  ext1 d
  simp only [coeff_sum, coeff_weightedHomogeneousComponent]
  rw [Finset.sum_eq_single (weight w d)]
  · rw [if_pos rfl]
  · intro m _ hm'
    rw [if_neg hm'.symm]
  · intro hm
    rw [if_pos rfl]
    simp only [Finite.mem_toFinset, mem_support, Ne, Classical.not_not] at hm
    have := coeff_weightedHomogeneousComponent (w := w) (weight w d) φ d
    rw [hm, if_pos rfl, coeff_zero] at this
    exact this.symm

Premises used: Classical.not_not, Set.Finite.mem_toFinset, finsum_eq_sum, Ne, if_pos, MvPolynomial.weightedHomogeneousComponent_finsupp, MvPolynomial.coeff_zero, Function.mem_support, MvPolynomial.coeff_weightedHomogeneousComponent, rfl, MvPolynomial.coeff_sum