diff --git a/Std/Data/List.lean b/Std/Data/List.lean
index 4165ebcfe7..bfb7f926d6 100644
--- a/Std/Data/List.lean
+++ b/Std/Data/List.lean
@@ -4,3 +4,4 @@ import Std.Data.List.Init.Attach
 import Std.Data.List.Lemmas
 import Std.Data.List.Pairwise
 import Std.Data.List.Perm
+import Std.Data.List.SplitOnList
diff --git a/Std/Data/List/Lemmas.lean b/Std/Data/List/Lemmas.lean
index fd749e4554..4c258d2a65 100644
--- a/Std/Data/List/Lemmas.lean
+++ b/Std/Data/List/Lemmas.lean
@@ -132,11 +132,30 @@ theorem drop_left : ∀ l₁ l₂ : List α, drop (length l₁) (l₁ ++ l₂) =
 theorem drop_left' {l₁ l₂ : List α} {n} (h : length l₁ = n) : drop n (l₁ ++ l₂) = l₂ := by
   rw [← h]; apply drop_left
 
+theorem drop_append_left (l l₁ l₂ : List α) :
+    drop (length l + length l₁) (l ++ l₂) = drop (length l₁) l₂ := by
+  match l with
+  | [] => simp
+  | [a] =>
+    simp only [length_singleton, singleton_append]
+    rw [Nat.add_comm, drop_add, drop_one, tail_cons]
+  | a :: b :: l =>
+    rw [← singleton_append, length_append, Nat.add_assoc, append_assoc]
+    have ih := by simpa only [length_append] using drop_append_left [a] (b::l++l₁) (b::l++l₂)
+    rw [ih, drop_append_left (b::l) l₁ l₂]
+termination_by length l
+
 /-! ### isEmpty -/
 
 @[simp] theorem isEmpty_nil : ([] : List α).isEmpty = true := rfl
 @[simp] theorem isEmpty_cons : (x :: xs : List α).isEmpty = false := rfl
 
+theorem isEmpty_iff_eq_nil {l : List α} : l.isEmpty ↔ l = [] := by cases l <;> simp [isEmpty]
+
+@[simp] theorem isEmpty_append : (l₁ ++ l₂ : List α).isEmpty ↔ l₁.isEmpty ∧ l₂.isEmpty := by
+  repeat rw [isEmpty_iff_eq_nil]
+  apply append_eq_nil
+
 /-! ### append -/
 
 theorem append_eq_append : List.append l₁ l₂ = l₁ ++ l₂ := rfl
@@ -165,6 +184,16 @@ theorem append_eq_append_iff {a b c d : List α} :
   | nil => simp; exact (or_iff_left_of_imp fun ⟨_, ⟨e, rfl⟩, h⟩ => e ▸ h.symm).symm
   | cons a as ih => cases c <;> simp [eq_comm, and_assoc, ih, and_or_left]
 
+theorem append_left_eq_self {a b : List α} : a ++ b = b ↔ a = [] := by
+  constructor <;> intro h
+  · exact List.eq_nil_of_length_eq_zero <| Nat.add_left_eq_self.mp (h ▸ List.length_append a b).symm
+  · simp [h]
+
+theorem append_right_eq_self {a b : List α} : a ++ b = a ↔ b = [] := by
+  constructor <;> intro h
+  · exact List.eq_nil_of_length_eq_zero <| Nat.add_right_eq_self.mp (h ▸ List.length_append a b).symm
+  · simp [h]
+
 @[simp] theorem mem_append {a : α} {s t : List α} : a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t := by
   induction s <;> simp_all [or_assoc]
 
@@ -652,6 +681,12 @@ theorem head!_of_head? [Inhabited α] : ∀ {l : List α}, head? l = some a →
 theorem head?_eq_head : ∀ l h, @head? α l = some (head l h)
   | _::_, _ => rfl
 
+theorem headD_eq_head : ∀ l {a₀} h, @headD α l a₀ = head l h
+  | _::_, _, _ => rfl
+
+theorem head_append : ∀ l m h, @head α (l ++ m) (by simp [h]) = head l h
+  | _::_, _, _ => rfl
+
 /-! ### tail -/
 
 @[simp] theorem tailD_eq_tail? (l l' : List α) : tailD l l' = (tail? l).getD l' := by
@@ -661,6 +696,19 @@ theorem tail_eq_tailD (l) : @tail α l = tailD l [] := by cases l <;> rfl
 
 theorem tail_eq_tail? (l) : @tail α l = (tail? l).getD [] := by simp [tail_eq_tailD]
 
+/-! ### head and tail -/
+
+theorem head_cons_tail : ∀ l h, @head α l h :: l.tail = l
+  | _::_, _ => rfl
+
+theorem tail_append (l m) (h : l ≠ []) : @tail α (l ++ m) = tail l ++ m := by
+  rw [← head_cons_tail l h]
+  simp
+
+theorem singleton_head_eq_self (l : List α) (hne : l ≠ []) (htl : l.tail = []) :
+    [l.head hne] = l := by
+  conv => rhs; rw [← head_cons_tail l hne, htl]
+
 /-! ### next? -/
 
 @[simp] theorem next?_nil : @next? α [] = none := rfl
@@ -1163,6 +1211,22 @@ theorem drop_eq_nil_of_eq_nil : ∀ {as : List α} {i}, as = [] → as.drop i =
 theorem ne_nil_of_drop_ne_nil {as : List α} {i : Nat} (h: as.drop i ≠ []) : as ≠ [] :=
   mt drop_eq_nil_of_eq_nil h
 
+/-! ### modify head -/
+
+theorem modifyHead_id : ∀ (l : List α), l.modifyHead id = l
+  | [] => rfl
+  | _::_ => rfl
+
+-- 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]
+@[simp 1100]
+theorem modifyHead_modifyHead (l : List α) (f g : α → α) :
+    (l.modifyHead f).modifyHead g = l.modifyHead (g ∘ f) := by cases l <;> simp
+
 /-! ### modify nth -/
 
 theorem modifyNthTail_id : ∀ n (l : List α), l.modifyNthTail id n = l
