-- 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
m : M
pos :
  ∀ (hm : Membership.mem (γ := Finset M) (Finset.image (⇑(weight w) : (a : σ →₀ ℕ) → M) φ.support) m),
    (↑((((DirectSum.mk (fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i))
                      (Finset.image (⇑(weight w) : (a : σ →₀ ℕ) → M) φ.support) :
                    ((i : (↑(↑(Finset.image (⇑(weight w) : (a : σ →₀ ℕ) → M) φ.support) : Set M) : Type u_2)) →
                        ↥(weightedHomogeneousSubmodule R w (↑i : M))) →+
                      DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) :
                  (a :
                      (i : (↑(↑(Finset.image (⇑(weight w) : (a : σ →₀ ℕ) → M) φ.support) : Set M) : Type u_2)) →
                        ↥(weightedHomogeneousSubmodule R w (↑i : M))) →
                    DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i))
                fun (m : (↑(↑(Finset.image (⇑(weight w) : (a : σ →₀ ℕ) → M) φ.support) : Set M) : Type u_2)) ↦
                Subtype.mk (p := fun (x : MvPolynomial σ R) ↦
                  Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w (↑m : M)) x)
                  ((weightedHomogeneousComponent w (↑m : M) : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) ⋯ :
              (a : M) → ↥(weightedHomogeneousSubmodule R w a))
            m) :
        MvPolynomial σ R) =
      (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ
neg :
  ∀ (hm : m ∉ Finset.image (⇑(weight w) : (a : σ →₀ ℕ) → M) φ.support),
    (↑((((DirectSum.mk (fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i))
                      (Finset.image (⇑(weight w) : (a : σ →₀ ℕ) → M) φ.support) :
                    ((i : (↑(↑(Finset.image (⇑(weight w) : (a : σ →₀ ℕ) → M) φ.support) : Set M) : Type u_2)) →
                        ↥(weightedHomogeneousSubmodule R w (↑i : M))) →+
                      DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) :
                  (a :
                      (i : (↑(↑(Finset.image (⇑(weight w) : (a : σ →₀ ℕ) → M) φ.support) : Set M) : Type u_2)) →
                        ↥(weightedHomogeneousSubmodule R w (↑i : M))) →
                    DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i))
                fun (m : (↑(↑(Finset.image (⇑(weight w) : (a : σ →₀ ℕ) → M) φ.support) : Set M) : Type u_2)) ↦
                Subtype.mk (p := fun (x : MvPolynomial σ R) ↦
                  Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w (↑m : M)) x)
                  ((weightedHomogeneousComponent w (↑m : M) : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) ⋯ :
              (a : M) → ↥(weightedHomogeneousSubmodule R w a))
            m) :
        MvPolynomial σ R) =
      (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ
⊢ (↑((((DirectSum.mk (fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i))
                    (Finset.image (⇑(weight w) : (a : σ →₀ ℕ) → M) φ.support) :
                  ((i : (↑(↑(Finset.image (⇑(weight w) : (a : σ →₀ ℕ) → M) φ.support) : Set M) : Type u_2)) →
                      ↥(weightedHomogeneousSubmodule R w (↑i : M))) →+
                    DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) :
                (a :
                    (i : (↑(↑(Finset.image (⇑(weight w) : (a : σ →₀ ℕ) → M) φ.support) : Set M) : Type u_2)) →
                      ↥(weightedHomogeneousSubmodule R w (↑i : M))) →
                  DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i))
              fun (m : (↑(↑(Finset.image (⇑(weight w) : (a : σ →₀ ℕ) → M) φ.support) : Set M) : Type u_2)) ↦
              Subtype.mk (p := fun (x : MvPolynomial σ R) ↦
                Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w (↑m : M)) x)
                ((weightedHomogeneousComponent w (↑m : M) : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) ⋯ :
            (a : M) → ↥(weightedHomogeneousSubmodule R w a))
          m) :
      MvPolynomial σ R) =
    (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ

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

Premises used: Finsupp.weight, MvPolynomial.support, DFunLike.coe, Finset.image