tests

src/Init/Data/List/Basic.lean

@@ -1190,10 +1190,10 @@ def isPrefixOf [BEq α] : List α → List α → Bool
   | _,     []    => false
   | a::as, b::bs => a == b && isPrefixOf as bs
 
-@[simp] theorem isPrefixOf_nil_left [BEq α] : isPrefixOf ([] : List α) l = true := by
+@[simp, grind =] 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 : α} :
+@[simp, grind =] theorem isPrefixOf_cons_nil [BEq α] : isPrefixOf (a::as) ([] : List α) = false := rfl
+@[grind =] theorem isPrefixOf_cons₂ [BEq α] {a : α} :
     isPrefixOf (a::as) (b::bs) = (a == b && isPrefixOf as bs) := rfl
 
 /--
@@ -1229,7 +1229,7 @@ Examples:
 def isSuffixOf [BEq α] (l₁ l₂ : List α) : Bool :=
   isPrefixOf l₁.reverse l₂.reverse
 
-@[simp] theorem isSuffixOf_nil_left [BEq α] : isSuffixOf ([] : List α) l = true := by
+@[simp, grind =] theorem isSuffixOf_nil_left [BEq α] : isSuffixOf ([] : List α) l = true := by
   simp [isSuffixOf]
 
 /--

src/Init/Data/List/Count.lean

