no goals
α : Type u_1
β : Type ?u.452644
γ : Type ?u.452647
inst✝ : DecidableEq α
s t : Multiset α
⊢ toFinset s ⊆ toFinset t ↔ s ⊆ t
simp only [Finset.subset_iff, Multiset.subset_iff, Multiset.mem_toFinset]