[GOAL]
α : Type u_1
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : IsAntisymm α r
inst✝ : IsTotal α r
s : Multiset α
a : α
⊢ a ∈ sort r s ↔ a ∈ s
[PROOFSTEP]
rw [← mem_coe, sort_eq]