@@ -2244,6 +2308,15 @@ theorem IsPrefix.eq_of_length (h : l₁ <+: l₂) : l₁.length = l₂.length 
 theorem IsSuffix.eq_of_length (h : l₁ <:+ l₂) : l₁.length = l₂.length → l₁ = l₂ :=
   h.sublist.eq_of_length
 
+theorem IsInfix.length_lt_of_ne (hin : l₁ <:+: l₂) (hne : l₁ ≠ l₂) : l₁.length < l₂.length :=
+  Nat.lt_of_le_of_ne (IsInfix.length_le hin) (mt (IsInfix.eq_of_length hin) hne)
+
+theorem IsPrefix.length_lt_of_ne (hpf : l₁ <+: l₂) (hne : l₁ ≠ l₂) : l₁.length < l₂.length :=
+  Nat.lt_of_le_of_ne (IsPrefix.length_le hpf) (mt (IsPrefix.eq_of_length hpf) hne)
+
+theorem IsSuffix.length_lt_of_ne (hsf : l₁ <:+ l₂) (hne : l₁ ≠ l₂) : l₁.length < l₂.length :=
+  Nat.lt_of_le_of_ne (IsSuffix.length_le hsf) (mt (IsSuffix.eq_of_length hsf) hne)
+
 theorem prefix_of_prefix_length_le :
     ∀ {l₁ l₂ l₃ : List α}, l₁ <+: l₃ → l₂ <+: l₃ → length l₁ ≤ length l₂ → l₁ <+: l₂
   | [], l₂, _, _, _, _ => nil_prefix _
@@ -2300,6 +2373,9 @@ theorem prefix_append_right_inj (l) : l ++ l₁ <+: l ++ l₂ ↔ l₁ <+: l₂
 theorem prefix_cons_inj (a) : a :: l₁ <+: a :: l₂ ↔ l₁ <+: l₂ :=
   prefix_append_right_inj [a]
 
+theorem singleton_prefix_cons (a) : [a] <+: a :: l :=
+  (prefix_cons_inj a).mpr (nil_prefix l)
+
 theorem take_prefix (n) (l : List α) : take n l <+: l :=
   ⟨_, take_append_drop _ _⟩
 
@@ -2336,6 +2412,101 @@ theorem IsInfix.filter (p : α → Bool) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+
   obtain ⟨xs, ys, rfl⟩ := h
   rw [filter_append, filter_append]; apply infix_append _
 
