diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index 6fdb8dc95a..8e86124a9f 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -826,46 +826,6 @@ def dropLast {α} : List α → List α
     have ih := length_dropLast_cons b bs
     simp [dropLast, ih]
 
-/-! ### isPrefixOf -/
-
-/--  `isPrefixOf l₁ l₂` returns `true` Iff `l₁` is a prefix of `l₂`.
-That is, there exists a `t` such that `l₂ == l₁ ++ t`. -/
-def isPrefixOf [BEq α] : List α → List α → Bool
-  | [],    _     => true
-  | _,     []    => false
-  | a::as, b::bs => a == b && isPrefixOf as bs
-
-@[simp] theorem isPrefixOf_nil_left [BEq α] : isPrefixOf ([] : List α) l = true := by
-  simp [isPrefixOf]
-@[simp] theorem isPrefixOf_cons_nil [BEq α] : isPrefixOf (a::as) ([] : List α) = false := rfl
-theorem isPrefixOf_cons₂ [BEq α] {a : α} :
-    isPrefixOf (a::as) (b::bs) = (a == b && isPrefixOf as bs) := rfl
-
-/-! ### isPrefixOf? -/
-
-/-- `isPrefixOf? l₁ l₂` returns `some t` when `l₂ == l₁ ++ t`. -/
-def isPrefixOf? [BEq α] : List α → List α → Option (List α)
-  | [], l₂ => some l₂
-  | _, [] => none
-  | (x₁ :: l₁), (x₂ :: l₂) =>
-    if x₁ == x₂ then isPrefixOf? l₁ l₂ else none
-
-/-! ### isSuffixOf -/
-
-/--  `isSuffixOf l₁ l₂` returns `true` Iff `l₁` is a suffix of `l₂`.
-That is, there exists a `t` such that `l₂ == t ++ l₁`. -/
-def isSuffixOf [BEq α] (l₁ l₂ : List α) : Bool :=
-  isPrefixOf l₁.reverse l₂.reverse
-
-@[simp] theorem isSuffixOf_nil_left [BEq α] : isSuffixOf ([] : List α) l = true := by
-  simp [isSuffixOf]
-
-/-! ### isSuffixOf? -/
-
-/-- `isSuffixOf? l₁ l₂` returns `some t` when `l₂ == t ++ l₁`.-/
-def isSuffixOf? [BEq α] (l₁ l₂ : List α) : Option (List α) :=
-  Option.map List.reverse <| isPrefixOf? l₁.reverse l₂.reverse
-
 /-! ### Subset -/
 
 /--
@@ -900,6 +860,68 @@ def isSublist [BEq α] : List α → List α → Bool
     then tl₁.isSublist tl₂
     else l₁.isSublist tl₂
 
