Also a version for `add_submonoid`. Unfortunately the proofs are almost identical, but that's consistent with the surrounding bits of the file anyway.

The key result is a dfinsupp version of the lemma in #8246,
```lean
x ∈ (⨆ i (H : p i), f i) ↔ ∃ v : ι →₀ M, (∀ i, v i ∈ f i) ∧ ∑ i in v.support, v i = x ∧ (∀ i, ¬ p i → v i = 0) :=
```
as
```lean
x ∈ (⨆ i (h : p i), S i) ↔ ∃ f : Π₀ i, S i, dfinsupp.lsum ℕ (λ i, (S i).subtype) (f.filter p) = x
```

Also a version for `add_submonoid`. Unfortunately the proofs are almost identical, but that's consistent with the surrounding bits of the file anyway.

The key result is a dfinsupp version of the lemma in #8246,
```lean
x ∈ (⨆ i (H : p i), f i) ↔ ∃ v : ι →₀ M, (∀ i, v i ∈ f i) ∧ ∑ i in v.support, v i = x ∧ (∀ i, ¬ p i → v i = 0) :=
```
as
```lean
x ∈ (⨆ i (h : p i), S i) ↔ ∃ f : Π₀ i, S i, dfinsupp.lsum ℕ (λ i, (S i).subtype) (f.filter p) = x
```