@@ -232,7 +232,7 @@ theorem count_le_count_cons {a b : α} {l : List α} : count a l ≤ count a (b
 theorem count_singleton {a b : α} : count a [b] = if b == a then 1 else 0 := by
   simp [count_cons]
 
-@[simp] theorem count_append {a : α} {l₁ l₂ : List α} : count a (l₁ ++ l₂) = count a l₁ + count a l₂ :=
+@[simp, grind =] theorem count_append {a : α} {l₁ l₂ : List α} : count a (l₁ ++ l₂) = count a l₁ + count a l₂ :=
   countP_append
 
 theorem count_flatten {a : α} {l : List (List α)} : count a l.flatten = (l.map (count a)).sum := by
@@ -283,7 +283,7 @@ theorem count_eq_length {l : List α} : count a l = l.length ↔ ∀ b ∈ l, a
 @[simp] theorem count_replicate_self {a : α} {n : Nat} : count a (replicate n a) = n :=
   (count_eq_length.2 <| fun _ h => (eq_of_mem_replicate h).symm).trans (length_replicate ..)
 
-theorem count_replicate {a b : α} {n : Nat} : count a (replicate n b) = if b == a then n else 0 := by
+@[grind =] theorem count_replicate {a b : α} {n : Nat} : count a (replicate n b) = if b == a then n else 0 := by
   split <;> (rename_i h; simp only [beq_iff_eq] at h)
   · exact ‹b = a› ▸ count_replicate_self ..
   · exact count_eq_zero.2 <| mt eq_of_mem_replicate (Ne.symm h)
@@ -295,14 +295,18 @@ theorem filter_beq {l : List α} (a : α) : l.filter (· == a) = replicate (coun
 theorem filter_eq [DecidableEq α] {l : List α} (a : α) : l.filter (· = a) = replicate (count a l) a :=
   funext (Bool.beq_eq_decide_eq · a) ▸ filter_beq a
 
-theorem le_count_iff_replicate_sublist {l : List α} : n ≤ count a l ↔ replicate n a <+ l := by
+@[grind =] theorem replicate_sublist_iff {l : List α} : replicate n a <+ l ↔ n ≤ count a l := by
   refine ⟨fun h => ?_, fun h => ?_⟩
-  · exact ((replicate_sublist_replicate a).2 h).trans <| filter_beq a ▸ filter_sublist
   · simpa only [count_replicate_self] using h.count_le a
+  · exact ((replicate_sublist_replicate a).2 h).trans <| filter_beq a ▸ filter_sublist
+
+@[deprecated replicate_sublist_iff (since := "2025-05-26")]
+theorem le_count_iff_replicate_sublist {l : List α} : n ≤ count a l ↔ replicate n a <+ l :=
+  replicate_sublist_iff.symm
 
 theorem replicate_count_eq_of_count_eq_length {l : List α} (h : count a l = length l) :
     replicate (count a l) a = l :=
-  (le_count_iff_replicate_sublist.mp (Nat.le_refl _)).eq_of_length <| length_replicate.trans h
+  (replicate_sublist_iff.mpr (Nat.le_refl _)).eq_of_length <| length_replicate.trans h
 
 @[simp] theorem count_filter {l : List α} (h : p a) : count a (filter p l) = count a l := by
   rw [count, countP_filter]; congr; funext b

src/Init/Data/List/Nat/Sublist.lean

@@ -30,7 +30,7 @@ theorem IsSuffix.getElem {xs ys : List α} (h : xs <:+ ys) {i} (hn : i < xs.leng
   have := h.length_le
   omega
 
-theorem isSuffix_iff : l₁ <:+ l₂ ↔
+theorem suffix_iff_getElem? : l₁ <:+ l₂ ↔
     l₁.length ≤ l₂.length ∧ ∀ i (h : i < l₁.length), l₂[i + l₂.length - l₁.length]? = some l₁[i] := by
   suffices l₁.length ≤ l₂.length ∧ l₁ <:+ l₂ ↔
       l₁.length ≤ l₂.length ∧ ∀ i (h : i < l₁.length), l₂[i + l₂.length - l₁.length]? = some l₁[i] by
@@ -41,7 +41,7 @@ theorem isSuffix_iff : l₁ <:+ l₂ ↔
       exact (this.mpr h).2
   simp only [and_congr_right_iff]
   intro le
-  rw [← reverse_prefix, isPrefix_iff]
+  rw [← reverse_prefix, prefix_iff_getElem?]
   simp only [length_reverse]
   constructor
   · intro w i h
@@ -60,15 +60,33 @@ theorem isSuffix_iff : l₁ <:+ l₂ ↔
     rw [w, getElem_reverse]
     exact Nat.lt_of_lt_of_le h le
 
-theorem isInfix_iff : l₁ <:+: l₂ ↔
+@[deprecated suffix_iff_getElem? (since := "2025-05-27")]
+abbrev isSuffix_iff := @suffix_iff_getElem?
+
+theorem suffix_iff_getElem {l₁ l₂ : List α} :
+    l₁ <:+ l₂ ↔ ∃ (_ : l₁.length ≤ l₂.length), ∀ i (_ : i < l₁.length), l₂[i + l₂.length - l₁.length] = l₁[i] := by
+  rw [suffix_iff_getElem?]
+  constructor
+  · rintro ⟨h, w⟩
+    refine ⟨h, fun i h => ?_⟩
+    specialize w i h
+    rw [getElem?_eq_getElem] at w
+    simpa using w
+  · rintro ⟨h, w⟩
+    refine ⟨h, fun i h => ?_⟩
+    specialize w i h
+    rw [getElem?_eq_getElem]
+    simpa using w
+
+theorem infix_iff_getElem? : l₁ <:+: l₂ ↔
     ∃ k, l₁.length + k ≤ l₂.length ∧ ∀ i (h : i < l₁.length), l₂[i + k]? = some l₁[i] := by
   constructor
   · intro h
     obtain ⟨t, p, s⟩ := infix_iff_suffix_prefix.mp h
     refine ⟨t.length - l₁.length, by have := p.length_le; have := s.length_le; omega, ?_⟩
-    rw [isSuffix_iff] at p
+    rw [suffix_iff_getElem?] at p
     obtain ⟨p', p⟩ := p
-    rw [isPrefix_iff] at s
+    rw [prefix_iff_getElem?] at s
     intro i h
     rw [s _ (by omega)]
     specialize p i (by omega)
@@ -93,6 +111,9 @@ theorem isInfix_iff : l₁ <:+: l₂ ↔
       simp_all
       omega
 
+@[deprecated infix_iff_getElem? (since := "2025-05-27")]
+abbrev isInfix_iff := @infix_iff_getElem?
+
 theorem suffix_iff_eq_append : l₁ <:+ l₂ ↔ take (length l₂ - length l₁) l₂ ++ l₁ = l₂ :=
   ⟨by rintro ⟨r, rfl⟩; simp only [length_append, Nat.add_sub_cancel_right, take_left], fun e =>
     ⟨_, e⟩⟩
@@ -115,7 +136,7 @@ theorem suffix_iff_eq_drop : l₁ <:+ l₂ ↔ l₁ = drop (length l₂ - length
   ⟨fun h => append_cancel_left <| (suffix_iff_eq_append.1 h).trans (take_append_drop _ _).symm,
     fun e => e.symm ▸ drop_suffix _ _⟩
 
-theorem prefix_take_le_iff {xs : List α} (hm : i < xs.length) :
+@[grind =] theorem prefix_take_le_iff {xs : List α} (hm : i < xs.length) :
     xs.take i <+: xs.take j ↔ i ≤ j := by
   simp only [prefix_iff_eq_take, length_take]
   induction i generalizing xs j with

src/Init/Data/List/Nat/TakeDrop.lean

@@ -199,7 +199,7 @@ theorem take_eq_dropLast {l : List α} {i : Nat} (h : i + 1 = l.length) :
         simpa using h
 
 theorem take_prefix_take_left {l : List α} {i j : Nat} (h : i ≤ j) : take i l <+: take j l := by
-  rw [isPrefix_iff]
+  rw [prefix_iff_getElem?]
   intro i w
   rw [getElem?_take_of_lt, getElem_take, getElem?_eq_getElem]
   simp only [length_take] at w

src/Init/Data/List/Pairwise.lean

@@ -276,9 +276,12 @@ theorem nodup_nil : @Nodup α [] :=
 theorem nodup_cons {a : α} {l : List α} : Nodup (a :: l) ↔ a ∉ l ∧ Nodup l := by
   simp only [Nodup, pairwise_cons, forall_mem_ne]
 
-@[grind →] theorem Nodup.sublist : l₁ <+ l₂ → Nodup l₂ → Nodup l₁ :=
+theorem Nodup.sublist : l₁ <+ l₂ → Nodup l₂ → Nodup l₁ :=
   Pairwise.sublist
 
+grind_pattern Nodup.sublist => l₁ <+ l₂, Nodup l₁
+grind_pattern Nodup.sublist => l₁ <+ l₂, Nodup l₂
+
 theorem Sublist.nodup : l₁ <+ l₂ → Nodup l₂ → Nodup l₁ :=
   Nodup.sublist
 

src/Init/Data/List/Sublist.lean

@@ -24,14 +24,14 @@ open Nat
 section isPrefixOf
 variable [BEq α]
 
-@[simp] theorem isPrefixOf_cons₂_self [LawfulBEq α] {a : α} :
+@[simp, grind =] theorem isPrefixOf_cons₂_self [LawfulBEq α] {a : α} :
     isPrefixOf (a::as) (a::bs) = isPrefixOf as bs := by simp [isPrefixOf_cons₂]
 
 @[simp] theorem isPrefixOf_length_pos_nil {l : List α} (h : 0 < l.length) : isPrefixOf l [] = false := by
   cases l <;> simp_all [isPrefixOf]
 
-@[simp] theorem isPrefixOf_replicate {a : α} :
-    isPrefixOf l (replicate n a) = (decide (l.length ≤ n) && l.all (· == a)) := by
+@[simp, grind =] theorem isPrefixOf_replicate {a : α} :
+    isPrefixOf l (replicate n a) = ((l.length ≤ n) && l.all (· == a)) := by
   induction l generalizing n with
   | nil => simp
   | cons _ _ ih =>
@@ -45,10 +45,10 @@ end isPrefixOf
 section isSuffixOf
 variable [BEq α]
 
-@[simp] theorem isSuffixOf_cons_nil : isSuffixOf (a::as) ([] : List α) = false := by
+@[simp, grind =] theorem isSuffixOf_cons_nil : isSuffixOf (a::as) ([] : List α) = false := by
   simp [isSuffixOf]
 
-@[simp] theorem isSuffixOf_replicate {a : α} :
+@[simp, grind =] theorem isSuffixOf_replicate {a : α} :
     isSuffixOf l (replicate n a) = (decide (l.length ≤ n) && l.all (· == a)) := by
   simp [isSuffixOf, all_eq]
 
@@ -58,7 +58,8 @@ end isSuffixOf
 
 /-! ### List subset -/
 
-theorem subset_def {l₁ l₂ : List α} : l₁ ⊆ l₂ ↔ ∀ {a : α}, a ∈ l₁ → a ∈ l₂ := .rfl
+-- For now we don't annotate lemmas about `Subset` for `grind`, but instead just unfold the definition.
+@[grind =] theorem subset_def {l₁ l₂ : List α} : l₁ ⊆ l₂ ↔ ∀ {a : α}, a ∈ l₁ → a ∈ l₂ := .rfl
 
 @[simp] theorem nil_subset (l : List α) : [] ⊆ l := nofun
 
@@ -139,11 +140,11 @@ theorem subset_replicate {n : Nat} {a : α} {l : List α} (h : n ≠ 0) : l ⊆
 
 /-! ### Sublist and isSublist -/
 
-@[simp] theorem nil_sublist : ∀ l : List α, [] <+ l
+@[simp, grind] theorem nil_sublist : ∀ l : List α, [] <+ l
   | [] => .slnil
   | a :: l => (nil_sublist l).cons a
 
-@[simp] theorem Sublist.refl : ∀ l : List α, l <+ l
+@[simp, grind] theorem Sublist.refl : ∀ l : List α, l <+ l
   | [] => .slnil
   | a :: l => (Sublist.refl l).cons₂ a
 
@@ -160,14 +161,14 @@ theorem Sublist.trans {l₁ l₂ l₃ : List α} (h₁ : l₁ <+ l₂) (h₂ : l
 
 instance : Trans (@Sublist α) Sublist Sublist := ⟨Sublist.trans⟩
 
-attribute [simp] Sublist.cons
+attribute [simp, grind] Sublist.cons
 
 theorem sublist_cons_self (a : α) (l : List α) : l <+ a :: l := (Sublist.refl l).cons _
 
 theorem sublist_of_cons_sublist : a :: l₁ <+ l₂ → l₁ <+ l₂ :=
   (sublist_cons_self a l₁).trans
 
-@[simp]
+@[simp, grind =]
 theorem cons_sublist_cons : a :: l₁ <+ a :: l₂ ↔ l₁ <+ l₂ :=
   ⟨fun | .cons _ s => sublist_of_cons_sublist s | .cons₂ _ s => s, .cons₂ _⟩
 
@@ -181,7 +182,7 @@ theorem sublist_or_mem_of_sublist (h : l <+ l₁ ++ a :: l₂) : l <+ l₁ ++ l
     | .cons _ h => exact (IH h).imp_left (Sublist.cons _)
     | .cons₂ _ h => exact (IH h).imp (Sublist.cons₂ _) (.tail _)
 
-theorem Sublist.subset : l₁ <+ l₂ → l₁ ⊆ l₂
+@[grind →] theorem Sublist.subset : l₁ <+ l₂ → l₁ ⊆ l₂
   | .slnil, _, h => h
   | .cons _ s, _, h => .tail _ (s.subset h)
   | .cons₂ .., _, .head .. => .head ..
@@ -190,10 +191,10 @@ theorem Sublist.subset : l₁ <+ l₂ → l₁ ⊆ l₂
 protected theorem Sublist.mem (hx : a ∈ l₁) (hl : l₁ <+ l₂) : a ∈ l₂ :=
   hl.subset hx
 
-theorem Sublist.head_mem (s : ys <+ xs) (h) : ys.head h ∈ xs :=
+@[grind] theorem Sublist.head_mem (s : ys <+ xs) (h) : ys.head h ∈ xs :=
   s.mem (List.head_mem h)
 
-theorem Sublist.getLast_mem (s : ys <+ xs) (h) : ys.getLast h ∈ xs :=
+@[grind] theorem Sublist.getLast_mem (s : ys <+ xs) (h) : ys.getLast h ∈ xs :=
   s.mem (List.getLast_mem h)
 
 instance : Trans (@Sublist α) Subset Subset :=
@@ -208,7 +209,7 @@ instance : Trans (fun l₁ l₂ => Sublist l₂ l₁) (Membership.mem : List α
 theorem mem_of_cons_sublist {a : α} {l₁ l₂ : List α} (s : a :: l₁ <+ l₂) : a ∈ l₂ :=
   (cons_subset.1 s.subset).1
 
-@[simp] theorem sublist_nil {l : List α} : l <+ [] ↔ l = [] :=
+@[simp, grind =] theorem sublist_nil {l : List α} : l <+ [] ↔ l = [] :=
   ⟨fun s => subset_nil.1 s.subset, fun H => H ▸ Sublist.refl _⟩
 
 theorem eq_nil_of_sublist_nil {l : List α} (s : l <+ []) : l = [] :=
@@ -219,29 +220,39 @@ theorem Sublist.length_le : l₁ <+ l₂ → length l₁ ≤ length l₂
   | .cons _l s => le_succ_of_le (length_le s)
   | .cons₂ _ s => succ_le_succ (length_le s)
 
+grind_pattern Sublist.length_le => l₁ <+ l₂, length l₁
+grind_pattern Sublist.length_le => l₁ <+ l₂, length l₂
+
 theorem Sublist.eq_of_length : l₁ <+ l₂ → length l₁ = length l₂ → l₁ = l₂
   | .slnil, _ => rfl
   | .cons a s, h => nomatch Nat.not_lt.2 s.length_le (h ▸ lt_succ_self _)
   | .cons₂ a s, h => by rw [s.eq_of_length (succ.inj h)]
 
+-- Only activative `eq_of_length` if we're already thinking about lengths.
+grind_pattern Sublist.eq_of_length => l₁ <+ l₂, length l₁, length l₂
+
 theorem Sublist.eq_of_length_le (s : l₁ <+ l₂) (h : length l₂ ≤ length l₁) : l₁ = l₂ :=
   s.eq_of_length <| Nat.le_antisymm s.length_le h
 
 theorem Sublist.length_eq (s : l₁ <+ l₂) : length l₁ = length l₂ ↔ l₁ = l₂ :=
   ⟨s.eq_of_length, congrArg _⟩
 
+@[grind]
 theorem tail_sublist : ∀ l : List α, tail l <+ l
   | [] => .slnil
   | a::l => sublist_cons_self a l
 
+@[grind]
 protected theorem Sublist.tail : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → tail l₁ <+ tail l₂
   | _, _, slnil => .slnil
   | _, _, Sublist.cons _ h => (tail_sublist _).trans h
   | _, _, Sublist.cons₂ _ h => h
 
+@[grind →]
 theorem Sublist.of_cons_cons {l₁ l₂ : List α} {a b : α} (h : a :: l₁ <+ b :: l₂) : l₁ <+ l₂ :=
   h.tail
 
+@[grind]
 protected theorem Sublist.map (f : α → β) {l₁ l₂} (s : l₁ <+ l₂) : map f l₁ <+ map f l₂ := by
   induction s with
   | slnil => simp
@@ -250,10 +261,12 @@ protected theorem Sublist.map (f : α → β) {l₁ l₂} (s : l₁ <+ l₂) : m
   | cons₂ a s ih =>
     simpa using cons₂ (f a) ih
 
+@[grind]
 protected theorem Sublist.filterMap (f : α → Option β) (s : l₁ <+ l₂) :
     filterMap f l₁ <+ filterMap f l₂ := by
   induction s <;> simp [filterMap_cons] <;> split <;> simp [*, cons, cons₂]
 
+@[grind]
 protected theorem Sublist.filter (p : α → Bool) {l₁ l₂} (s : l₁ <+ l₂) : filter p l₁ <+ filter p l₂ := by
   rw [← filterMap_eq_filter]; apply s.filterMap
 
@@ -263,6 +276,7 @@ theorem head_filter_mem (xs : List α) (p : α → Bool) (h) : (xs.filter p).hea
 theorem getLast_filter_mem (xs : List α) (p : α → Bool) (h) : (xs.filter p).getLast h ∈ xs :=
   filter_sublist.getLast_mem h
 
+@[grind =]
 theorem sublist_filterMap_iff {l₁ : List β} {f : α → Option β} :
     l₁ <+ l₂.filterMap f ↔ ∃ l', l' <+ l₂ ∧ l₁ = l'.filterMap f := by
   induction l₂ generalizing l₁ with
@@ -297,10 +311,12 @@ theorem sublist_filterMap_iff {l₁ : List β} {f : α → Option β} :
         rwa [filterMap_cons_some] at h
         assumption
 
+@[grind =]
 theorem sublist_map_iff {l₁ : List β} {f : α → β} :
     l₁ <+ l₂.map f ↔ ∃ l', l' <+ l₂ ∧ l₁ = l'.map f := by
   simp only [← filterMap_eq_map, sublist_filterMap_iff]
 
+@[grind =]
 theorem sublist_filter_iff {l₁ : List α} {p : α → Bool} :
     l₁ <+ l₂.filter p ↔ ∃ l', l' <+ l₂ ∧ l₁ = l'.filter p := by
   simp only [← filterMap_eq_filter, sublist_filterMap_iff]
@@ -309,11 +325,15 @@ theorem sublist_append_left : ∀ l₁ l₂ : List α, l₁ <+ l₁ ++ l₂
   | [], _ => nil_sublist _
   | _ :: l₁, l₂ => (sublist_append_left l₁ l₂).cons₂ _
 
+grind_pattern sublist_append_left => Sublist, l₁ ++ l₂
+
 theorem sublist_append_right : ∀ l₁ l₂ : List α, l₂ <+ l₁ ++ l₂
   | [], _ => Sublist.refl _
   | _ :: l₁, l₂ => (sublist_append_right l₁ l₂).cons _
 
-@[simp] theorem singleton_sublist {a : α} {l} : [a] <+ l ↔ a ∈ l := by
+grind_pattern sublist_append_right => Sublist, l₁ ++ l₂
+
+@[simp, grind =] theorem singleton_sublist {a : α} {l} : [a] <+ l ↔ a ∈ l := by
   refine ⟨fun h => h.subset (mem_singleton_self _), fun h => ?_⟩
   obtain ⟨_, _, rfl⟩ := append_of_mem h
   exact ((nil_sublist _).cons₂ _).trans (sublist_append_right ..)
@@ -321,10 +341,14 @@ theorem sublist_append_right : ∀ l₁ l₂ : List α, l₂ <+ l₁ ++ l₂
 @[simp] theorem sublist_append_of_sublist_left (s : l <+ l₁) : l <+ l₁ ++ l₂ :=
   s.trans <| sublist_append_left ..
 
+grind_pattern sublist_append_of_sublist_left => l <+ l₁, l₁ ++ l₂
+
 @[simp] theorem sublist_append_of_sublist_right (s : l <+ l₂) : l <+ l₁ ++ l₂ :=
   s.trans <| sublist_append_right ..
 
-@[simp] theorem append_sublist_append_left : ∀ l, l ++ l₁ <+ l ++ l₂ ↔ l₁ <+ l₂
+grind_pattern sublist_append_of_sublist_right => l <+ l₂, l₁ ++ l₂
+
+@[simp, grind =] theorem append_sublist_append_left : ∀ l, l ++ l₁ <+ l ++ l₂ ↔ l₁ <+ l₂
   | [] => Iff.rfl
   | _ :: l => cons_sublist_cons.trans (append_sublist_append_left l)
 
@@ -339,6 +363,9 @@ theorem Sublist.append_right : l₁ <+ l₂ → ∀ l, l₁ ++ l <+ l₂ ++ l
 theorem Sublist.append (hl : l₁ <+ l₂) (hr : r₁ <+ r₂) : l₁ ++ r₁ <+ l₂ ++ r₂ :=
   (hl.append_right _).trans ((append_sublist_append_left _).2 hr)
 
+grind_pattern Sublist.append => l₁ <+ l₂, r₁ <+ r₂, l₁ ++ r₁, l₂ ++ r₂
+
+@[grind =]
 theorem sublist_cons_iff {a : α} {l l'} :
     l <+ a :: l' ↔ l <+ l' ∨ ∃ r, l = a :: r ∧ r <+ l' := by
   constructor
@@ -350,6 +377,7 @@ theorem sublist_cons_iff {a : α} {l l'} :
     · exact h.cons _
     · exact h.cons₂ _
 
+@[grind =]
 theorem cons_sublist_iff {a : α} {l l'} :
     a :: l <+ l' ↔ ∃ r₁ r₂, l' = r₁ ++ r₂ ∧ a ∈ r₁ ∧ l <+ r₂ := by
   induction l' with
@@ -433,6 +461,7 @@ theorem Sublist.of_sublist_append_right (w : ∀ a, a ∈ l → a ∉ l₁) (h :
     exact fun x m => w x (mem_append_left l₂' m) (h₁.mem m)
   simp_all
 
+@[grind]
 theorem Sublist.middle {l : List α} (h : l <+ l₁ ++ l₂) (a : α) : l <+ l₁ ++ a :: l₂ := by
   rw [sublist_append_iff] at h
   obtain ⟨l₁', l₂', rfl, h₁, h₂⟩ := h
@@ -443,13 +472,14 @@ theorem Sublist.reverse : l₁ <+ l₂ → l₁.reverse <+ l₂.reverse
   | .cons _ h => by rw [reverse_cons]; exact sublist_append_of_sublist_left h.reverse
   | .cons₂ _ h => by rw [reverse_cons, reverse_cons]; exact h.reverse.append_right _
 
-@[simp] theorem reverse_sublist : l₁.reverse <+ l₂.reverse ↔ l₁ <+ l₂ :=
+@[simp, grind =] theorem reverse_sublist : l₁.reverse <+ l₂.reverse ↔ l₁ <+ l₂ :=
   ⟨fun h => l₁.reverse_reverse ▸ l₂.reverse_reverse ▸ h.reverse, Sublist.reverse⟩
 
+@[grind _=_]
 theorem sublist_reverse_iff : l₁ <+ l₂.reverse ↔ l₁.reverse <+ l₂ :=
   by rw [← reverse_sublist, reverse_reverse]
 
-@[simp] theorem append_sublist_append_right (l) : l₁ ++ l <+ l₂ ++ l ↔ l₁ <+ l₂ :=
+@[simp, grind =] theorem append_sublist_append_right (l) : l₁ ++ l <+ l₂ ++ l ↔ l₁ <+ l₂ :=
   ⟨fun h => by
     have := h.reverse
     simp only [reverse_append, append_sublist_append_left, reverse_sublist] at this
@@ -464,6 +494,7 @@ theorem sublist_reverse_iff : l₁ <+ l₂.reverse ↔ l₁.reverse <+ l₂ :=
     | refl => apply Sublist.refl
     | step => simp [*, replicate, Sublist.cons]
 
+@[grind =]
 theorem sublist_replicate_iff : l <+ replicate m a ↔ ∃ n, n ≤ m ∧ l = replicate n a := by
   induction l generalizing m with
   | nil =>
@@ -551,7 +582,7 @@ theorem flatten_sublist_iff {L : List (List α)} {l} :
         exact ⟨l₁, L'.flatten, by simp, by simpa using h 0 (by simp), L', rfl,
           fun i lt => by simpa using h (i+1) (Nat.add_lt_add_right lt 1)⟩
 
-@[simp] theorem isSublist_iff_sublist [BEq α] [LawfulBEq α] {l₁ l₂ : List α} :
+@[simp, grind =] theorem isSublist_iff_sublist [BEq α] [LawfulBEq α] {l₁ l₂ : List α} :
     l₁.isSublist l₂ ↔ l₁ <+ l₂ := by
   cases l₁ <;> cases l₂ <;> simp [isSublist]
   case cons.cons hd₁ tl₁ hd₂ tl₂ =>
@@ -573,41 +604,49 @@ theorem flatten_sublist_iff {L : List (List α)} {l} :
 instance [DecidableEq α] (l₁ l₂ : List α) : Decidable (l₁ <+ l₂) :=
   decidable_of_iff (l₁.isSublist l₂) isSublist_iff_sublist
 
+@[grind]
 protected theorem Sublist.drop : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → ∀ i, l₁.drop i <+ l₂.drop i
   | _, _, h, 0 => h
   | _, _, h, i + 1 => by rw [← drop_tail, ← drop_tail]; exact h.tail.drop i
 
 /-! ### IsPrefix / IsSuffix / IsInfix -/
 
-@[simp] theorem prefix_append (l₁ l₂ : List α) : l₁ <+: l₁ ++ l₂ := ⟨l₂, rfl⟩
+@[simp, grind] theorem prefix_append (l₁ l₂ : List α) : l₁ <+: l₁ ++ l₂ := ⟨l₂, rfl⟩
 
-@[simp] theorem suffix_append (l₁ l₂ : List α) : l₂ <:+ l₁ ++ l₂ := ⟨l₁, rfl⟩
+@[simp, grind] 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
+@[simp, grind] theorem infix_append' (l₁ l₂ l₃ : List α) : l₂ <:+: l₁ ++ (l₂ ++ l₃) := by
   rw [← List.append_assoc]; apply infix_append
 
+theorem infix_append_left : l₁ <:+: l₁ ++ l₂ := ⟨[], l₂, rfl⟩
+theorem infix_append_right : l₂ <:+: l₁ ++ l₂ := ⟨l₁, [], by simp⟩
+
 theorem IsPrefix.isInfix : l₁ <+: l₂ → l₁ <:+: l₂ := fun ⟨t, h⟩ => ⟨[], t, h⟩
 
+grind_pattern IsPrefix.isInfix => l₁ <+: l₂, IsInfix
+
 theorem IsSuffix.isInfix : l₁ <:+ l₂ → l₁ <:+: l₂ := fun ⟨t, h⟩ => ⟨t, [], by rw [h, append_nil]⟩
 
-@[simp] theorem nil_prefix {l : List α} : [] <+: l := ⟨l, rfl⟩
+grind_pattern IsSuffix.isInfix => l₁ <:+ l₂, IsInfix
 
-@[simp] theorem nil_suffix {l : List α} : [] <:+ l := ⟨l, append_nil _⟩
+@[simp, grind] theorem nil_prefix {l : List α} : [] <+: l := ⟨l, rfl⟩
 
-@[simp] theorem nil_infix {l : List α} : [] <:+: l := nil_prefix.isInfix
+@[simp, grind] theorem nil_suffix {l : List α} : [] <:+ l := ⟨l, append_nil _⟩
+
+@[simp, grind] theorem nil_infix {l : List α} : [] <:+: l := nil_prefix.isInfix
 
 theorem prefix_refl (l : List α) : l <+: l := ⟨[], append_nil _⟩
-@[simp] theorem prefix_rfl {l : List α} : l <+: l := prefix_refl l
+@[simp, grind] theorem prefix_rfl {l : List α} : l <+: l := prefix_refl l
 
 theorem suffix_refl (l : List α) : l <:+ l := ⟨[], rfl⟩
-@[simp] theorem suffix_rfl {l : List α} : l <:+ l := suffix_refl l
+@[simp, grind] theorem suffix_rfl {l : List α} : l <:+ l := suffix_refl l
 
 theorem infix_refl (l : List α) : l <:+: l := prefix_rfl.isInfix
-@[simp] theorem infix_rfl {l : List α} : l <:+: l := infix_refl l
+@[simp, grind] theorem infix_rfl {l : List α} : l <:+: l := infix_refl l
 
-@[simp] theorem suffix_cons (a : α) : ∀ l, l <:+ a :: l := suffix_append [a]
+@[simp, grind] 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⟩
 
@@ -617,12 +656,38 @@ theorem infix_concat : l₁ <:+: l₂ → l₁ <:+: concat l₂ a := fun ⟨l₁
 theorem IsPrefix.trans : ∀ {l₁ l₂ l₃ : List α}, l₁ <+: l₂ → l₂ <+: l₃ → l₁ <+: l₃
   | _, _, _, ⟨r₁, rfl⟩, ⟨r₂, rfl⟩ => ⟨r₁ ++ r₂, (append_assoc _ _ _).symm⟩
 
+grind_pattern IsPrefix.trans => l₁ <+: l₂, l₂ <+: l₃
+
 theorem IsSuffix.trans : ∀ {l₁ l₂ l₃ : List α}, l₁ <:+ l₂ → l₂ <:+ l₃ → l₁ <:+ l₃
   | _, _, _, ⟨l₁, rfl⟩, ⟨l₂, rfl⟩ => ⟨l₂ ++ l₁, append_assoc _ _ _⟩
 
+grind_pattern IsSuffix.trans => l₁ <:+ l₂, l₂ <:+ l₃
+
 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]⟩
 
+grind_pattern IsInfix.trans => l₁ <:+: l₂, l₂ <:+: l₃
+
+theorem prefix_append_of_prefix (h : l₁ <+: l₂) : l₁ <+: l₂ ++ l₃ :=
+  h.trans (prefix_append l₂ l₃)
+
+grind_pattern prefix_append_of_prefix => l₁ <+: l₂, l₂ ++ l₃
+
+theorem suffix_append_of_suffix (h : l₁ <:+ l₃) : l₁ <:+ l₂ ++ l₃ :=
+  h.trans (suffix_append l₂ l₃)
+
+grind_pattern suffix_append_of_suffix => l₁ <:+ l₃, l₂ ++ l₃
+
+theorem infix_append_of_infix_left (h : l₁ <:+: l₂) : l₁ <:+: l₂ ++ l₃ :=
+  h.trans infix_append_left
+
+grind_pattern infix_append_of_infix_left => l₁ <:+: l₂, l₂ ++ l₃
+
+theorem infix_append_of_infix_right (h : l₁ <:+: l₃) : l₁ <:+: l₂ ++ l₃ :=
+  h.trans infix_append_right
+
+grind_pattern infix_append_of_infix_right => l₁ <:+: l₃, l₂ ++ l₃
+
 protected theorem IsInfix.sublist : l₁ <:+: l₂ → l₁ <+ l₂
   | ⟨_, _, h⟩ => h ▸ (sublist_append_right ..).trans (sublist_append_left ..)
 
@@ -641,11 +706,11 @@ protected theorem IsSuffix.sublist (h : l₁ <:+ l₂) : l₁ <+ l₂ :=
 protected theorem IsSuffix.subset (hl : l₁ <:+ l₂) : l₁ ⊆ l₂ :=
   hl.sublist.subset
 
-@[simp] theorem infix_nil : l <:+: [] ↔ l = [] := ⟨(sublist_nil.1 ·.sublist), (· ▸ infix_rfl)⟩
+@[simp, grind =] theorem infix_nil : l <:+: [] ↔ l = [] := ⟨(sublist_nil.1 ·.sublist), (· ▸ infix_rfl)⟩
 
-@[simp] theorem prefix_nil : l <+: [] ↔ l = [] := ⟨(sublist_nil.1 ·.sublist), (· ▸ prefix_rfl)⟩
+@[simp, grind =] theorem prefix_nil : l <+: [] ↔ l = [] := ⟨(sublist_nil.1 ·.sublist), (· ▸ prefix_rfl)⟩
 
-@[simp] theorem suffix_nil : l <:+ [] ↔ l = [] := ⟨(sublist_nil.1 ·.sublist), (· ▸ suffix_rfl)⟩
+@[simp, grind =] theorem suffix_nil : l <:+ [] ↔ l = [] := ⟨(sublist_nil.1 ·.sublist), (· ▸ suffix_rfl)⟩
 
 theorem eq_nil_of_infix_nil (h : l <:+: []) : l = [] := infix_nil.mp h
 theorem eq_nil_of_prefix_nil (h : l <+: []) : l = [] := prefix_nil.mp h
@@ -676,23 +741,23 @@ theorem IsPrefix.getElem {xs ys : List α} (h : xs <+: ys) {i} (hi : i < xs.leng
 
 -- See `Init.Data.List.Nat.Sublist` for `IsSuffix.getElem`.
 
-theorem IsPrefix.mem (hx : a ∈ l₁) (hl : l₁ <+: l₂) : a ∈ l₂ :=
+@[grind →] theorem IsPrefix.mem (hx : a ∈ l₁) (hl : l₁ <+: l₂) : a ∈ l₂ :=
   hl.subset hx
 
-theorem IsSuffix.mem (hx : a ∈ l₁) (hl : l₁ <:+ l₂) : a ∈ l₂ :=
+@[grind →] theorem IsSuffix.mem (hx : a ∈ l₁) (hl : l₁ <:+ l₂) : a ∈ l₂ :=
   hl.subset hx
 
-theorem IsInfix.mem (hx : a ∈ l₁) (hl : l₁ <:+: l₂) : a ∈ l₂ :=
+@[grind →] theorem IsInfix.mem (hx : a ∈ l₁) (hl : l₁ <:+: l₂) : a ∈ l₂ :=
   hl.subset hx
 
-@[simp] theorem reverse_suffix : reverse l₁ <:+ reverse l₂ ↔ l₁ <+: l₂ :=
+@[simp, grind =] 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
+@[simp, grind =] 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
+@[simp, grind =] 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]
@@ -701,12 +766,21 @@ theorem IsInfix.mem (hx : a ∈ l₁) (hl : l₁ <:+: l₂) : a ∈ l₂ :=
 theorem IsInfix.reverse : l₁ <:+: l₂ → reverse l₁ <:+: reverse l₂ :=
   reverse_infix.2
 
+grind_pattern IsInfix.reverse => l₁ <:+: l₂, l₁.reverse
+grind_pattern IsInfix.reverse => l₁ <:+: l₂, l₂.reverse
+
 theorem IsSuffix.reverse : l₁ <:+ l₂ → reverse l₁ <+: reverse l₂ :=
   reverse_prefix.2
 
+grind_pattern IsSuffix.reverse => l₁ <:+ l₂, l₁.reverse
+grind_pattern IsSuffix.reverse => l₁ <:+ l₂, l₂.reverse
+
 theorem IsPrefix.reverse : l₁ <+: l₂ → reverse l₁ <:+ reverse l₂ :=
   reverse_suffix.2
 
+grind_pattern IsPrefix.reverse => l₁ <+: l₂, l₁.reverse
+grind_pattern IsPrefix.reverse => l₁ <+: l₂, l₂.reverse
+
 theorem IsPrefix.head {l₁ l₂ : List α} (h : l₁ <+: l₂) (hx : l₁ ≠ []) :
     l₁.head hx = l₂.head (h.ne_nil hx) := by
   cases l₁ <;> cases l₂ <;> simp only [head_cons, ne_eq, not_true_eq_false] at hx ⊢
@@ -780,7 +854,7 @@ theorem prefix_cons_iff : l₁ <+: a :: l₂ ↔ l₁ = [] ∨ ∃ t, l₁ = a :
       · simp only [w]
         refine ⟨s, by simp [h']⟩
 
-@[simp] theorem cons_prefix_cons : a :: l₁ <+: b :: l₂ ↔ a = b ∧ l₁ <+: l₂ := by
+@[simp, grind =] theorem cons_prefix_cons : a :: l₁ <+: b :: l₂ ↔ a = b ∧ l₁ <+: l₂ := by
   simp only [prefix_cons_iff, cons.injEq, false_or, List.cons_ne_nil]
   constructor
   · rintro ⟨t, ⟨rfl, rfl⟩, h⟩
@@ -831,7 +905,7 @@ theorem infix_concat_iff {l₁ l₂ : List α} {a : α} :
   rw [← reverse_infix, reverse_concat, infix_cons_iff, reverse_infix,
     ← reverse_prefix, reverse_concat]
 
-theorem isPrefix_iff : l₁ <+: l₂ ↔ ∀ i (h : i < l₁.length), l₂[i]? = some l₁[i] := by
+theorem prefix_iff_getElem? : l₁ <+: l₂ ↔ ∀ i (h : i < l₁.length), l₂[i]? = some l₁[i] := by
   induction l₁ generalizing l₂ with
   | nil => simp
   | cons a l₁ ih =>
@@ -843,7 +917,12 @@ theorem isPrefix_iff : l₁ <+: l₂ ↔ ∀ i (h : i < l₁.length), l₂[i]? =
       rw (occs := [2]) [← Nat.and_forall_add_one]
       simp [Nat.succ_lt_succ_iff, eq_comm]
 
-theorem isPrefix_iff_getElem {l₁ l₂ : List α} :
+-- See `Init.Data.List.Nat.Sublist` for `isSuffix_iff` and `ifInfix_iff`.
+
+@[deprecated prefix_iff_getElem? (since := "2025-05-27")]
+abbrev isPrefix_iff := @prefix_iff_getElem?
+
+theorem prefix_iff_getElem {l₁ l₂ : List α} :
     l₁ <+: l₂ ↔ ∃ (h : l₁.length ≤ l₂.length), ∀ i (hx : i < l₁.length),
       l₁[i] = l₂[i]'(Nat.lt_of_lt_of_le hx h) where
   mp h := ⟨h.length_le, fun _ h' ↦ h.getElem h'⟩
@@ -861,9 +940,16 @@ theorem isPrefix_iff_getElem {l₁ l₂ : List α} :
         simp only [cons_prefix_cons]
         exact ⟨h 0 (zero_lt_succ _), tail_ih hl fun a ha ↦ h a.succ (succ_lt_succ ha)⟩
 
--- See `Init.Data.List.Nat.Sublist` for `isSuffix_iff` and `ifInfix_iff`.
+@[deprecated prefix_iff_getElem (since := "2025-05-27")]
+abbrev isPrefix_iff_getElem := @prefix_iff_getElem
 
-theorem isPrefix_filterMap_iff {β} {f : α → Option β} {l₁ : List α} {l₂ : List β} :
+theorem cons_prefix_iff {a : α} {l₁ l₂ : List α} :
+    a :: l₁ <+: l₂ ↔ ∃ l', l₂ = a :: l' ∧ l₁ <+: l' := by
+  match l₂ with
+  | nil => simp
+  | cons b l₂ => simp [and_assoc, eq_comm]
+
+theorem prefix_filterMap_iff {β} {f : α → Option β} {l₁ : List α} {l₂ : List β} :
     l₂ <+: filterMap f l₁ ↔ ∃ l, l <+: l₁ ∧ l₂ = filterMap f l := by
   simp only [IsPrefix, append_eq_filterMap_iff]
   constructor
@@ -872,7 +958,10 @@ theorem isPrefix_filterMap_iff {β} {f : α → Option β} {l₁ : List α} {l
   · rintro ⟨l₁, ⟨l₂, rfl⟩, rfl⟩
     exact ⟨_, l₁, l₂, rfl, rfl, rfl⟩
 
-theorem isSuffix_filterMap_iff {β} {f : α → Option β} {l₁ : List α} {l₂ : List β} :
+@[deprecated prefix_filterMap_iff (since := "2025-05-27")]
+abbrev isPrefix_filterMap_iff := @prefix_filterMap_iff
+
+theorem suffix_filterMap_iff {β} {f : α → Option β} {l₁ : List α} {l₂ : List β} :
     l₂ <:+ filterMap f l₁ ↔ ∃ l, l <:+ l₁ ∧ l₂ = filterMap f l := by
   simp only [IsSuffix, append_eq_filterMap_iff]
   constructor
@@ -881,7 +970,10 @@ theorem isSuffix_filterMap_iff {β} {f : α → Option β} {l₁ : List α} {l
   · rintro ⟨l₁, ⟨l₂, rfl⟩, rfl⟩
     exact ⟨_, l₂, l₁, rfl, rfl, rfl⟩
 
-theorem isInfix_filterMap_iff {β} {f : α → Option β} {l₁ : List α} {l₂ : List β} :
+@[deprecated suffix_filterMap_iff (since := "2025-05-27")]
+abbrev isSuffix_filterMap_iff := @suffix_filterMap_iff
+
+theorem infix_filterMap_iff {β} {f : α → Option β} {l₁ : List α} {l₂ : List β} :
     l₂ <:+: filterMap f l₁ ↔ ∃ l, l <:+: l₁ ∧ l₂ = filterMap f l := by
   simp only [IsInfix, append_eq_filterMap_iff, filterMap_eq_append_iff]
   constructor
@@ -890,31 +982,52 @@ theorem isInfix_filterMap_iff {β} {f : α → Option β} {l₁ : List α} {l₂
   · rintro ⟨l₃, ⟨l₂, l₁, rfl⟩, rfl⟩
     exact ⟨_, _, _, l₁, rfl, ⟨⟨l₂, l₃, rfl, rfl, rfl⟩, rfl⟩⟩
 
-theorem isPrefix_filter_iff {p : α → Bool} {l₁ l₂ : List α} :
+@[deprecated infix_filterMap_iff (since := "2025-05-27")]
+abbrev isInfix_filterMap_iff := @infix_filterMap_iff
+
+theorem prefix_filter_iff {p : α → Bool} {l₁ l₂ : List α} :
     l₂ <+: l₁.filter p ↔ ∃ l, l <+: l₁ ∧ l₂ = l.filter p := by
-  rw [← filterMap_eq_filter, isPrefix_filterMap_iff]
+  rw [← filterMap_eq_filter, prefix_filterMap_iff]
 
-theorem isSuffix_filter_iff {p : α → Bool} {l₁ l₂ : List α} :
+@[deprecated prefix_filter_iff (since := "2025-05-27")]
+abbrev isPrefix_filter_iff := @prefix_filter_iff
+
+theorem suffix_filter_iff {p : α → Bool} {l₁ l₂ : List α} :
     l₂ <:+ l₁.filter p ↔ ∃ l, l <:+ l₁ ∧ l₂ = l.filter p := by
-  rw [← filterMap_eq_filter, isSuffix_filterMap_iff]
+  rw [← filterMap_eq_filter, suffix_filterMap_iff]
 
-theorem isInfix_filter_iff {p : α → Bool} {l₁ l₂ : List α} :
+@[deprecated suffix_filter_iff (since := "2025-05-27")]
+abbrev isSuffix_filter_iff := @suffix_filter_iff
+
+theorem infix_filter_iff {p : α → Bool} {l₁ l₂ : List α} :
     l₂ <:+: l₁.filter p ↔ ∃ l, l <:+: l₁ ∧ l₂ = l.filter p := by
-  rw [← filterMap_eq_filter, isInfix_filterMap_iff]
+  rw [← filterMap_eq_filter, infix_filterMap_iff]
 
-theorem isPrefix_map_iff {β} {f : α → β} {l₁ : List α} {l₂ : List β} :
+@[deprecated infix_filter_iff (since := "2025-05-27")]
+abbrev isInfix_filter_iff := @infix_filter_iff
+
+theorem prefix_map_iff {β} {f : α → β} {l₁ : List α} {l₂ : List β} :
     l₂ <+: l₁.map f ↔ ∃ l, l <+: l₁ ∧ l₂ = l.map f := by
-  rw [← filterMap_eq_map, isPrefix_filterMap_iff]
+  rw [← filterMap_eq_map, prefix_filterMap_iff]
 
-theorem isSuffix_map_iff {β} {f : α → β} {l₁ : List α} {l₂ : List β} :
+@[deprecated prefix_map_iff (since := "2025-05-27")]
+abbrev isPrefix_map_iff := @prefix_map_iff
+
+theorem suffix_map_iff {β} {f : α → β} {l₁ : List α} {l₂ : List β} :
     l₂ <:+ l₁.map f ↔ ∃ l, l <:+ l₁ ∧ l₂ = l.map f := by
-  rw [← filterMap_eq_map, isSuffix_filterMap_iff]
+  rw [← filterMap_eq_map, suffix_filterMap_iff]
 
-theorem isInfix_map_iff {β} {f : α → β} {l₁ : List α} {l₂ : List β} :
+@[deprecated suffix_map_iff (since := "2025-05-27")]
+abbrev isSuffix_map_iff := @suffix_map_iff
+
+theorem infix_map_iff {β} {f : α → β} {l₁ : List α} {l₂ : List β} :
     l₂ <:+: l₁.map f ↔ ∃ l, l <:+: l₁ ∧ l₂ = l.map f := by
-  rw [← filterMap_eq_map, isInfix_filterMap_iff]
+  rw [← filterMap_eq_map, infix_filterMap_iff]
 
-theorem isPrefix_replicate_iff {n} {a : α} {l : List α} :
+@[deprecated infix_map_iff (since := "2025-05-27")]
+abbrev isInfix_map_iff := @infix_map_iff
+
+@[grind =] theorem prefix_replicate_iff {n} {a : α} {l : List α} :
     l <+: List.replicate n a ↔ l.length ≤ n ∧ l = List.replicate l.length a := by
   rw [IsPrefix]
   simp only [append_eq_replicate_iff]
@@ -926,12 +1039,18 @@ theorem isPrefix_replicate_iff {n} {a : α} {l : List α} :
     · simpa using add_sub_of_le h
     · simpa using w
 
-theorem isSuffix_replicate_iff {n} {a : α} {l : List α} :
+@[deprecated prefix_replicate_iff (since := "2025-05-27")]
+abbrev isPrefix_replicate_iff := @prefix_replicate_iff
+
+@[grind =] theorem suffix_replicate_iff {n} {a : α} {l : List α} :
     l <:+ List.replicate n a ↔ l.length ≤ n ∧ l = List.replicate l.length a := by
-  rw [← reverse_prefix, reverse_replicate, isPrefix_replicate_iff]
+  rw [← reverse_prefix, reverse_replicate, prefix_replicate_iff]
   simp [reverse_eq_iff]
 
-theorem isInfix_replicate_iff {n} {a : α} {l : List α} :
+@[deprecated suffix_replicate_iff (since := "2025-05-27")]
+abbrev isSuffix_replicate_iff := @suffix_replicate_iff
+
+@[grind =] theorem infix_replicate_iff {n} {a : α} {l : List α} :
     l <:+: List.replicate n a ↔ l.length ≤ n ∧ l = List.replicate l.length a := by
   rw [IsInfix]
   simp only [append_eq_replicate_iff, length_append]
@@ -943,6 +1062,9 @@ theorem isInfix_replicate_iff {n} {a : α} {l : List α} :
     · simpa using Nat.sub_add_cancel h
     · simpa using w
 
+@[deprecated infix_replicate_iff (since := "2025-05-27")]
+abbrev isInfix_replicate_iff := @infix_replicate_iff
+
 theorem infix_of_mem_flatten : ∀ {L : List (List α)}, l ∈ L → l <:+: flatten L
   | l' :: _, h =>
     match h with
@@ -956,16 +1078,16 @@ theorem infix_of_mem_flatten : ∀ {L : List (List α)}, l ∈ L → l <:+: flat
 theorem prefix_cons_inj (a) : a :: l₁ <+: a :: l₂ ↔ l₁ <+: l₂ :=
   prefix_append_right_inj [a]
 
-theorem take_prefix (i) (l : List α) : take i l <+: l :=
+@[grind] theorem take_prefix (i) (l : List α) : take i l <+: l :=
   ⟨_, take_append_drop _ _⟩
 
-theorem drop_suffix (i) (l : List α) : drop i l <:+ l :=
+@[grind] theorem drop_suffix (i) (l : List α) : drop i l <:+ l :=
   ⟨_, take_append_drop _ _⟩
 
-theorem take_sublist (i) (l : List α) : take i l <+ l :=
+@[grind] theorem take_sublist (i) (l : List α) : take i l <+ l :=
   (take_prefix i l).sublist
 
-theorem drop_sublist (i) (l : List α) : drop i l <+ l :=
+@[grind] theorem drop_sublist (i) (l : List α) : drop i l <+ l :=
   (drop_suffix i l).sublist
 
 theorem take_subset (i) (l : List α) : take i l ⊆ l :=
@@ -986,22 +1108,22 @@ theorem drop_suffix_drop_left (l : List α) {i j : Nat} (h : i ≤ j) : drop j l
 
 -- See `Init.Data.List.Nat.TakeDrop` for `take_prefix_take_left`.
 
-theorem drop_sublist_drop_left (l : List α) {i j : Nat} (h : i ≤ j) : drop j l <+ drop i l :=
+@[grind] theorem drop_sublist_drop_left (l : List α) {i j : Nat} (h : i ≤ j) : drop j l <+ drop i l :=
   (drop_suffix_drop_left l h).sublist
 
-theorem drop_subset_drop_left (l : List α) {i j : Nat} (h : i ≤ j) : drop j l ⊆ drop i l :=
+@[grind] theorem drop_subset_drop_left (l : List α) {i j : Nat} (h : i ≤ j) : drop j l ⊆ drop i l :=
   (drop_sublist_drop_left l h).subset
 
-theorem takeWhile_prefix (p : α → Bool) : l.takeWhile p <+: l :=
+@[grind] theorem takeWhile_prefix (p : α → Bool) : l.takeWhile p <+: l :=
   ⟨l.dropWhile p, takeWhile_append_dropWhile⟩
 
-theorem dropWhile_suffix (p : α → Bool) : l.dropWhile p <:+ l :=
+@[grind] theorem dropWhile_suffix (p : α → Bool) : l.dropWhile p <:+ l :=
   ⟨l.takeWhile p, takeWhile_append_dropWhile⟩
 
-theorem takeWhile_sublist (p : α → Bool) : l.takeWhile p <+ l :=
+@[grind] theorem takeWhile_sublist (p : α → Bool) : l.takeWhile p <+ l :=
   (takeWhile_prefix p).sublist
 
-theorem dropWhile_sublist (p : α → Bool) : l.dropWhile p <+ l :=
+@[grind] theorem dropWhile_sublist (p : α → Bool) : l.dropWhile p <+ l :=
   (dropWhile_suffix p).sublist
 
 theorem takeWhile_subset {l : List α} (p : α → Bool) : l.takeWhile p ⊆ l :=
@@ -1010,61 +1132,61 @@ theorem takeWhile_subset {l : List α} (p : α → Bool) : l.takeWhile p ⊆ l :
 theorem dropWhile_subset {l : List α} (p : α → Bool) : l.dropWhile p ⊆ l :=
   (dropWhile_sublist p).subset
 
-theorem dropLast_prefix : ∀ l : List α, l.dropLast <+: l
+@[grind] theorem dropLast_prefix : ∀ l : List α, l.dropLast <+: l
   | [] => ⟨nil, by rw [dropLast, List.append_nil]⟩
   | a :: l => ⟨_, dropLast_concat_getLast (cons_ne_nil a l)⟩
 
-theorem dropLast_sublist (l : List α) : l.dropLast <+ l :=
+@[grind] theorem dropLast_sublist (l : List α) : l.dropLast <+ l :=
   (dropLast_prefix l).sublist
 
 theorem dropLast_subset (l : List α) : l.dropLast ⊆ l :=
   (dropLast_sublist l).subset
 
-theorem tail_suffix (l : List α) : tail l <:+ l := by rw [← drop_one]; apply drop_suffix
+@[grind] theorem tail_suffix (l : List α) : tail l <:+ l := by rw [← drop_one]; apply drop_suffix
 
-theorem IsPrefix.map {β} (f : α → β) ⦃l₁ l₂ : List α⦄ (h : l₁ <+: l₂) : l₁.map f <+: l₂.map f := by
+@[grind] theorem IsPrefix.map {β} (f : α → β) ⦃l₁ l₂ : List α⦄ (h : l₁ <+: l₂) : l₁.map f <+: l₂.map f := by
   obtain ⟨r, rfl⟩ := h
   rw [map_append]; apply prefix_append
 
-theorem IsSuffix.map {β} (f : α → β) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+ l₂) : l₁.map f <:+ l₂.map f := by
+@[grind] theorem IsSuffix.map {β} (f : α → β) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+ l₂) : l₁.map f <:+ l₂.map f := by
   obtain ⟨r, rfl⟩ := h
   rw [map_append]; apply suffix_append
 
-theorem IsInfix.map {β} (f : α → β) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+: l₂) : l₁.map f <:+: l₂.map f := by
+@[grind] theorem IsInfix.map {β} (f : α → β) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+: l₂) : l₁.map f <:+: l₂.map f := by
   obtain ⟨r₁, r₂, rfl⟩ := h
   rw [map_append, map_append]; apply infix_append
 
-theorem IsPrefix.filter (p : α → Bool) ⦃l₁ l₂ : List α⦄ (h : l₁ <+: l₂) :
+@[grind] 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₂) :
+@[grind] 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₂) :
+@[grind] 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 _
 
-theorem IsPrefix.filterMap {β} (f : α → Option β) ⦃l₁ l₂ : List α⦄ (h : l₁ <+: l₂) :
+@[grind] theorem IsPrefix.filterMap {β} (f : α → Option β) ⦃l₁ l₂ : List α⦄ (h : l₁ <+: l₂) :
     filterMap f l₁ <+: filterMap f l₂ := by
   obtain ⟨xs, rfl⟩ := h
   rw [filterMap_append]; apply prefix_append
 
-theorem IsSuffix.filterMap {β} (f : α → Option β) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+ l₂) :
+@[grind] theorem IsSuffix.filterMap {β} (f : α → Option β) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+ l₂) :
     filterMap f l₁ <:+ filterMap f l₂ := by
   obtain ⟨xs, rfl⟩ := h
   rw [filterMap_append]; apply suffix_append
 
-theorem IsInfix.filterMap {β} (f : α → Option β) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+: l₂) :
+@[grind] theorem IsInfix.filterMap {β} (f : α → Option β) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+: l₂) :
     filterMap f l₁ <:+: filterMap f l₂ := by
   obtain ⟨xs, ys, rfl⟩ := h
   rw [filterMap_append, filterMap_append]; apply infix_append
 
-@[simp] theorem isPrefixOf_iff_prefix [BEq α] [LawfulBEq α] {l₁ l₂ : List α} :
+@[simp, grind =] theorem isPrefixOf_iff_prefix [BEq α] [LawfulBEq α] {l₁ l₂ : List α} :
     l₁.isPrefixOf l₂ ↔ l₁ <+: l₂ := by
   induction l₁ generalizing l₂ with
   | nil => simp
@@ -1076,7 +1198,7 @@ theorem IsInfix.filterMap {β} (f : α → Option β) ⦃l₁ l₂ : List α⦄
 instance [DecidableEq α] (l₁ l₂ : List α) : Decidable (l₁ <+: l₂) :=
   decidable_of_iff (l₁.isPrefixOf l₂) isPrefixOf_iff_prefix
 
-@[simp] theorem isSuffixOf_iff_suffix [BEq α] [LawfulBEq α] {l₁ l₂ : List α} :
+@[simp, grind =] theorem isSuffixOf_iff_suffix [BEq α] [LawfulBEq α] {l₁ l₂ : List α} :
     l₁.isSuffixOf l₂ ↔ l₁ <:+ l₂ := by
   simp [isSuffixOf]
 

tests/lean/grind/sublist.lean

@@ -0,0 +1,19 @@
+open List
+
+set_option grind.warning false
+
+example (h : zs <+ ys) (w : xs ++ ys <+ zs) (h' : ¬xs = []) : False := by
+  fail_if_success grind
+  -- I'm not sure how to make progress here without manually adding that since `xs ≠ []`, it must be a `cons`.
+  have : ∃ y ys, xs = y :: ys := match xs, h' with | _ :: _, _ => by simp
+  grind (gen := 6)
+
+example {xs ys zs : List α} (h : zs <+ ys) :
+    xs ++ ys <+ zs ↔ xs = [] ∧ ys = zs := by
+  constructor
+  · intro w
+    grind -- stuck, because of the failure of the example above.
+    -- An alternative idea would be to argue via inequalities about lengths,
+    -- but any grind pattern for `Sublist.length_le` seems to result in an explosion of useless facts.
+  · intro w
+    grind

tests/lean/run/grind_list_sublist.lean

@@ -0,0 +1,40 @@
+open List
+
+set_option grind.warning false
+
+variable {α} {l₁ l₂ l₃ l₄ l₅ : List α}
+
+example : l₂ ++ l₄ ⊆ l₁ ++ l₂ ++ l₃ ++ l₄ ++ l₅ := by
+  grind
+
+example : l₂ ++ l₄ <+ l₁ ++ l₂ ++ l₃ ++ l₄ ++ l₅ := by
+  grind
+
+example : l₁ ++ l₂ <+: l₁ ++ (l₂ ++ l₃) := by
+  grind
+
+example : l₂ ++ l₃ <:+ l₁ ++ l₂ ++ l₃ := by
+  grind
+
+example : l₂ ++ l₃ <:+: l₁ ++ l₂ ++ l₃ ++ l₄ := by
+  grind
+
+example (h : l₁ <:+: l₂) : l₁.filter p <:+: (l₂ ++ l₃).filter p := by
+  grind
+
+example (h : l₁ <+: l₂) : l₁.map f <+: (l₂ ++ l₃).map f := by
+  grind
+
+example (h : l₁ <+: l₂) : l₁.reverse <:+ xs ++ l₂.reverse := by grind
+
+example (h : l₁ <+: l₂) : l₁.reverse <:+: xs ++ l₂.reverse := by grind
+
+example (h : l₁ <:+: l₂) : l₁.reverse <:+: xs ++ l₂.reverse ++ ys := by grind
+
+example (h : 8 ≤ xs.count 37) : replicate 7 37 <+ xs := by grind
+
+-- Can we do this without unfolding `IsSuffix`?
+example (h : replicate (n + 1) 37 <:+ xs) : n ≤ xs.count 37 := by grind [IsSuffix]
+
+-- Can we do this without unfolding `IsInfix`?
+example (h : replicate (n + 1) 37 <:+: xs) : n ≤ 2 * xs.count 37 := by grind [IsInfix]