no goals
ι : Type u_3
R : Type ?u.121042
M : Type u_1
σ : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid M
inst✝² : SetLike σ M
inst✝¹ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝ : Decomposition ℳ
x : M
i : ι
hx : x ∈ ℳ i
⊢ ↑(↑(↑(decompose ℳ) x) i) = x
rw [decompose_of_mem _ hx, DirectSum.of_eq_same, Subtype.coe_mk]