chore: move implementation details of into namespace

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

@@ -40,12 +40,15 @@ def merge (xs ys : List α) (le : α → α → Bool := by exact fun a b => a
 
 /--
 Split a list in two equal parts. If the length is odd, the first part will be one element longer.
+
+This is an implementation detail of `mergeSort`.
 -/
-def splitInTwo (l : { l : List α // l.length = n }) :
+def MergeSort.Internal.splitInTwo (l : { l : List α // l.length = n }) :
     { l : List α // l.length = (n+1)/2 } × { l : List α // l.length = n/2 } :=
   let r := splitAt ((n+1)/2) l.1
   (⟨r.1, by simp [r, splitAt_eq, l.2]; omega⟩, ⟨r.2, by simp [r, splitAt_eq, l.2]; omega⟩)
 
+open MergeSort.Internal in
 set_option linter.unusedVariables false in
 /--
 Simplified implementation of stable merge sort.

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

@@ -25,6 +25,8 @@ namespace List
 
 /-! ### splitInTwo -/
 
+namespace MergeSort.Internal
+
 @[simp] theorem splitInTwo_fst (l : { l : List α // l.length = n }) :
     (splitInTwo l).1 = ⟨l.1.take ((n+1)/2), by simp [splitInTwo, splitAt_eq, l.2]; omega⟩ := by
   simp [splitInTwo, splitAt_eq]
@@ -82,6 +84,10 @@ theorem splitInTwo_fst_le_splitInTwo_snd {l : { l : List α // l.length = n }} (
   intro a b ma mb
   exact h.rel_of_mem_take_of_mem_drop ma mb
 
+end MergeSort.Internal
+
+open MergeSort.Internal
+
 /-! ### enumLE -/
 
 variable {le : α → α → Bool}