chore: upstream some List.Perm lemmas (#6524)

This PR upstreams some remaining `List.Perm` lemmas from Batteries.

src/Init/Data/List/Perm.lean

@@ -510,4 +510,18 @@ theorem Perm.eraseP (f : α → Bool) {l₁ l₂ : List α}
     refine (IH₁ H).trans (IH₂ ((p₁.pairwise_iff ?_).1 H))
     exact fun h h₁ h₂ => h h₂ h₁
 
+theorem perm_insertIdx [DecidableEq α] {α} (x : α) (l : List α) {n} (h : n ≤ l.length) :
+    insertIdx n x l ~ x :: l := by
+  induction l generalizing n with
+  | nil =>
+    cases n with
+    | zero => rfl
+    | succ => cases h
+  | cons _ _ ih =>
+    cases n with
+    | zero => simp [insertIdx]
+    | succ =>
+      simp only [insertIdx, modifyTailIdx]
+      refine .trans (.cons _ (ih (Nat.le_of_succ_le_succ h))) (.swap ..)
+
 end List

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

@@ -253,6 +253,10 @@ theorem merge_perm_append : ∀ {xs ys : List α}, merge xs ys le ~ xs ++ ys
     · exact (merge_perm_append.cons y).trans
         ((Perm.swap x y _).trans (perm_middle.symm.cons x))
 
+theorem Perm.merge (s₁ s₂ : α → α → Bool) (hl : l₁ ~ l₂) (hr : r₁ ~ r₂) :
+    merge l₁ r₁ s₁ ~ merge l₂ r₂ s₂ :=
+  Perm.trans (merge_perm_append ..) <| Perm.trans (Perm.append hl hr) <| Perm.symm (merge_perm_append ..)
+
 /-! ### mergeSort -/
 
 @[simp] theorem mergeSort_nil : [].mergeSort r = [] := by rw [List.mergeSort]