no goals
ι : Type u_2
M : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Zero M
s : Multiset (ι →₀ M)
x : ι
x✝ : List (ι →₀ M)
⊢ x ∈ sup (map Finsupp.support (Quot.mk Setoid.r x✝)) ↔ ∃ f x_1, x ∈ f.support
simpa only [Multiset.quot_mk_to_coe'', Multiset.coe_map, Multiset.sup_coe, List.foldr_map]
using List.mem_foldr_sup_support_iff