no goals
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
⊢ Function.Embedding.trans (Equiv.toEmbedding (coeEquiv m)) (Function.Embedding.subtype fun x => x ∈ toEnumFinset m) =
    coeEmbedding m
ext <;> rfl