chore(*): bundle typeclasses

src/data/finset/sort.lean

@@ -22,8 +22,7 @@ variables {α β : Type*}
 
 /-! ### sort -/
 section sort
-variables (r : α → α → Prop) [decidable_rel r]
-  [is_trans α r] [is_antisymm α r] [is_total α r]
+variables (r : α → α → Prop) [decidable_rel r] [is_linear_order α r]
 
 /-- `sort s` constructs a sorted list from the unordered set `s`.
   (Uses merge sort algorithm.) -/

src/data/list/sort.lean

@@ -195,8 +195,8 @@ lemma sorted.insertion_sort_eq : ∀ {l : list α} (h : sorted r l), insertion_s
     exacts [rel_of_sorted_cons h _ (or.inl rfl), h.tail]
   end
 
-section total_and_transitive
-variables [is_total α r] [is_trans α r]
+section total_preorder
+variables [is_total_preorder α r]
 
 theorem sorted.ordered_insert (a : α) : ∀ l, sorted r l → sorted r (ordered_insert r a l)
 | []       h := sorted_singleton a
@@ -219,7 +219,7 @@ theorem sorted_insertion_sort : ∀ l, sorted r (insertion_sort r l)
 | []       := sorted_nil
 | (a :: l) := (sorted_insertion_sort l).ordered_insert a _
 
-end total_and_transitive
+end total_preorder
 end correctness
 end insertion_sort
 
@@ -331,8 +331,8 @@ using_well_founded
 @[simp] lemma length_merge_sort (l : list α) : (merge_sort r l).length = l.length :=
 (perm_merge_sort r _).length_eq
 
-section total_and_transitive
-variables {r} [is_total α r] [is_trans α r]
+section total_preorder
+variables {r} [is_total_preorder α r]
 
 theorem sorted.merge : ∀ {l l' : list α}, sorted r l → sorted r l' → sorted r (merge r l l')
 | []       []        h₁ h₂ := by simp [merge]
@@ -382,7 +382,7 @@ theorem merge_sort_eq_insertion_sort [is_antisymm α r] (l : list α) :
 eq_of_perm_of_sorted ((perm_merge_sort r l).trans (perm_insertion_sort r l).symm)
   (sorted_merge_sort r l) (sorted_insertion_sort r l)
 
-end total_and_transitive
+end total_preorder
 end correctness
 
 @[simp] theorem merge_sort_nil : [].merge_sort r = [] :=

src/data/multiset/sort.lean

@@ -17,9 +17,11 @@ namespace multiset
 open list
 variables {α : Type*}
 
+-- TODO: move to core.
+instance (r : α → α → Prop) [is_linear_order α r] : is_total_preorder α r := { }
+
 section sort
-variables (r : α → α → Prop) [decidable_rel r]
-  [is_trans α r] [is_antisymm α r] [is_total α r]
+variables (r : α → α → Prop) [decidable_rel r] [is_linear_order α r]
 
 /-- `sort s` constructs a sorted list from the multiset `s`.
   (Uses merge sort algorithm.) -/

src/logic/equiv/list.lean

@@ -72,19 +72,15 @@ end list
 section finset
 variables [encodable α]
 
-private def enle : α → α → Prop := encode ⁻¹'o (≤)
-
-private lemma enle.is_linear_order : is_linear_order α enle :=
+instance is_linear_order_enle : is_linear_order α (encode ⁻¹'o (≤)) :=
 (rel_embedding.preimage ⟨encode, encode_injective⟩ (≤)).is_linear_order
 
-private def decidable_enle (a b : α) : decidable (enle a b) :=
-by unfold enle order.preimage; apply_instance
-
-local attribute [instance] enle.is_linear_order decidable_enle
+instance decidable_enle (a b : α) : decidable ((encode ⁻¹'o (≤)) a b) :=
+by unfold order.preimage; apply_instance
 
 /-- Explicit encoding function for `multiset α` -/
 def encode_multiset (s : multiset α) : ℕ :=
-encode (s.sort enle)
+encode (s.sort (encode ⁻¹'o (≤)))
 
 /-- Explicit decoding function for `multiset α` -/
 def decode_multiset (n : ℕ) : option (multiset α) :=
@@ -162,7 +158,7 @@ def fintype_pi (α : Type*) (π : α → Type*) [decidable_eq α] [fintype α] [
 
 /-- The elements of a `fintype` as a sorted list. -/
 def sorted_univ (α) [fintype α] [encodable α] : list α :=
-finset.univ.sort (encodable.encode' α ⁻¹'o (≤))
+@finset.sort _ (encodable.encode' α ⁻¹'o (≤)) _ encodable.is_linear_order_enle finset.univ
 
 @[simp] theorem mem_sorted_univ {α} [fintype α] [encodable α] (x : α) : x ∈ sorted_univ α :=
 (finset.mem_sort _).2 (finset.mem_univ _)

src/order/well_founded_set.lean

@@ -633,7 +633,7 @@ end
   partially well-ordered on a set `s`, the relation `list.sublist_forall₂ r` is partially
   well-ordered on the set of lists of elements of `s`. That relation is defined so that
   `list.sublist_forall₂ r l₁ l₂` whenever `l₁` related pointwise by `r` to a sublist of `l₂`.  -/
-lemma partially_well_ordered_on_sublist_forall₂ (r : α → α → Prop) [is_refl α r] [is_trans α r]
+lemma partially_well_ordered_on_sublist_forall₂ (r : α → α → Prop) [is_preorder α r]
   {s : set α} (h : s.partially_well_ordered_on r) :
   { l : list α | ∀ x, x ∈ l → x ∈ s }.partially_well_ordered_on (list.sublist_forall₂ r) :=
 begin