+/-! ### IsPrefix / isPrefixOf / isPrefixOf? -/
+
+/--
+`IsPrefix l₁ l₂`, or `l₁ <+: l₂`, means that `l₁` is a prefix of `l₂`,
+that is, `l₂` has the form `l₁ ++ t` for some `t`.
+-/
+def IsPrefix (l₁ : List α) (l₂ : List α) : Prop := Exists fun t => l₁ ++ t = l₂
+
+@[inherit_doc] infixl:50 " <+: " => IsPrefix
+
+/--  `isPrefixOf l₁ l₂` returns `true` Iff `l₁` is a prefix of `l₂`.
+That is, there exists a `t` such that `l₂ == l₁ ++ t`. -/
+def isPrefixOf [BEq α] : List α → List α → Bool
+  | [],    _     => true
+  | _,     []    => false
+  | a::as, b::bs => a == b && isPrefixOf as bs
+
+@[simp] theorem isPrefixOf_nil_left [BEq α] : isPrefixOf ([] : List α) l = true := by
+  simp [isPrefixOf]
+@[simp] theorem isPrefixOf_cons_nil [BEq α] : isPrefixOf (a::as) ([] : List α) = false := rfl
+theorem isPrefixOf_cons₂ [BEq α] {a : α} :
+    isPrefixOf (a::as) (b::bs) = (a == b && isPrefixOf as bs) := rfl
+
+/-- `isPrefixOf? l₁ l₂` returns `some t` when `l₂ == l₁ ++ t`. -/
+def isPrefixOf? [BEq α] : List α → List α → Option (List α)
+  | [], l₂ => some l₂
+  | _, [] => none
+  | (x₁ :: l₁), (x₂ :: l₂) =>
+    if x₁ == x₂ then isPrefixOf? l₁ l₂ else none
+
+/-! ### IsSuffix / isSuffixOf / isSuffixOf? -/
+
+/--  `isSuffixOf l₁ l₂` returns `true` Iff `l₁` is a suffix of `l₂`.
+That is, there exists a `t` such that `l₂ == t ++ l₁`. -/
+def isSuffixOf [BEq α] (l₁ l₂ : List α) : Bool :=
+  isPrefixOf l₁.reverse l₂.reverse
+
+@[simp] theorem isSuffixOf_nil_left [BEq α] : isSuffixOf ([] : List α) l = true := by
+  simp [isSuffixOf]
+
+/-- `isSuffixOf? l₁ l₂` returns `some t` when `l₂ == t ++ l₁`.-/
+def isSuffixOf? [BEq α] (l₁ l₂ : List α) : Option (List α) :=
+  Option.map List.reverse <| isPrefixOf? l₁.reverse l₂.reverse
+
+/--
+`IsSuffix l₁ l₂`, or `l₁ <:+ l₂`, means that `l₁` is a suffix of `l₂`,
+that is, `l₂` has the form `t ++ l₁` for some `t`.
+-/
+def IsSuffix (l₁ : List α) (l₂ : List α) : Prop := Exists fun t => t ++ l₁ = l₂
+
+@[inherit_doc] infixl:50 " <:+ " => IsSuffix
+
+/-! ### IsInfix -/
+
+/--
+`IsInfix l₁ l₂`, or `l₁ <:+: l₂`, means that `l₁` is a contiguous
+substring of `l₂`, that is, `l₂` has the form `s ++ l₁ ++ t` for some `s, t`.
+-/
+def IsInfix (l₁ : List α) (l₂ : List α) : Prop := Exists fun s => Exists fun t => s ++ l₁ ++ t = l₂
+
+@[inherit_doc] infixl:50 " <:+: " => IsInfix
+
 /-! ### rotateLeft -/
 
 /--
diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index d944952612..d4ae89adb9 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -2700,6 +2700,201 @@ theorem join_sublist_iff {L : List (List α)} {l} :
 instance [DecidableEq α] (l₁ l₂ : List α) : Decidable (l₁ <+ l₂) :=
   decidable_of_iff (l₁.isSublist l₂) isSublist_iff_sublist
 
