chore: modify signature of lemmas about mergeSort

src/Init/Data/List/Sort/Lemmas.lean

@@ -114,14 +114,15 @@ theorem enumLE_trans (trans : ∀ a b c, le a b → le b c → le a c)
   · simp_all
   · simp_all
 
-theorem enumLE_total (total : ∀ a b, !le a b → le b a)
-    (a b : Nat × α) : !enumLE le a b → enumLE le b a := by
+theorem enumLE_total (total : ∀ a b, le a b || le b a)
+    (a b : Nat × α) : enumLE le a b || enumLE le b a := by
   simp only [enumLE]
   split <;> split
-  · simpa using Nat.le_of_lt
+  · simpa using Nat.le_total a.fst b.fst
   · simp
   · simp
-  · simp_all [total a.2 b.2]
+  · have := total a.2 b.2
+    simp_all
 
 /-! ### merge -/
 
@@ -162,12 +163,12 @@ theorem mem_merge {a : α} {xs ys : List α} : a ∈ merge xs ys le ↔ a ∈ xs
 attribute [local instance] boolRelToRel
 
 /--
-If the ordering relation `le` is transitive and total (i.e. `le a b ∨ le b a` for all `a, b`)
+If the ordering relation `le` is transitive and total (i.e. `le a b || le b a` for all `a, b`)
 then the `merge` of two sorted lists is sorted.
 -/
 theorem sorted_merge
     (trans : ∀ (a b c : α), le a b → le b c → le a c)
-    (total : ∀ (a b : α), !le a b → le b a)
+    (total : ∀ (a b : α), le a b || le b a)
     (l₁ l₂ : List α) (h₁ : l₁.Pairwise le) (h₂ : l₂.Pairwise le) : (merge l₁ l₂ le).Pairwise le := by
   induction l₁ generalizing l₂ with
   | nil => simpa only [merge]
@@ -188,9 +189,10 @@ theorem sorted_merge
       · apply Pairwise.cons
         · intro z m
           rw [mem_merge, mem_cons] at m
+          simp only [Bool.not_eq_true] at h
           rcases m with (⟨rfl|m⟩|m)
-          · exact total _ _ (by simpa using h)
-          · exact trans _ _ _ (total _ _ (by simpa using h)) (rel_of_pairwise_cons h₁ m)
+          · simpa [h] using total y z
+          · exact trans _ _ _ (by simpa [h] using total x y) (rel_of_pairwise_cons h₁ m)
           · exact rel_of_pairwise_cons h₂ m
         · exact ih₂ h₂.tail
 
@@ -243,13 +245,13 @@ termination_by l => l.length
 /--
 The result of `mergeSort` is sorted,
 as long as the comparison function is transitive (`le a b → le b c → le a c`)
-and total in the sense that `le a b ∨ le b a`.
+and total in the sense that `le a b || le b a`.
 
 The comparison function need not be irreflexive, i.e. `le a b` and `le b a` is allowed even when `a ≠ b`.
 -/
 theorem sorted_mergeSort
     (trans : ∀ (a b c : α), le a b → le b c → le a c)
-    (total : ∀ (a b : α), !le a b → le b a) :
+    (total : ∀ (a b : α), le a b || le b a) :
     (l : List α) → (mergeSort l le).Pairwise le
   | [] => by simp [mergeSort]
   | [a] => by simp [mergeSort]
@@ -317,7 +319,7 @@ termination_by _ l => l.length
 
 theorem mergeSort_cons {le : α → α → Bool}
     (trans : ∀ (a b c : α), le a b → le b c → le a c)
-    (total : ∀ (a b : α), !le a b → le b a)
+    (total : ∀ (a b : α), le a b || le b a)
     (a : α) (l : List α) :
     ∃ l₁ l₂, mergeSort (a :: l) le = l₁ ++ a :: l₂ ∧ mergeSort l le = l₁ ++ l₂ ∧
       ∀ b, b ∈ l₁ → !le a b := by
@@ -376,7 +378,7 @@ then `c` is still a sublist of `mergeSort le l`.
 -/
 theorem sublist_mergeSort
     (trans : ∀ (a b c : α), le a b → le b c → le a c)
-    (total : ∀ (a b : α), !le a b → le b a) :
+    (total : ∀ (a b : α), le a b || le b a) :
     ∀ {c : List α} (_ : c.Pairwise le) (_ : c <+ l),
     c <+ mergeSort l le
   | _, _, .slnil => nil_sublist _
@@ -407,7 +409,7 @@ then `[a, b]` is still a sublist of `mergeSort le l`.
 -/
 theorem pair_sublist_mergeSort
     (trans : ∀ (a b c : α), le a b → le b c → le a c)
-    (total : ∀ (a b : α), !le a b → le b a)
+    (total : ∀ (a b : α), le a b || le b a)
     (hab : le a b) (h : [a, b] <+ l) : [a, b] <+ mergeSort l le :=
   sublist_mergeSort trans total (pairwise_pair.mpr hab) h