+theorem IsPrefix.iff_isPrefixOf [BEq α] [LawfulBEq α] {l₁ l₂ : List α} :
+    l₁ <+: l₂ ↔ isPrefixOf l₁ l₂ := by
+  match l₁, l₂ with
+  | [],   _  => simp [nil_prefix]
+  | _::_, [] => simp
+  | a::as, b::bs =>
+    constructor
+    · intro ⟨t, ht⟩
+      simp only [cons_append, cons.injEq] at ht
+      have hpf : as <+: bs := ⟨t, ht.2⟩
+      simpa [isPrefixOf, ht.1] using IsPrefix.iff_isPrefixOf.mp hpf
+    · intro h
+      simp only [isPrefixOf, Bool.and_eq_true, beq_iff_eq] at h
+      let ⟨t, ht⟩ := IsPrefix.iff_isPrefixOf.mpr h.2
+      exists t
+      simpa [h.1]
+
+theorem IsSuffix.iff_isSuffixOf [BEq α] [LawfulBEq α] {l₁ l₂ : List α} :
+    l₁ <:+ l₂ ↔ isSuffixOf l₁ l₂ := by
+  match l₁, l₂ with
+  | [],   _  => simp [nil_suffix, isSuffixOf]
+  | _::_, [] => simp [isSuffixOf, isPrefixOf]
+  | a::as, b::bs =>
+    constructor
+    · intro ⟨t, ht⟩
+      have hpf : (as.reverse ++ [a]) <+: (bs.reverse ++ [b]) := by
+        exists t.reverse
+        simpa using congrArg reverse ht
+      simpa [isSuffixOf, reverse_cons] using IsPrefix.iff_isPrefixOf.mp hpf
+    · intro h
+      simp only [isSuffixOf, reverse_cons] at h
+      let ⟨t, ht⟩ := IsPrefix.iff_isPrefixOf.mpr h
+      exists t.reverse
+      simpa using congrArg reverse ht
+
+theorem eq_of_cons_prefix_cons {a b : α} {l₁ l₂} (h : a :: l₁ <+: b :: l₂) : a = b := by
+  let ⟨t, ht⟩ := h
+  simp only [cons_append, cons.injEq] at ht
+  exact ht.1
+
+theorem head_eq_head_of_prefix (hl₁ : l₁ ≠ []) (hl₂ : l₂ ≠ []) (h : l₁ <+: l₂) :
+    l₁.head hl₁ = l₂.head hl₂ := by
+  obtain ⟨a, l₁, rfl⟩ := l₁.exists_cons_of_ne_nil hl₁
+  obtain ⟨b, l₂, rfl⟩ := l₂.exists_cons_of_ne_nil hl₂
+  simp [eq_of_cons_prefix_cons h, head_cons]
+
+theorem tail_prefix_tail_of_prefix (hl₁ : l₁ ≠ []) (hl₂ : l₂ ≠ []) (h : l₁ <+: l₂) :
+    l₁.tail <+: l₂.tail := by
+  have heq := head_eq_head_of_prefix hl₁ hl₂ h
+  let ⟨t, ht⟩ := h
+  rw [← head_cons_tail l₁ hl₁, ← head_cons_tail l₂ hl₂, ← heq] at ht
+  simp only [cons_append, cons.injEq, true_and] at ht
+  exact ⟨t, ht⟩
+
+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]
+
+theorem prefix_iff_head_eq_and_tail_prefix (hl₁ : l₁ ≠ []) (hl₂ : l₂ ≠ []) :
+    l₁ <+: l₂ ↔ l₁.head hl₁ = l₂.head hl₂ ∧ l₁.tail <+: l₂.tail := by
+  constructor <;> intro h
+  · exact ⟨head_eq_head_of_prefix hl₁ hl₂ h, tail_prefix_tail_of_prefix hl₁ hl₂ h⟩
+  · let ⟨t, ht⟩ := h.2
+    exists t
+    rw [← head_cons_tail l₁ hl₁, ← head_cons_tail l₂ hl₂]
+    simpa [h.1]
+
+theorem ne_nil_of_not_prefix (h : ¬l₁ <+: l₂) : l₁ ≠ [] := by
+  intro heq
+  simp [heq, nil_prefix] at h
+
+theorem not_prefix_and_not_prefix_symm_iff_exists [BEq α] [LawfulBEq α] [DecidableEq α]
+    {l₁ l₂ : List α} : ¬l₁ <+: l₂ ∧ ¬l₂ <+: l₁ ↔ ∃ c₁ c₂ pre suf₁ suf₂, c₁ ≠ c₂ ∧
+      l₁ = pre ++ c₁ :: suf₁ ∧ l₂ = pre ++ c₂ :: suf₂ := by
+  constructor <;> intro h
+  · obtain ⟨c₁, l₁, rfl⟩ := l₁.exists_cons_of_ne_nil (ne_nil_of_not_prefix h.1)
+    obtain ⟨c₂, l₂, rfl⟩ := l₂.exists_cons_of_ne_nil (ne_nil_of_not_prefix h.2)
+    simp only [cons_prefix_iff, not_and] at h
+    cases Decidable.em (c₁ = c₂)
+    · subst c₂
+      simp only [forall_const] at h
+      let ⟨c₁', c₂', pre, suf₁, suf₂, hc, heq₁, heq₂⟩ :=
+        not_prefix_and_not_prefix_symm_iff_exists.mp h
+      exact ⟨c₁', c₂', c₁::pre, suf₁, suf₂, hc, by simp [heq₁], by simp [heq₂]⟩
+    · next hc =>
+      exact ⟨c₁, c₂, [], l₁, l₂, hc, nil_append .., nil_append ..⟩
+  · let ⟨c₁, c₂, pre, suf₁, suf₂, hc, heq₁, heq₂⟩ := h
+    rw [heq₁, heq₂]
+    simp [prefix_append_right_inj, cons_prefix_iff, hc, hc.symm]
+
 /-! ### drop -/
 
 theorem mem_of_mem_drop {n} {l : List α} (h : a ∈ l.drop n) : a ∈ l := drop_subset _ _ h