+/-! ### IsPrefix / IsSuffix / IsInfix -/
+
+@[simp] theorem prefix_append (l₁ l₂ : List α) : l₁ <+: l₁ ++ l₂ := ⟨l₂, rfl⟩
+
+@[simp] theorem suffix_append (l₁ l₂ : List α) : l₂ <:+ l₁ ++ l₂ := ⟨l₁, rfl⟩
+
+theorem infix_append (l₁ l₂ l₃ : List α) : l₂ <:+: l₁ ++ l₂ ++ l₃ := ⟨l₁, l₃, rfl⟩
+
+@[simp] theorem infix_append' (l₁ l₂ l₃ : List α) : l₂ <:+: l₁ ++ (l₂ ++ l₃) := by
+  rw [← List.append_assoc]; apply infix_append
+
+theorem IsPrefix.isInfix : l₁ <+: l₂ → l₁ <:+: l₂ := fun ⟨t, h⟩ => ⟨[], t, h⟩
+
+theorem IsSuffix.isInfix : l₁ <:+ l₂ → l₁ <:+: l₂ := fun ⟨t, h⟩ => ⟨t, [], by rw [h, append_nil]⟩
+
+theorem nil_prefix (l : List α) : [] <+: l := ⟨l, rfl⟩
+
+theorem nil_suffix (l : List α) : [] <:+ l := ⟨l, append_nil _⟩
+
+theorem nil_infix (l : List α) : [] <:+: l := (nil_prefix _).isInfix
+
+theorem prefix_refl (l : List α) : l <+: l := ⟨[], append_nil _⟩
+
+theorem suffix_refl (l : List α) : l <:+ l := ⟨[], rfl⟩
+
+theorem infix_refl (l : List α) : l <:+: l := (prefix_refl l).isInfix
+
+@[simp] theorem suffix_cons (a : α) : ∀ l, l <:+ a :: l := suffix_append [a]
+
+theorem infix_cons : l₁ <:+: l₂ → l₁ <:+: a :: l₂ := fun ⟨L₁, L₂, h⟩ => ⟨a :: L₁, L₂, h ▸ rfl⟩
+
+theorem infix_concat : l₁ <:+: l₂ → l₁ <:+: concat l₂ a := fun ⟨L₁, L₂, h⟩ =>
+  ⟨L₁, concat L₂ a, by simp [← h, concat_eq_append, append_assoc]⟩
+
+theorem IsPrefix.trans : ∀ {l₁ l₂ l₃ : List α}, l₁ <+: l₂ → l₂ <+: l₃ → l₁ <+: l₃
+  | _, _, _, ⟨r₁, rfl⟩, ⟨r₂, rfl⟩ => ⟨r₁ ++ r₂, (append_assoc _ _ _).symm⟩
+
+theorem IsSuffix.trans : ∀ {l₁ l₂ l₃ : List α}, l₁ <:+ l₂ → l₂ <:+ l₃ → l₁ <:+ l₃
+  | _, _, _, ⟨l₁, rfl⟩, ⟨l₂, rfl⟩ => ⟨l₂ ++ l₁, append_assoc _ _ _⟩
+
+theorem IsInfix.trans : ∀ {l₁ l₂ l₃ : List α}, l₁ <:+: l₂ → l₂ <:+: l₃ → l₁ <:+: l₃
+  | l, _, _, ⟨l₁, r₁, rfl⟩, ⟨l₂, r₂, rfl⟩ => ⟨l₂ ++ l₁, r₁ ++ r₂, by simp only [append_assoc]⟩
+
+protected theorem IsInfix.sublist : l₁ <:+: l₂ → l₁ <+ l₂
+  | ⟨_, _, h⟩ => h ▸ (sublist_append_right ..).trans (sublist_append_left ..)
+
+protected theorem IsInfix.subset (hl : l₁ <:+: l₂) : l₁ ⊆ l₂ :=
+  hl.sublist.subset
+
+protected theorem IsPrefix.sublist (h : l₁ <+: l₂) : l₁ <+ l₂ :=
+  h.isInfix.sublist
+
+protected theorem IsPrefix.subset (hl : l₁ <+: l₂) : l₁ ⊆ l₂ :=
+  hl.sublist.subset
+
+protected theorem IsSuffix.sublist (h : l₁ <:+ l₂) : l₁ <+ l₂ :=
+  h.isInfix.sublist
+
+protected theorem IsSuffix.subset (hl : l₁ <:+ l₂) : l₁ ⊆ l₂ :=
+  hl.sublist.subset
+
+@[simp] theorem reverse_suffix : reverse l₁ <:+ reverse l₂ ↔ l₁ <+: l₂ :=
+  ⟨fun ⟨r, e⟩ => ⟨reverse r, by rw [← reverse_reverse l₁, ← reverse_append, e, reverse_reverse]⟩,
+   fun ⟨r, e⟩ => ⟨reverse r, by rw [← reverse_append, e]⟩⟩
+
+@[simp] theorem reverse_prefix : reverse l₁ <+: reverse l₂ ↔ l₁ <:+ l₂ := by
+  rw [← reverse_suffix]; simp only [reverse_reverse]
+
+@[simp] theorem reverse_infix : reverse l₁ <:+: reverse l₂ ↔ l₁ <:+: l₂ := by
+  refine ⟨fun ⟨s, t, e⟩ => ⟨reverse t, reverse s, ?_⟩, fun ⟨s, t, e⟩ => ⟨reverse t, reverse s, ?_⟩⟩
+  · rw [← reverse_reverse l₁, append_assoc, ← reverse_append, ← reverse_append, e,
+      reverse_reverse]
+  · rw [append_assoc, ← reverse_append, ← reverse_append, e]
+
+theorem IsInfix.length_le (h : l₁ <:+: l₂) : l₁.length ≤ l₂.length :=
+  h.sublist.length_le
+
+theorem IsPrefix.length_le (h : l₁ <+: l₂) : l₁.length ≤ l₂.length :=
+  h.sublist.length_le
+
+theorem IsSuffix.length_le (h : l₁ <:+ l₂) : l₁.length ≤ l₂.length :=
+  h.sublist.length_le
+
+@[simp] theorem infix_nil : l <:+: [] ↔ l = [] := ⟨(sublist_nil.1 ·.sublist), (· ▸ infix_refl _)⟩
+
+@[simp] theorem prefix_nil : l <+: [] ↔ l = [] := ⟨(sublist_nil.1 ·.sublist), (· ▸ prefix_refl _)⟩
+
+@[simp] theorem suffix_nil : l <:+ [] ↔ l = [] := ⟨(sublist_nil.1 ·.sublist), (· ▸ suffix_refl _)⟩
+
+theorem infix_iff_prefix_suffix (l₁ l₂ : List α) : l₁ <:+: l₂ ↔ ∃ t, l₁ <+: t ∧ t <:+ l₂ :=
+  ⟨fun ⟨_, t, e⟩ => ⟨l₁ ++ t, ⟨_, rfl⟩, e ▸ append_assoc .. ▸ ⟨_, rfl⟩⟩,
+    fun ⟨_, ⟨t, rfl⟩, s, e⟩ => ⟨s, t, append_assoc .. ▸ e⟩⟩
+
+theorem IsInfix.eq_of_length (h : l₁ <:+: l₂) : l₁.length = l₂.length → l₁ = l₂ :=
+  h.sublist.eq_of_length
+
+theorem IsPrefix.eq_of_length (h : l₁ <+: l₂) : l₁.length = l₂.length → l₁ = l₂ :=
+  h.sublist.eq_of_length
+
+theorem IsSuffix.eq_of_length (h : l₁ <:+ l₂) : l₁.length = l₂.length → l₁ = l₂ :=
+  h.sublist.eq_of_length
+
+theorem prefix_of_prefix_length_le :
+    ∀ {l₁ l₂ l₃ : List α}, l₁ <+: l₃ → l₂ <+: l₃ → length l₁ ≤ length l₂ → l₁ <+: l₂
+  | [], l₂, _, _, _, _ => nil_prefix _
+  | a :: l₁, b :: l₂, _, ⟨r₁, rfl⟩, ⟨r₂, e⟩, ll => by
+    injection e with _ e'; subst b
+    rcases prefix_of_prefix_length_le ⟨_, rfl⟩ ⟨_, e'⟩ (le_of_succ_le_succ ll) with ⟨r₃, rfl⟩
+    exact ⟨r₃, rfl⟩
+
+theorem prefix_or_prefix_of_prefix (h₁ : l₁ <+: l₃) (h₂ : l₂ <+: l₃) : l₁ <+: l₂ ∨ l₂ <+: l₁ :=
+  (Nat.le_total (length l₁) (length l₂)).imp (prefix_of_prefix_length_le h₁ h₂)
+    (prefix_of_prefix_length_le h₂ h₁)
+
+theorem suffix_of_suffix_length_le
+    (h₁ : l₁ <:+ l₃) (h₂ : l₂ <:+ l₃) (ll : length l₁ ≤ length l₂) : l₁ <:+ l₂ :=
+  reverse_prefix.1 <|
+    prefix_of_prefix_length_le (reverse_prefix.2 h₁) (reverse_prefix.2 h₂) (by simp [ll])
+
+theorem suffix_or_suffix_of_suffix (h₁ : l₁ <:+ l₃) (h₂ : l₂ <:+ l₃) : l₁ <:+ l₂ ∨ l₂ <:+ l₁ :=
+  (prefix_or_prefix_of_prefix (reverse_prefix.2 h₁) (reverse_prefix.2 h₂)).imp reverse_prefix.1
+    reverse_prefix.1
+
+theorem suffix_cons_iff : l₁ <:+ a :: l₂ ↔ l₁ = a :: l₂ ∨ l₁ <:+ l₂ := by
+  constructor
+  · rintro ⟨⟨hd, tl⟩, hl₃⟩
+    · exact Or.inl hl₃
+    · simp only [cons_append] at hl₃
+      injection hl₃ with _ hl₄
+      exact Or.inr ⟨_, hl₄⟩
+  · rintro (rfl | hl₁)
+    · exact (a :: l₂).suffix_refl
+    · exact hl₁.trans (l₂.suffix_cons _)
+
+theorem infix_cons_iff : l₁ <:+: a :: l₂ ↔ l₁ <+: a :: l₂ ∨ l₁ <:+: l₂ := by
+  constructor
+  · rintro ⟨⟨hd, tl⟩, t, hl₃⟩
+    · exact Or.inl ⟨t, hl₃⟩
+    · simp only [cons_append] at hl₃
+      injection hl₃ with _ hl₄
+      exact Or.inr ⟨_, t, hl₄⟩
+  · rintro (h | hl₁)
+    · exact h.isInfix
+    · exact infix_cons hl₁
+
+theorem infix_of_mem_join : ∀ {L : List (List α)}, l ∈ L → l <:+: join L
+  | l' :: _, h =>
+    match h with
+    | List.Mem.head .. => infix_append [] _ _
+    | List.Mem.tail _ hlMemL =>
+      IsInfix.trans (infix_of_mem_join hlMemL) <| (suffix_append _ _).isInfix
+
+theorem prefix_append_right_inj (l) : l ++ l₁ <+: l ++ l₂ ↔ l₁ <+: l₂ :=
+  exists_congr fun r => by rw [append_assoc, append_right_inj]
+
+@[simp]
+theorem prefix_cons_inj (a) : a :: l₁ <+: a :: l₂ ↔ l₁ <+: l₂ :=
+  prefix_append_right_inj [a]
+
+theorem take_prefix (n) (l : List α) : take n l <+: l :=
+  ⟨_, take_append_drop _ _⟩
+
+theorem drop_suffix (n) (l : List α) : drop n l <:+ l :=
+  ⟨_, take_append_drop _ _⟩
+
+theorem take_sublist (n) (l : List α) : take n l <+ l :=
+  (take_prefix n l).sublist
+
+theorem drop_sublist (n) (l : List α) : drop n l <+ l :=
+  (drop_suffix n l).sublist
+
+theorem take_subset (n) (l : List α) : take n l ⊆ l :=
+  (take_sublist n l).subset
+
+theorem drop_subset (n) (l : List α) : drop n l ⊆ l :=
+  (drop_sublist n l).subset
+
+theorem mem_of_mem_take {l : List α} (h : a ∈ l.take n) : a ∈ l :=
+  take_subset n l h
+
+theorem IsPrefix.filter (p : α → Bool) ⦃l₁ l₂ : List α⦄ (h : l₁ <+: l₂) :
+    l₁.filter p <+: l₂.filter p := by
+  obtain ⟨xs, rfl⟩ := h
+  rw [filter_append]; apply prefix_append
+
+theorem IsSuffix.filter (p : α → Bool) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+ l₂) :
+    l₁.filter p <:+ l₂.filter p := by
+  obtain ⟨xs, rfl⟩ := h
+  rw [filter_append]; apply suffix_append
+
+theorem IsInfix.filter (p : α → Bool) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+: l₂) :
+    l₁.filter p <:+: l₂.filter p := by
+  obtain ⟨xs, ys, rfl⟩ := h
+  rw [filter_append, filter_append]; apply infix_append _
+
 /-! ### rotateLeft -/
 
 @[simp] theorem rotateLeft_zero (l : List α) : rotateLeft l 0 = l := by