Theorem: MvPolynomial.DirectSum.coeLinearMap_eq_finsum (DividedPowers/ForMathlib/WeightedHomogeneous.lean)

State before:
R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
σ : Type u_1
inst✝³ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : DirectSum M fun i => ↥(weightedHomogeneousSubmodule R w i)
⊢ (DirectSum.coeLinearMap fun i => weightedHomogeneousSubmodule R w i) x = ∑ᶠ (m : M), ↑(x m)
Tactic:
rw [DirectSum.coeLinearMap_eq_support_sum, DFinsupp.sum]
State after:
R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
σ : Type u_1
inst✝³ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : DirectSum M fun i => ↥(weightedHomogeneousSubmodule R w i)
⊢ ∑ i ∈ DFinsupp.support x, ↑(x i) = ∑ᶠ (m : M), ↑(x m)

State before:
R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
σ : Type u_1
inst✝³ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : DirectSum M fun i => ↥(weightedHomogeneousSubmodule R w i)
⊢ ∑ i ∈ DFinsupp.support x, ↑(x i) = ∑ᶠ (m : M), ↑(x m)
Tactic:
rw [finsum_eq_sum_of_support_subset]
State after:
case h
R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
σ : Type u_1
inst✝³ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : DirectSum M fun i => ↥(weightedHomogeneousSubmodule R w i)
⊢ (Function.support fun m => ↑(x m)) ⊆ ↑(DFinsupp.support x)

State before:
case h
R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
σ : Type u_1
inst✝³ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : DirectSum M fun i => ↥(weightedHomogeneousSubmodule R w i)
⊢ (Function.support fun m => ↑(x m)) ⊆ ↑(DFinsupp.support x)
Tactic:
apply DirectSum.support_subset_submodule
State after:
no goals