ι : Type u_3
R : Type ?u.193623
M : Type u_1
σ : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid M
inst✝³ : SetLike σ M
inst✝² : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝¹ : Decomposition ℳ
inst✝ : (i : ι) → (x : { x // x ∈ ℳ i }) → Decidable (x ≠ 0)
r : M
⊢ ∑ i in Dfinsupp.support (↑(decompose ℳ) r), ↑(↑(↑(decompose ℳ) r) i) =
    ↑(decompose ℳ).symm
      (∑ i in Dfinsupp.support (↑(decompose ℳ) r), ↑(of (fun i => { x // x ∈ ℳ i }) i) (↑(↑(decompose ℳ) r) i))
ι : Type u_3
R : Type ?u.193623
M : Type u_1
σ : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid M
inst✝³ : SetLike σ M
inst✝² : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝¹ : Decomposition ℳ
inst✝ : (i : ι) → (x : { x // x ∈ ℳ i }) → Decidable (x ≠ 0)
r : M
⊢ ∑ i in Dfinsupp.support (↑(decompose ℳ) r), ↑(↑(↑(decompose ℳ) r) i) = r
conv_rhs =>
  rw [← (decompose ℳ).symm_apply_apply r, ← sum_support_of (fun i ↦ ℳ i) (decompose ℳ r)]
ι : Type u_3
R : Type ?u.193623
M : Type u_1
σ : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid M
inst✝³ : SetLike σ M
inst✝² : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝¹ : Decomposition ℳ
inst✝ : (i : ι) → (x : { x // x ∈ ℳ i }) → Decidable (x ≠ 0)
r : M
⊢ ∑ i in Dfinsupp.support (↑(decompose ℳ) r), ↑(↑(↑(decompose ℳ) r) i) =
    ∑ i in Dfinsupp.support (↑(decompose ℳ) r),
      ↑(decompose ℳ).symm (↑(of (fun i => { x // x ∈ ℳ i }) i) (↑(↑(decompose ℳ) r) i))
ι : Type u_3
R : Type ?u.193623
M : Type u_1
σ : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid M
inst✝³ : SetLike σ M
inst✝² : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝¹ : Decomposition ℳ
inst✝ : (i : ι) → (x : { x // x ∈ ℳ i }) → Decidable (x ≠ 0)
r : M
⊢ ∑ i in Dfinsupp.support (↑(decompose ℳ) r), ↑(↑(↑(decompose ℳ) r) i) =
    ↑(decompose ℳ).symm
      (∑ i in Dfinsupp.support (↑(decompose ℳ) r), ↑(of (fun i => { x // x ∈ ℳ i }) i) (↑(↑(decompose ℳ) r) i))
rw [decompose_symm_sum]
no goals
ι : Type u_3
R : Type ?u.193623
M : Type u_1
σ : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid M
inst✝³ : SetLike σ M
inst✝² : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝¹ : Decomposition ℳ
inst✝ : (i : ι) → (x : { x // x ∈ ℳ i }) → Decidable (x ≠ 0)
r : M
⊢ ∑ i in Dfinsupp.support (↑(decompose ℳ) r), ↑(↑(↑(decompose ℳ) r) i) =
    ∑ i in Dfinsupp.support (↑(decompose ℳ) r),
      ↑(decompose ℳ).symm (↑(of (fun i => { x // x ∈ ℳ i }) i) (↑(↑(decompose ℳ) r) i))
simp_rw [decompose_symm_of]