diff --git a/Std/Data/List/SplitOnList.lean b/Std/Data/List/SplitOnList.lean
new file mode 100644
index 0000000000..78eb8f5c10
--- /dev/null
+++ b/Std/Data/List/SplitOnList.lean
@@ -0,0 +1,160 @@
+/-
+Copyright (c) 2024 Bulhwi Cha, Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bulhwi Cha, Mario Carneiro
+-/
+import Std.Data.List.Lemmas
+
+/-!
+# `List.splitOnList`
+
+This file introduces the `List.splitOnList` function, which is a specification for `String.splitOn`.
+We need it to prove `String.splitOn_of_valid` in `Std.Data.String.Lemmas`.
+```
+[1, 1, 2, 3, 2, 4, 4].splitOnList []     = [[1, 1, 2, 3, 2, 4, 4]]
+[1, 1, 2, 3, 2, 4, 4].splitOnList [5, 6] = [[1, 1, 2, 3, 2, 4, 4]]
+[1, 1, 2, 3, 2, 4, 4].splitOnList [2, 3] = [[1, 1], [2, 4, 4]]
+```
+-/
+
+namespace List
+
+/-- Returns `(l₁, l₂)` for the first split `l = l₁ ++ l₂` such that `P l₂` returns true. -/
+def splitOnceRightP (P : List α → Bool) (l : List α) : Option (List α × List α) :=
+  if P l then
+    some ([], l)
+  else
+    match l with
+    | [] => none
+    | a::l => (splitOnceRightP P l).map fun (l, r) => (a :: l, r)
+
+theorem splitOnceRightP_of_P {P : List α → Bool} {l} (h : P l) :
+    splitOnceRightP P l = some ([], l) := by
+  unfold splitOnceRightP
+  simp [h]
+
+theorem splitOnceRight_nil (P : List α → Bool) :
+    splitOnceRightP P [] = if P [] then some ([], []) else none :=
+  rfl
+
+theorem splitOnceRight_of_ne_nil_of_not_P {P : List α → Bool} {l} (hne : l ≠ []) (hnp : ¬P l) :
+    splitOnceRightP P l = (splitOnceRightP P l.tail).map fun (lf, rt) => (l.head hne :: lf, rt) :=
+      by
+  obtain ⟨a, l, rfl⟩ := exists_cons_of_ne_nil hne
+  conv => lhs; unfold splitOnceRightP
+  simp [hnp]
+
+theorem eq_append_of_splitOnceRightP {P : List α → Bool} {l} :
+    ∀ l₁ l₂, splitOnceRightP P l = some (l₁, l₂) → l = l₁ ++ l₂ := by
+  induction l with
+  | nil => simp [splitOnceRightP]
+  | cons a l ih =>
+    if h : P (a :: l) then
+      simp [splitOnceRightP, h]
+    else
+      simp only [splitOnceRightP, h]
+      match e : splitOnceRightP P l with
+      | none => simp
+      | some (lf, rt) => simp; apply ih; assumption
+
+theorem P_of_splitOnceRightP {P : List α → Bool} {l} :
+    ∀ l₁ l₂, splitOnceRightP P l = some (l₁, l₂) → P l₂ := by
+  induction l with
+  | nil => simp [splitOnceRightP]
+  | cons a l ih =>
+    if h : P (a :: l) then
+      simp [splitOnceRightP, h]
+    else
+      simp only [splitOnceRightP, h]
+      match e : splitOnceRightP P l with
+      | none => simp
+      | some (lf, rt) => simp; apply ih; assumption
+
+variable [BEq α] [LawfulBEq α]
+
+theorem splitOnceRightP_isPrefixOf_eq_none_of_length_lt {l sep : List α}
+    (h : l.length < sep.length) : splitOnceRightP sep.isPrefixOf l = none := by
+  have not_isPrefixOf_of_length_lt {l} (h : l.length < sep.length) : ¬sep.isPrefixOf l := by
+    rw [← IsPrefix.iff_isPrefixOf]
+    exact mt IsPrefix.length_le (Nat.not_le_of_lt h)
+  induction l with
+  | nil => unfold splitOnceRightP; simp [not_isPrefixOf_of_length_lt h]
+  | cons a l ih =>
+    unfold splitOnceRightP
+    simp only [not_isPrefixOf_of_length_lt h, ↓reduceIte, Option.map_eq_none']
+    have h' : l.length < sep.length :=
+      calc
+        l.length < (a :: l).length := by simp
+        _ < sep.length := h
+    exact ih h'
+
+/--
+Split a list at every occurrence of a separator list. The separators are not in the result.
+```
+[1, 1, 2, 3, 2, 4, 4].splitOnList [2, 3] = [[1, 1], [2, 4, 4]]
+```
+-/
+def splitOnList (l sep : List α) : List (List α) :=
+  if h : sep.isEmpty then
+    [l]
+  else
+    match e : splitOnceRightP sep.isPrefixOf l with
+    | none => [l]
+    | some (l₁, l₂) =>
+      have : l₂.length - sep.length < l.length := by
+        rw [eq_append_of_splitOnceRightP l₁ l₂ e, length_append]
+        calc
+          l₂.length - sep.length < l₂.length := Nat.sub_lt_self (by simp [length_pos,
+            ← isEmpty_iff_eq_nil, h]) (IsPrefix.length_le <| IsPrefix.iff_isPrefixOf.mpr
+            (P_of_splitOnceRightP l₁ l₂ e))
+          _ ≤ l₁.length + l₂.length := Nat.le_add_left ..
+      l₁ :: splitOnList (l₂.drop sep.length) sep
+termination_by l.length
+
+theorem splitOnList_nil_left (sep : List α) : splitOnList [] sep = [[]] := by
+  cases sep <;> rfl
+
+theorem splitOnList_nil_right (l : List α) : splitOnList l [] = [l] := by
+  simp [splitOnList]
+
+theorem splitOnList_append_append_of_isPrefixOf {l : List α} (sep₁) {sep₂} (hsp₂ : sep₂ ≠ [])
+    (hpf : sep₂.isPrefixOf l) :
+    splitOnList (sep₁ ++ l) (sep₁ ++ sep₂) =
+      [] :: splitOnList (l.drop sep₂.length) (sep₁ ++ sep₂) := by
+  have hnem : ¬(sep₁ ++ sep₂).isEmpty := by simp [isEmpty_iff_eq_nil, hsp₂]
+  have hpf : (sep₁ ++ sep₂).isPrefixOf (sep₁ ++ l) := by
+    rwa [← IsPrefix.iff_isPrefixOf, prefix_append_right_inj, IsPrefix.iff_isPrefixOf]
+  conv => lhs; unfold splitOnList
+  simp only [hnem, ↓reduceDite, length_append]
+  rw [splitOnceRightP_of_P hpf]
+  simp [drop_append_left]
+
+theorem splitOnList_of_isPrefixOf {l sep : List α} (hsp : sep ≠ []) (hpf : sep.isPrefixOf l) :
+    splitOnList l sep = [] :: splitOnList (l.drop sep.length) sep :=
+  splitOnList_append_append_of_isPrefixOf [] hsp hpf
+
+theorem splitOnList_refl_of_ne_nil (l : List α) (h : l ≠ []) : splitOnList l l = [[], []] := by
+  have hpf : l.isPrefixOf l := IsPrefix.iff_isPrefixOf.mp (prefix_refl l)
+  simp [splitOnList_of_isPrefixOf h hpf, splitOnList_nil_left]
+
+theorem splitOnList_of_ne_nil_of_not_isPrefixOf {l sep : List α} (hne : l ≠ [])
+    (hnpf : ¬sep.isPrefixOf l) :
+    splitOnList l sep = modifyHead (l.head hne :: ·) (splitOnList l.tail sep) := by
+  unfold splitOnList
+  obtain ⟨a, sep, rfl⟩ := exists_cons_of_ne_nil (ne_nil_of_not_prefix (mt IsPrefix.iff_isPrefixOf.mp
+    hnpf))
+  simp only [isEmpty_cons, ↓reduceDite]
+  rw [splitOnceRight_of_ne_nil_of_not_P hne hnpf]
+  match splitOnceRightP (a::sep).isPrefixOf l.tail with
+  | none => simp [head_cons_tail]
+  | some (lf, rt) => rfl
+
+theorem splitOnList_eq_singleton_of_length_lt {l sep : List α} (h : l.length < sep.length) :
+    splitOnList l sep = [l] := by
+  have hne : ¬sep.isEmpty := by
+    simpa [isEmpty_iff_eq_nil, length_pos] using Nat.lt_of_le_of_lt (Nat.zero_le l.length) h
+  unfold splitOnList
+  simp only [hne, ↓reduceDite]
+  rw [splitOnceRightP_isPrefixOf_eq_none_of_length_lt h]
+
+end List
diff --git a/Std/Data/Nat/Lemmas.lean b/Std/Data/Nat/Lemmas.lean
index a0c16adb9d..2671e31804 100644
--- a/Std/Data/Nat/Lemmas.lean
+++ b/Std/Data/Nat/Lemmas.lean
@@ -194,6 +194,24 @@ protected def sum_trichotomy (a b : Nat) : a < b ⊕' a = b ⊕' b < a :=
 
 @[deprecated] alias succ_add_eq_succ_add := Nat.succ_add_eq_add_succ
 
+protected theorem add_left_eq_self {n m : Nat} : n + m = m ↔ n = 0 := by
+  conv => lhs; rhs; rw [← Nat.zero_add m]
+  rw [Nat.add_right_cancel_iff]
+
+protected theorem add_right_eq_self {n m : Nat} : n + m = n ↔ m = 0 := by
+  conv => lhs; rhs; rw [← Nat.add_zero n]
+  rw [Nat.add_left_cancel_iff]
+
+protected theorem add_left_le_self {n m : Nat} : n + m ≤ m ↔ n = 0 := by
+  conv => lhs; rhs; rw [← Nat.zero_add m]
+  rw [Nat.add_le_add_iff_right]
+  apply Nat.le_zero
+
+protected theorem add_right_le_self {n m : Nat} : n + m ≤ n ↔ m = 0 := by
+  conv => lhs; rhs; rw [← Nat.add_zero n]
+  rw [Nat.add_le_add_iff_left]
+  apply Nat.le_zero
+
 /-! ## sub -/
 
 @[deprecated] protected alias le_of_le_of_sub_le_sub_right := Nat.le_of_sub_le_sub_right
diff --git a/Std/Data/String/Lemmas.lean b/Std/Data/String/Lemmas.lean
index c472875da4..a726a97c9b 100644
--- a/Std/Data/String/Lemmas.lean
+++ b/Std/Data/String/Lemmas.lean
@@ -4,10 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bulhwi Cha, Mario Carneiro
 -/
 import Std.Data.Char
-import Std.Data.Nat.Lemmas
-import Std.Data.List.Lemmas
+import Std.Data.List.SplitOnList
 import Std.Data.String.Basic
-import Std.Tactic.Lint.Misc
+import Std.Logic
 import Std.Tactic.SeqFocus
 
 @[simp] theorem Char.length_toString (c : Char) : c.toString.length = 1 := rfl
@@ -478,7 +477,229 @@ theorem splitAux_of_valid (p l m r acc) :
 theorem split_of_valid (s p) : split s p = (List.splitOnP p s.1).map mk := by
   simpa [split] using splitAux_of_valid p [] [] s.1 []
 
--- TODO: splitOn
+end String
+
+namespace List
+open String
+
+/-- Auxiliary definition for proving `String.splitOnAux_of_valid`. -/
+private def splitOnListAux (sep₁ sep₂ l m : List Char) (h : sep₂ ≠ []) : List (List Char) :=
+  if hls : m = [] then
+    [l ++ sep₁]
+  else
+    have : utf8Len m.tail < utf8Len m := by
+      conv => rhs; rw [← head_cons_tail m hls, utf8Len_cons]
+      exact Nat.lt_add_of_pos_right (csize_pos (m.head hls))
+    if m.head hls = sep₂.head h then
+      if htl₂ : sep₂.tail = [] then
+        l :: splitOnListAux [] (sep₁ ++ [sep₂.head h]) [] m.tail (by simp [h])
+      else
+        splitOnListAux (sep₁ ++ [m.head hls]) sep₂.tail l m.tail htl₂
+    else
+      splitOnListAux [] (sep₁ ++ sep₂) (l ++ sep₁ ++ [m.head hls]) m.tail (by simp [h])
+termination_by utf8Len m
+
+private theorem modifyHead_append_splitOnListAux (sep₁ sep₂ l m r) (h : sep₂ ≠ []) :
+    modifyHead (l ++ ·) (splitOnListAux sep₁ sep₂ m r h) =
+      splitOnListAux sep₁ sep₂ (l ++ m) r h := by
+  unfold splitOnListAux
+  simp only [append_assoc]
+  split
+  · simp
+  · next hls =>
+    have : utf8Len r.tail < utf8Len r := by
+      conv => rhs; rw [← head_cons_tail r hls, utf8Len_cons]
+      exact Nat.lt_add_of_pos_right (csize_pos (r.head hls))
+    split
+    · split <;> [simp; apply modifyHead_append_splitOnListAux]
+    · apply modifyHead_append_splitOnListAux
+termination_by utf8Len r
+
+-- NOTE: make the following changes: `sep₂` ⇒ `sep₂ ++ sep₃`, `m` ⇒ `sep₂ ++ m`
+private theorem splitOnListAux_of_isPrefixOf (sep₁ sep₂ l m) (hsp₂ : sep₂ ≠ [])
+    (hpf : sep₂.isPrefixOf m) :
+    splitOnListAux sep₁ sep₂ l m hsp₂ = l :: splitOnListAux [] (sep₁ ++ sep₂) []
+      (m.drop sep₂.length) (by simp [hsp₂]) := by
+  obtain ⟨c₂, sep₂, rfl⟩ := sep₂.exists_cons_of_ne_nil hsp₂
+  let ⟨t, ht⟩ := IsPrefix.iff_isPrefixOf.mpr hpf
+  conv => lhs; unfold splitOnListAux
+  simp only [← ht, cons_append, ↓reduceDite, head_cons, ↓reduceIte, tail_cons, length_cons,
+    drop_succ_cons, drop_left]
+  split
+  · subst sep₂; simp
+  · next htl₂ =>
+    have : utf8Len sep₂ < utf8Len (c₂ :: sep₂) := Nat.lt_add_of_pos_right (csize_pos c₂)
+    simpa only [append_assoc, singleton_append, drop_left] using
+      splitOnListAux_of_isPrefixOf (sep₁++[c₂]) sep₂ l (sep₂++t) htl₂ (IsPrefix.iff_isPrefixOf.mp
+      <| prefix_append sep₂ t)
+termination_by utf8Len sep₂
+
+private theorem splitOnListAux_append_cons_append_cons_of_ne (c₃ cₘ) (sep₁ sep₂ sep₃ l m)
+    (hne : c₃ ≠ cₘ) :
+    splitOnListAux sep₁ (sep₂ ++ c₃ :: sep₃) l (sep₂ ++ cₘ :: m) (by simp) =
+      splitOnListAux [] (sep₁ ++ sep₂ ++ c₃ :: sep₃) (l ++ sep₁ ++ sep₂ ++ [cₘ]) m (by simp) := by
+  conv => lhs; unfold splitOnListAux
+  simp only [append_eq_nil, and_false, ↓reduceDite, append_assoc]
+  cases sep₂
+  · simp only [nil_append, head_cons, tail_cons, ite_eq_right_iff]
+    intro heq
+    exact absurd heq.symm hne
+  · next c₂ sep₂ =>
+    simp only [cons_append, head_cons, ↓reduceIte, tail_cons, append_eq_nil, and_false, ↓reduceDite]
+    simpa using (splitOnListAux_append_cons_append_cons_of_ne c₃ cₘ (sep₁++[c₂]) sep₂
+      sep₃ l m hne)
+
+private theorem splitOnListAux_nil_eq_modifyHead_append_splitOnList (sep l m) (h : sep ≠ []) :
+    splitOnListAux [] sep l m h = modifyHead (l ++ ·) (splitOnList m sep) := by
+  unfold splitOnListAux
+  simp only [append_nil, head_cons, tail_cons, nil_append]
+  split
+  · next hls => simp [hls, splitOnList_nil_left]
+  · next hls =>
+    obtain ⟨cₛ, sep, rfl⟩ := sep.exists_cons_of_ne_nil h
+    obtain ⟨cₘ, m, rfl⟩ := m.exists_cons_of_ne_nil hls
+    have : utf8Len m < utf8Len (cₘ :: m) := Nat.lt_add_of_pos_right (csize_pos cₘ)
+    simp only [List.headD_cons, List.head_cons, List.tail_cons, false_or]
+    split
+    · subst cₛ
+      split
+      · subst sep
+        simp only [modifyHead, by simpa using splitOnList_of_isPrefixOf h (show [cₘ].isPrefixOf
+          (cₘ :: m) by simp), append_nil, cons.injEq, true_and]
+        simpa only [nil_append, ← Function.id_def, modifyHead_id] using
+          splitOnListAux_nil_eq_modifyHead_append_splitOnList [cₘ] [] m (by simp)
+      · next hsp =>
+        match hpf : sep.isPrefixOf m with
+        | true =>
+          have : utf8Len (m.drop sep.length) < utf8Len (cₘ :: m) := by
+            let ⟨t, ht⟩ := IsPrefix.iff_isPrefixOf.mpr hpf
+            simp [← ht, Nat.add_comm (utf8Len sep), Nat.add_assoc]
+            exact Nat.lt_add_of_pos_right <| Nat.lt_of_lt_of_le (csize_pos cₘ)
+              (Nat.le_add_right (csize cₘ) (utf8Len sep))
+          have hpf' : (cₘ :: sep).isPrefixOf (cₘ :: m) := by
+            rwa [← IsPrefix.iff_isPrefixOf, prefix_cons_inj, IsPrefix.iff_isPrefixOf]
+          simp [splitOnListAux_of_isPrefixOf [cₘ] sep l m hsp hpf, by simpa using
+            (splitOnList_of_isPrefixOf (by simp) hpf')]
+          simpa only [nil_append, ← Function.id_def, modifyHead_id] using
+            splitOnListAux_nil_eq_modifyHead_append_splitOnList (cₘ::sep) [] (m.drop sep.length) (by
+              simp)
+        | false =>
+          cases Decidable.em (m = [])
+          · subst m
+            have hlt : [cₘ].length < (cₘ :: sep).length := by
+              conv => rhs; rw [← singleton_append, length_append]
+              exact Nat.lt_add_of_pos_right (length_pos.mpr hsp)
+            simp [splitOnListAux, splitOnList_eq_singleton_of_length_lt hlt]
+          · next htl =>
+            match hpf' : m.isPrefixOf sep with
+            | true =>
+              have hne : m ≠ sep := by
+                intro heq
+                rw [heq] at hpf hpf'
+                exact (ne_true_of_eq_false hpf) hpf'
+              have hlt : (cₘ :: m).length < (cₘ :: sep).length := IsPrefix.length_lt_of_ne
+                ((prefix_cons_inj cₘ).mpr <| IsPrefix.iff_isPrefixOf.mpr hpf') (by simp [hne])
+              simp [splitOnList_eq_singleton_of_length_lt hlt]
+              sorry
+            | false =>
+              let ⟨c₂', cₘ', pre, suf₂, sufₘ, hc, heq₂, heqₘ⟩ :=
+                not_prefix_and_not_prefix_symm_iff_exists.mp
+                ⟨mt IsPrefix.iff_isPrefixOf.mp (ne_true_of_eq_false hpf),
+                 mt IsPrefix.iff_isPrefixOf.mp (ne_true_of_eq_false hpf')⟩
+              have : utf8Len sufₘ < utf8Len m := by
+                rw [heqₘ, utf8Len_append, utf8Len_cons, ← Nat.add_assoc, Nat.add_comm _
+                  (utf8Len sufₘ), Nat.add_assoc]
+                exact Nat.lt_add_of_pos_right (Nat.add_pos_right _ (csize_pos cₘ'))
+              conv => lhs; rw [heqₘ]; arg 2; rw [heq₂]
+              rw [splitOnListAux_append_cons_append_cons_of_ne c₂' cₘ' [cₘ] pre suf₂ l sufₘ hc,
+                splitOnListAux_nil_eq_modifyHead_append_splitOnList ([cₘ]++pre++c₂'::suf₂)
+                (l++[cₘ]++pre++[cₘ']) sufₘ (by simp)]
+              rw [heqₘ, heq₂]
+              sorry
+    · next hhd =>
+      have hnpf : ¬(cₛ :: sep).isPrefixOf (cₘ :: m) := by
+        intro hpf
+        simp [isPrefixOf] at hpf
+        exact hhd hpf.1.symm
+      simp only [splitOnListAux_nil_eq_modifyHead_append_splitOnList (cₛ :: sep) (l ++ [cₘ]) m (by
+        simp), by simpa only [tail_cons, ne_eq, not_false_eq_true, head_cons] using
+        splitOnList_of_ne_nil_of_not_isPrefixOf (by simp) hnpf, head_cons, tail_cons,
+        modifyHead_modifyHead]
+      simp
+termination_by utf8Len m
+
+namespace Test
+set_option linter.missingDocs false
+
+def l := "ABC".1
+def cₘ := '<'
+def pre := "<".1
+def cₘ' := '<'
+def c₂' := '$'
+def sufₘ := "$>>DEF".1
+def suf₂ := ">>DEF".1
+
+#eval (modifyHead (fun x => l ++ [cₘ] ++ pre ++ [cₘ'] ++ x) (splitOnList sufₘ ([cₘ] ++ pre ++ c₂' ::
+  suf₂))).map String.mk
+#eval (modifyHead (fun x => l ++ x) (splitOnList (cₘ :: (pre ++ cₘ' :: sufₘ)) (cₘ :: (pre ++ c₂' :: suf₂)))).map
+  String.mk
+
+def m := cₘ :: (pre ++ cₘ' :: sufₘ)
+def sep := cₘ :: (pre ++ c₂' :: suf₂)
+theorem h : sep ≠ [] := by simp [sep]
+
+#eval String.mk m
+#eval String.mk sep
+
+#eval (splitOnListAux l sep [] m h).map String.mk
+#eval (modifyHead (l ++ ·) (splitOnList m sep)).map String.mk
+
+end Test
+end List
+
+namespace String
+
+theorem splitOnAux_of_valid (sep₁ sep₂ l m r acc) (h : sep₂ ≠ []) :
+    splitOnAux ⟨l ++ m ++ sep₁ ++ r⟩ ⟨sep₁ ++ sep₂⟩ ⟨utf8Len l⟩ ⟨utf8Len (l ++ m ++ sep₁)⟩
+      ⟨utf8Len sep₁⟩ acc = acc.reverse ++ (List.splitOnListAux sep₁ sep₂ m r h).map mk := by
+  obtain ⟨c₂, sep₂, rfl⟩ := sep₂.exists_cons_of_ne_nil h
+  rw [splitOnAux, List.splitOnListAux]
+  simp only [List.append_assoc, utf8Len_append, atEnd_iff, endPos_eq, Pos.mk_le_mk,
+    Nat.add_le_add_iff_left, Nat.add_right_le_self, utf8Len_eq_zero, by simpa only
+    [List.append_assoc, utf8Len_append] using (⟨get_of_valid (l++m++sep₁) r, next_of_valid
+    (l++m++sep₁) (r.headD default) r, extract_of_valid l (m++sep₁) r⟩ : _∧_∧_),  List.reverse_cons,
+    get_of_valid, List.headD_cons, beq_iff_eq, next, Pos.addChar_eq, utf8Len_cons,
+    Nat.add_left_le_self, Pos.sub_eq, dite_eq_ite]
+  split
+  · simp
+  · next hls =>
+    obtain ⟨cᵣ, r, rfl⟩ := r.exists_cons_of_ne_nil hls
+    simp only [List.headD_cons, List.head_cons, List.tail_cons, false_or]
+    split
+    · next hc =>
+      subst c₂
+      rw [← Nat.add_assoc, Nat.add_assoc, Nat.add_sub_cancel, Nat.add_assoc]
+      split
+      · subst sep₂
+        simpa [by simpa using extract_of_valid l m (sep₁++cᵣ::r)] using
+          splitOnAux_of_valid [] (sep₁++[cᵣ]) (l++m++sep₁++[cᵣ]) [] r (⟨m⟩::acc) (by simp)
+      · next hsp₂ =>
+        simpa using splitOnAux_of_valid (sep₁++[cᵣ]) sep₂ l m r acc hsp₂
+    · next hc =>
+      simpa [Nat.add_assoc] using splitOnAux_of_valid [] (sep₁++c₂::sep₂) l (m++sep₁++[cᵣ]) r acc
+        (by simp)
+
+theorem splitOn_of_valid (s sep) : splitOn s sep = (List.splitOnList s.1 sep.1).map mk := by
+  simp only [splitOn, beq_iff_eq]
+  split
+  · next hsp => simp [hsp, List.splitOnList]
+  · next hsp =>
+    have aux := by simpa using splitOnAux_of_valid [] sep.1 [] [] s.1 [] (hsp ∘ ext)
+    rw [aux]; clear aux
+    apply congrArg (List.map mk)
+    simpa only [List.nil_append, ← Function.id_def, List.modifyHead_id]
+      using List.splitOnListAux_nil_eq_modifyHead_append_splitOnList sep.1 [] s.1 (by rwa [ext_iff]
+        at hsp)
 
 @[simp] theorem toString_toSubstring (s : String) : s.toSubstring.toString = s :=
   extract_zero_endPos _
diff --git a/Std/Logic.lean b/Std/Logic.lean
index 43a9b31f66..b10d460bf0 100644
--- a/Std/Logic.lean
+++ b/Std/Logic.lean
@@ -12,6 +12,10 @@ instance {f : α → β} [DecidablePred p] : DecidablePred (p ∘ f) :=
 
 @[deprecated] alias proofIrrel := proof_irrel
 
+/-! ## id -/
+
+theorem Function.id_def : @id α = fun x => x := rfl
+
 /-! ## exists and forall -/
 
 alias ⟨forall_not_of_not_exists, not_exists_of_forall_not⟩ := not_exists