-- Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean
theorem weightedHomogeneousComponent_directSum [DecidableEq M]
    (x : DirectSum M fun i : M => ↥(weightedHomogeneousSubmodule R w i)) (m : M) :
    (weightedHomogeneousComponent w m)
      ((DirectSum.coeLinearMap fun i : M => weightedHomogeneousSubmodule R w i) x) = x m

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m : M
⊢ (weightedHomogeneousComponent w m) ((coeLinearMap fun i => weightedHomogeneousSubmodule R w i) x) = ↑(x m)

Tactic:
rw [DirectSum.coeLinearMap_eq_dfinsupp_sum, DFinsupp.sum, map_sum]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m : M
⊢ ∑ x_1 ∈ DFinsupp.support x, (weightedHomogeneousComponent w m) ↑(x x_1) = ↑(x m)

Proof state:
case h.e'_3
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m : M
⊢ ↑(x m) = (weightedHomogeneousComponent w m) ↑(x m)

Tactic:
rw [weightedHomogeneousComponent_of_isWeightedHomogeneous_same (x m).prop]

Result:
no goals

Proof state:
case convert_3
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m : M
hm : x m = 0
⊢ (weightedHomogeneousComponent w m) ↑(x m) = 0

Tactic:
rw [hm, Submodule.coe_zero, map_zero]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m : M
⊢ ∑ x_1 ∈ DFinsupp.support x, (weightedHomogeneousComponent w m) ↑(x x_1) = ↑(x m)

Tactic:
convert @Finset.sum_eq_single M (MvPolynomial σ R) _ (DFinsupp.support x) _ m _ _

Result:
case h.e'_3
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m : M
⊢ ↑(x m) = (weightedHomogeneousComponent w m) ↑(x m)

case convert_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m : M
⊢ ∀ b ∈ DFinsupp.support x, b ≠ m → (weightedHomogeneousComponent w m) ↑(x b) = 0

case convert_3
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m : M
⊢ m ∉ DFinsupp.support x → (weightedHomogeneousComponent w m) ↑(x m) = 0

Proof state:
case convert_3
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m : M
⊢ m ∉ DFinsupp.support x → (weightedHomogeneousComponent w m) ↑(x m) = 0

Tactic:
rw [DFinsupp.not_mem_support_iff]

Result:
case convert_3
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m : M
⊢ x m = 0 → (weightedHomogeneousComponent w m) ↑(x m) = 0

Proof state:
case convert_3
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m : M
⊢ x m = 0 → (weightedHomogeneousComponent w m) ↑(x m) = 0

Tactic:
intro hm

Result:
case convert_3
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m : M
hm : x m = 0
⊢ (weightedHomogeneousComponent w m) ↑(x m) = 0

Proof state:
case convert_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m : M
⊢ ∀ b ∈ DFinsupp.support x, b ≠ m → (weightedHomogeneousComponent w m) ↑(x b) = 0

Tactic:
intro n _ hmn

Result:
case convert_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m n : M
a✝ : n ∈ DFinsupp.support x
hmn : n ≠ m
⊢ (weightedHomogeneousComponent w m) ↑(x n) = 0

Proof state:
case convert_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m n : M
a✝ : n ∈ DFinsupp.support x
hmn : n ≠ m
⊢ (weightedHomogeneousComponent w m) ↑(x n) = 0

Tactic:
rw [weightedHomogeneousComponent_of_isWeightedHomogeneous_ne (x n).prop hmn.symm]

Result:
no goals