Theorem: DirectSum.finsupp_sum_support_decompose' (DividedPowers/ForMathlib/GradedRingQuot.lean)

State before:
R : Type u_1
inst✝¹⁰ : CommSemiring R
ι✝ : Type u_2
inst✝⁹ : DecidableEq ι✝
inst✝⁸ : AddCommMonoid ι✝
A : Type u_3
inst✝⁷ : CommSemiring A
inst✝⁶ : DecidableEq A
inst✝⁵ : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
ι : Type u_3
M : Type u_1
σ : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid M
inst✝² : SetLike σ M
inst✝¹ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝ : Decomposition ℳ
inst : (i : ι) → (x : ↥(ℳ i)) → Decidable (x ≠ 0)
r : M
⊢ r = DFinsupp.sum ((decompose ℳ) r) fun i x => ↑x
Tactic:
conv_lhs => rw [← sum_support_decompose ℳ r]
State after:
R : Type u_1
inst✝¹⁰ : CommSemiring R
ι✝ : Type u_2
inst✝⁹ : DecidableEq ι✝
inst✝⁸ : AddCommMonoid ι✝
A : Type u_3
inst✝⁷ : CommSemiring A
inst✝⁶ : DecidableEq A
inst✝⁵ : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
ι : Type u_3
M : Type u_1
σ : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid M
inst✝² : SetLike σ M
inst✝¹ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝ : Decomposition ℳ
inst : (i : ι) → (x : ↥(ℳ i)) → Decidable (x ≠ 0)
r : M
⊢ ∑ i ∈ DFinsupp.support ((decompose ℳ) r), ↑(((decompose ℳ) r) i) = DFinsupp.sum ((decompose ℳ) r) fun i x => ↑x

State before:
R : Type u_1
inst✝¹⁰ : CommSemiring R
ι✝ : Type u_2
inst✝⁹ : DecidableEq ι✝
inst✝⁸ : AddCommMonoid ι✝
A : Type u_3
inst✝⁷ : CommSemiring A
inst✝⁶ : DecidableEq A
inst✝⁵ : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
ι : Type u_3
M : Type u_1
σ : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid M
inst✝² : SetLike σ M
inst✝¹ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝ : Decomposition ℳ
inst : (i : ι) → (x : ↥(ℳ i)) → Decidable (x ≠ 0)
r : M
⊢ ∑ i ∈ DFinsupp.support ((decompose ℳ) r), ↑(((decompose ℳ) r) i) = DFinsupp.sum ((decompose ℳ) r) fun i x => ↑x
Tactic:
rfl
State after:
no goals