use List.mergeSort instead of hand-made insertionSort

Src/Problem28A.lean

@@ -3,26 +3,12 @@
 -/
 variable {α : Type}
 
-def orderedInsert (a : α) (ord : α → Nat) : List α → List α
-  | [] => [a]
-  | b :: l =>
-    if ord a ≤ ord b then a :: b :: l
-    else b :: orderedInsert a ord l
-
-/-- insertion sort -/
-def insertionSort (ord : α → Nat) : List α → List α
-  | [] => []
-  | b :: l => orderedInsert b ord <| insertionSort ord l
-
-#guard insertionSort (fun x => x) [3, 1, 4, 1, 5, 9, 2, 6, 5, 3, 5]
-  = [1, 1, 2, 3, 3, 4, 5, 5, 5, 6, 9]
-
 -- You can use this!
-#check insertionSort
+#check List.mergeSort
 
 def lsort (l : List (List α)) : List (List α) :=
   -- sorry
-  insertionSort (fun l => l.length) l
+  List.mergeSort l (fun l₁ l₂ => l₁.length ≤ l₂.length)
   -- sorry
 
 -- The following codes are for test and you should not edit these.

Src/Problem28B.lean

@@ -4,21 +4,8 @@
 -/
 variable {α : Type}
 
-/-- Insert an element in a way that
-does not break the order of the sorted list. -/
-def orderedInsert (a : α) (ord : α → Nat) : List α → List α
-  | [] => [a]
-  | b :: l =>
-    if ord a ≤ ord b then a :: b :: l
-    else b :: orderedInsert a ord l
-
-/-- insertion sort -/
-def insertionSort (ord : α → Nat) : List α → List α
-  | [] => []
-  | b :: l => orderedInsert b ord <| insertionSort ord l
-
 -- You can use this!
-#check insertionSort
+#check List.mergeSort
 --#--
 /-- Count the number of lists in list `l` that have the same length as `target` -/
 def makeToLengthFreq (l : List (List α)) (target : List α) : Nat :=
@@ -28,7 +15,7 @@ def makeToLengthFreq (l : List (List α)) (target : List α) : Nat :=
 
 def lfsort (l : List (List α)) : List (List α) :=
   -- sorry
-  insertionSort (makeToLengthFreq l) l
+  List.mergeSort l (fun t s => makeToLengthFreq l t ≤ makeToLengthFreq l s)
   -- sorry
 
 -- The following codes are for test and you should not edit these.