remove upstreamed

Batteries/Data/List/Lemmas.lean

@@ -590,37 +590,6 @@ theorem insertP_loop (a : α) (l r : List α) :
   induction l with simp [insertP, insertP.loop, cond]
   | cons _ _ ih => split <;> simp [insertP_loop, ih]
 
-/-! ### merge -/
-
-theorem cons_merge_cons (s : α → α → Bool) (a b l r) :
-    merge (a::l) (b::r) s = if s a b then a :: merge l (b::r) s else b :: merge (a::l) r s := by
-  simp only [merge]
-
-@[simp] theorem cons_merge_cons_pos (s : α → α → Bool) (l r) (h : s a b) :
-    merge (a::l) (b::r) s = a :: merge l (b::r) s := by
-  rw [cons_merge_cons, if_pos h]
-
-@[simp] theorem cons_merge_cons_neg (s : α → α → Bool) (l r) (h : ¬ s a b) :
-    merge (a::l) (b::r) s = b :: merge (a::l) r s := by
-  rw [cons_merge_cons, if_neg h]
-
-@[simp] theorem length_merge (s : α → α → Bool) (l r) :
-    (merge l r s).length = l.length + r.length := by
-  match l, r with
-  | [], r => simp
-  | l, [] => simp
-  | a::l, b::r =>
-    rw [cons_merge_cons]
-    split
-    · simp_arith [length_merge s l (b::r)]
-    · simp_arith [length_merge s (a::l) r]
-
-theorem mem_merge_left (s : α → α → Bool) (h : x ∈ l) : x ∈ merge l r s :=
-  mem_merge.2 <| .inl h
-
-theorem mem_merge_right (s : α → α → Bool) (h : x ∈ r) : x ∈ merge l r s :=
-  mem_merge.2 <| .inr h
-
 /-! ### foldlM and foldrM -/
 
 theorem foldlM_map [Monad m] (f : β₁ → β₂) (g : α → β₂ → m α) (l : List β₁) (init : α) :