α : Type u_1
β : Type ?u.3947
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : IsAntisymm α r
inst✝ : IsTotal α r
s : Finset α
⊢ ↑(sort r s) = ↑(toList s)
α : Type u_1
β : Type ?u.3947
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : IsAntisymm α r
inst✝ : IsTotal α r
s : Finset α
⊢ sort r s ~ toList s
rw [← Multiset.coe_eq_coe]
no goals
α : Type u_1
β : Type ?u.3947
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : IsAntisymm α r
inst✝ : IsTotal α r
s : Finset α
⊢ ↑(sort r s) = ↑(toList s)
simp only [coe_toList, sort_eq]