feat(List): add lemmas about Sublist (#12326)

- Move `tail_sublist` to `Basic`
- Rename `sublist_of_cons_sublist_cons` to `Sublist.of_cons_cos`
- Rename `cons_sublist_cons_iff` to `cons_sublist_cons`
- Add `Sublist.tail`, `drop_sublist_drop_left`, `Sublist.drop`
- Protect some lemmas

Author: urkud

Mathlib/Data/List/Basic.lean

@@ -1026,13 +1026,25 @@ theorem sublist_cons_of_sublist (a : α) (h : l₁ <+ l₂) : l₁ <+ a :: l₂
 #align list.sublist_append_of_sublist_left List.sublist_append_of_sublist_left
 #align list.sublist_append_of_sublist_right List.sublist_append_of_sublist_right
 
-theorem sublist_of_cons_sublist_cons {l₁ l₂ : List α} : ∀ {a : α}, a :: l₁ <+ a :: l₂ → l₁ <+ l₂
-  | _, Sublist.cons _ s => sublist_of_cons_sublist s
-  | _, Sublist.cons₂ _ s => s
-#align list.sublist_of_cons_sublist_cons List.sublist_of_cons_sublist_cons
+theorem tail_sublist : ∀ l : List α, tail l <+ l
+  | [] => .slnil
+  | a::l => sublist_cons a l
+#align list.tail_sublist List.tail_sublist
 
-theorem cons_sublist_cons_iff {l₁ l₂ : List α} {a : α} : a :: l₁ <+ a :: l₂ ↔ l₁ <+ l₂ :=
-  ⟨sublist_of_cons_sublist_cons, Sublist.cons_cons _⟩
+@[gcongr] 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
+
+theorem Sublist.of_cons_cons {l₁ l₂ : List α} {a b : α} (h : a :: l₁ <+ b :: l₂) : l₁ <+ l₂ :=
+  h.tail
+#align list.sublist_of_cons_sublist_cons List.Sublist.of_cons_cons
+
+@[deprecated] -- 2024-04-07
+theorem sublist_of_cons_sublist_cons {a} (h : a :: l₁ <+ a :: l₂) : l₁ <+ l₂ := h.of_cons_cons
+
+attribute [simp] cons_sublist_cons
+@[deprecated] alias cons_sublist_cons_iff := cons_sublist_cons -- 2024-04-07
 #align list.cons_sublist_cons_iff List.cons_sublist_cons_iff
 
 #align list.append_sublist_append_left List.append_sublist_append_left

Mathlib/Data/List/Chain.lean

@@ -6,6 +6,7 @@ Authors: Mario Carneiro, Kenny Lau, Yury Kudryashov
 import Mathlib.Logic.Relation
 import Mathlib.Data.List.Forall2
 import Mathlib.Data.List.Lex
+import Mathlib.Data.List.Infix
 
 #align_import data.list.chain from "leanprover-community/mathlib"@"dd71334db81d0bd444af1ee339a29298bef40734"
 

Mathlib/Data/List/Duplicate.lean

@@ -118,7 +118,7 @@ theorem duplicate_iff_sublist : x ∈+ l ↔ [x, x] <+ l := by
   induction' l with y l IH
   · simp
   · by_cases hx : x = y
-    · simp [hx, cons_sublist_cons_iff, singleton_sublist]
+    · simp [hx, cons_sublist_cons, singleton_sublist]
     · rw [duplicate_cons_iff_of_ne hx, IH]
       refine' ⟨sublist_cons_of_sublist y, fun h => _⟩
       cases h

Mathlib/Data/List/Forall2.lean

@@ -3,7 +3,7 @@ Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Johannes Hölzl
 -/
-import Mathlib.Data.List.Infix
+import Mathlib.Data.List.Basic
 
 #align_import data.list.forall2 from "leanprover-community/mathlib"@"5a3e819569b0f12cbec59d740a2613018e7b8eec"
 

Mathlib/Data/List/Infix.lean

@@ -90,13 +90,13 @@ theorem prefix_concat_iff {l₁ l₂ : List α} {a : α} :
 #align list.reverse_prefix List.reverse_prefix
 #align list.reverse_infix List.reverse_infix
 
-alias ⟨_, isSuffix.reverse⟩ := reverse_prefix
+protected alias ⟨_, isSuffix.reverse⟩ := reverse_prefix
 #align list.is_suffix.reverse List.isSuffix.reverse
 
-alias ⟨_, isPrefix.reverse⟩ := reverse_suffix
+protected alias ⟨_, isPrefix.reverse⟩ := reverse_suffix
 #align list.is_prefix.reverse List.isPrefix.reverse
 
-alias ⟨_, isInfix.reverse⟩ := reverse_infix
+protected alias ⟨_, isInfix.reverse⟩ := reverse_infix
 #align list.is_infix.reverse List.isInfix.reverse
 
 #align list.is_infix.length_le List.IsInfix.length_le
@@ -182,9 +182,10 @@ theorem dropLast_sublist (l : List α) : l.dropLast <+ l :=
   (dropLast_prefix l).sublist
 #align list.init_sublist List.dropLast_sublist
 
-theorem tail_sublist (l : List α) : l.tail <+ l :=
-  (tail_suffix l).sublist
-#align list.tail_sublist List.tail_sublist
+@[gcongr]
+theorem drop_sublist_drop_left (l : List α) {m n : ℕ} (h : m ≤ n) : drop n l <+ drop m l := by
+  rw [← Nat.sub_add_cancel h, drop_add]
+  apply drop_sublist
 
 theorem dropLast_subset (l : List α) : l.dropLast ⊆ l :=
   (dropLast_sublist l).subset
@@ -202,6 +203,11 @@ theorem mem_of_mem_tail (h : a ∈ l.tail) : a ∈ l :=
   tail_subset l h
 #align list.mem_of_mem_tail List.mem_of_mem_tail
 
+@[gcongr]
+protected theorem Sublist.drop : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → ∀ n, l₁.drop n <+ l₂.drop n
+  | _, _, h, 0 => h
+  | _, _, h, n + 1 => by rw [← drop_tail, ← drop_tail]; exact h.tail.drop n
+
 theorem prefix_iff_eq_append : l₁ <+: l₂ ↔ l₁ ++ drop (length l₁) l₂ = l₂ :=
   ⟨by rintro ⟨r, rfl⟩; rw [drop_left], fun e => ⟨_, e⟩⟩
 #align list.prefix_iff_eq_append List.prefix_iff_eq_append

Mathlib/Data/List/Rotate.lean

@@ -6,6 +6,7 @@ Authors: Chris Hughes, Yakov Pechersky
 import Mathlib.Data.List.Nodup
 import Mathlib.Data.List.Zip
 import Mathlib.Data.Nat.Defs
+import Mathlib.Data.List.Infix
 
 #align_import data.list.rotate from "leanprover-community/mathlib"@"f694c7dead66f5d4c80f446c796a5aad14707f0e"
 

Mathlib/Data/List/Sort.lean

@@ -5,6 +5,7 @@ Authors: Jeremy Avigad
 -/
 import Mathlib.Data.List.OfFn
 import Mathlib.Data.List.Nodup
+import Mathlib.Data.List.Infix
 
 #align_import data.list.sort from "leanprover-community/mathlib"@"f694c7dead66f5d4c80f446c796a5aad14707f0e"