From d2189542b5a29393fe5fc244b86fb64d1a43baa5 Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Sat, 4 Jan 2025 15:04:13 +1100
Subject: [PATCH] chore: upstream some List.Perm lemmas (#6524)

This PR upstreams some remaining `List.Perm` lemmas from Batteries.
---
 src/Init/Data/List/Perm.lean        | 14 ++++++++++++++
 src/Init/Data/List/Sort/Lemmas.lean |  4 ++++
 2 files changed, 18 insertions(+)

diff --git a/src/Init/Data/List/Perm.lean b/src/Init/Data/List/Perm.lean
index 501d02daf5..5eef4cc036 100644
--- a/src/Init/Data/List/Perm.lean
+++ b/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
diff --git a/src/Init/Data/List/Sort/Lemmas.lean b/src/Init/Data/List/Sort/Lemmas.lean
index 9bb216e5bf..a8e160fe51 100644
--- a/src/Init/Data/List/Sort/Lemmas.lean
+++ b/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]