refactor: move theorems about lists from mathlib

* `List.isEmpty_iff_eq_nil` and `List.modifyHead_modifyHead` are from
  `Mathlib.Data.List.Basic`. I removed the `simp` priority and `nolint`
  attribute from `modifyHead_modifyHead` because we don't need them
  anymore.
* `List.cons_prefix_cons` is from `Mathlib.Data.List.Infix`. Its
  previous name was `List.cons_prefix_iff`.

We need these theorems to prove `String.splitOn_of_valid`. See
#756.

Co-authored-by: Kim Morrison <[email protected]>

Batteries/Data/List/Lemmas.lean

@@ -23,6 +23,10 @@ open Nat
 theorem drop_one : ∀ l : List α, drop 1 l = tail l
   | [] | _ :: _ => rfl
 
+/-! ### isEmpty -/
+
+theorem isEmpty_iff_eq_nil {l : List α} : l.isEmpty ↔ l = [] := by cases l <;> simp [isEmpty]
+
 /-! ### zipWith -/
 
 theorem zipWith_distrib_tail : (zipWith f l l').tail = zipWith f l.tail l'.tail := by
@@ -272,6 +276,11 @@ theorem tail_drop (l : List α) (n : Nat) : (l.drop n).tail = l.drop (n + 1) :=
     · simp
     · simp [hl]
 
+/-! ### modifyHead -/
+
+@[simp] theorem modifyHead_modifyHead (l : List α) (f g : α → α) :
+    (l.modifyHead f).modifyHead g = l.modifyHead (g ∘ f) := by cases l <;> simp [modifyHead]
+
 /-! ### modifyNth -/
 
 @[simp] theorem modifyNth_nil (f : α → α) (n) : [].modifyNth f n = [] := by cases n <;> rfl
@@ -1217,6 +1226,15 @@ theorem IsInfix.filter (p : α → Bool) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+
   obtain ⟨xs, ys, rfl⟩ := h
   rw [filter_append, filter_append]; apply infix_append _
 
+theorem cons_prefix_cons : 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]
+
 /-! ### drop -/
 
 theorem mem_of_mem_drop {n} {l : List α} (h : a ∈ l.drop n) : a ∈ l := drop_subset _ _ h