refactor: move theorems about lists to std

* `List.isEmpty_iff_eq_nil` and `List.modifyHead_modifyHead` are from
  `Mathlib.Data.List.Basic`.
* `List.cons_prefix_iff` is from `Mathlib.Data.List.Infix`.
* We need these theorems to prove `String.splitOn_of_valid`.

See leanprover-community/batteries#756.

Mathlib/Data/List/Basic.lean

@@ -602,10 +602,6 @@ theorem map_reverseAux (f : α → β) (l₁ l₂ : List α) :
 
 /-! ### empty -/
 
--- Porting note: this does not work as desired
--- attribute [simp] List.isEmpty
-
-theorem isEmpty_iff_eq_nil {l : List α} : l.isEmpty ↔ l = [] := by cases l <;> simp [isEmpty]
 #align list.empty_iff_eq_nil List.isEmpty_iff_eq_nil
 
 /-! ### dropLast -/
@@ -890,14 +886,6 @@ theorem nthLe_cons {l : List α} {a : α} {n} (hl) :
 
 end deprecated
 
--- Porting note: List.modifyHead has @[simp], and Lean 4 treats this as
--- an invitation to unfold modifyHead in any context,
--- not just use the equational lemmas.
-
--- @[simp]
-@[simp 1100, nolint simpNF]
-theorem modifyHead_modifyHead (l : List α) (f g : α → α) :
-    (l.modifyHead f).modifyHead g = l.modifyHead (g ∘ f) := by cases l <;> simp
 #align list.modify_head_modify_head List.modifyHead_modifyHead
 
 /-! ### Induction from the right -/

Mathlib/Data/List/Infix.lean

@@ -300,14 +300,6 @@ theorem prefix_take_le_iff {L : List (List (Option α))} (hm : m < L.length) :
         exact ⟨Nat.succ_le_succ, Nat.le_of_succ_le_succ⟩
 #align list.prefix_take_le_iff List.prefix_take_le_iff
 
-theorem cons_prefix_iff : a :: l₁ <+: b :: l₂ ↔ a = b ∧ l₁ <+: l₂ := by
-  constructor
-  · rintro ⟨L, hL⟩
-    simp only [cons_append] at hL
-    injection hL with hLLeft hLRight
-    exact ⟨hLLeft, ⟨L, hLRight⟩⟩
-  · rintro ⟨rfl, h⟩
-    rwa [prefix_cons_inj]
 #align list.cons_prefix_iff List.cons_prefix_iff
 
 protected theorem IsPrefix.map (h : l₁ <+: l₂) (f : α → β) : l₁.map f <+: l₂.map f := by