no goals
α : Type u_1
s t : Multiset α
⊢ ∀ (a b : List α),
    Quotient.mk (isSetoid α) a ∈ powerset (Quotient.mk (isSetoid α) b) ↔
      Quotient.mk (isSetoid α) a ≤ Quotient.mk (isSetoid α) b
simp [Subperm, and_comm]