chore: cleanup some List lemmas

Mathlib/Computability/Primrec.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Mathlib.Algebra.Order.Ring.Nat
-import Mathlib.Data.List.GetD
 import Mathlib.Logic.Equiv.List
 import Mathlib.Logic.Function.Iterate
 
@@ -925,9 +924,14 @@ theorem list_get? : Primrec₂ (@List.get? α) :=
       induction' l with _ l IH <;> simp [*]
     · apply IH
 
+theorem list_getElem? : Primrec₂ (fun (l : List α) (n : ℕ) => l[n]?) := by
+  convert list_get?
+  ext
+  simp
+
 theorem list_getD (d : α) : Primrec₂ fun l n => List.getD l n d := by
-  simp only [List.getD_eq_getD_get?]
-  exact option_getD.comp₂ list_get? (const _)
+  simp only [List.getD_eq_getElem?_getD]
+  exact option_getD.comp₂ list_getElem? (const _)
 
 theorem list_getI [Inhabited α] : Primrec₂ (@List.getI α _) :=
   list_getD _

Mathlib/Data/List/Enum.lean

@@ -34,23 +34,22 @@ theorem get_enum (l : List α) (i : Fin l.enum.length) :
     l.enum.get i = (i.1, l.get (i.cast enum_length)) := by
   simp
 
-theorem mk_add_mem_enumFrom_iff_get? {n i : ℕ} {x : α} {l : List α} :
+@[deprecated mk_add_mem_enumFrom_iff_getElem? (since := "2024-08-12")]
+theorem mk_add_mem_enumFrom_iff_get? {n i : Nat} {x : α} {l : List α} :
     (n + i, x) ∈ enumFrom n l ↔ l.get? i = x := by
   simp [mem_iff_get?]
 
-theorem mk_mem_enumFrom_iff_le_and_get?_sub {n i : ℕ} {x : α} {l : List α} :
+@[deprecated mk_mem_enumFrom_iff_le_and_getElem?_sub (since := "2024-08-12")]
+theorem mk_mem_enumFrom_iff_le_and_get?_sub {n i : Nat} {x : α} {l : List α} :
     (i, x) ∈ enumFrom n l ↔ n ≤ i ∧ l.get? (i - n) = x := by
-  if h : n ≤ i then
-    rcases Nat.exists_eq_add_of_le h with ⟨i, rfl⟩
-    simp [mk_add_mem_enumFrom_iff_get?, Nat.add_sub_cancel_left]
-  else
-    have : ∀ k, n + k ≠ i := by rintro k rfl; simp at h
-    simp [h, mem_iff_get?, this]
-
-theorem mk_mem_enum_iff_get? {i : ℕ} {x : α} {l : List α} : (i, x) ∈ enum l ↔ l.get? i = x := by
-  simp [enum, mk_mem_enumFrom_iff_le_and_get?_sub]
-
-theorem mem_enum_iff_get? {x : ℕ × α} {l : List α} : x ∈ enum l ↔ l.get? x.1 = x.2 :=
-  mk_mem_enum_iff_get?
+  simp [mk_mem_enumFrom_iff_le_and_getElem?_sub]
+
+@[deprecated mem_enum_iff_getElem? (since := "2024-08-12")]
+theorem mk_mem_enum_iff_get? {i : Nat} {x : α} {l : List α} : (i, x) ∈ enum l ↔ l.get? i = x := by
+  simp [enum, mk_mem_enumFrom_iff_le_and_getElem?_sub]
+
+@[deprecated mk_mem_enum_iff_getElem? (since := "2024-08-12")]
+theorem mem_enum_iff_get? {x : Nat × α} {l : List α} : x ∈ enum l ↔ l.get? x.1 = x.2 := by
+  simp [mem_enum_iff_getElem?]
 
 end List

Mathlib/Data/List/Infix.lean

@@ -38,12 +38,15 @@ variable {l l₁ l₂ l₃ : List α} {a b : α} {m n : ℕ}
 
 section Fix
 
+@[deprecated prefix_refl (since := "2024-08-12")]
 theorem prefix_rfl : l <+: l :=
   prefix_refl _
 
+@[deprecated suffix_refl (since := "2024-08-12")]
 theorem suffix_rfl : l <:+ l :=
   suffix_refl _
 
+@[deprecated infix_refl (since := "2024-08-12")]
 theorem infix_rfl : l <:+: l :=
   infix_refl _
 
@@ -54,26 +57,33 @@ theorem prefix_concat_iff {l₁ l₂ : List α} {a : α} :
   simpa only [← reverse_concat', reverse_inj, reverse_suffix] using
     suffix_cons_iff (l₁ := l₁.reverse) (l₂ := l₂.reverse)
 
-protected alias ⟨_, isSuffix.reverse⟩ := reverse_prefix
+protected alias ⟨_, IsSuffix.reverse⟩ := reverse_prefix
 
-protected alias ⟨_, isPrefix.reverse⟩ := reverse_suffix
+protected alias ⟨_, IsPrefix.reverse⟩ := reverse_suffix
 
-protected alias ⟨_, isInfix.reverse⟩ := reverse_infix
+protected alias ⟨_, IsInfix.reverse⟩ := reverse_infix
+
+@[deprecated IsSuffix.reverse (since := "2024-08-12")] alias isSuffix.reverse := IsSuffix.reverse
+@[deprecated IsPrefix.reverse (since := "2024-08-12")] alias isPrefix.reverse := IsPrefix.reverse
+@[deprecated IsInfix.reverse (since := "2024-08-12")] alias isInfix.reverse := IsInfix.reverse
 
 alias ⟨eq_nil_of_infix_nil, _⟩ := infix_nil
 
 alias ⟨eq_nil_of_prefix_nil, _⟩ := prefix_nil
 
 alias ⟨eq_nil_of_suffix_nil, _⟩ := suffix_nil
 
+@[deprecated IsInfix.eq_of_length (since := "2024-08-12")]
 theorem eq_of_infix_of_length_eq (h : l₁ <:+: l₂) : l₁.length = l₂.length → l₁ = l₂ :=
-  h.sublist.eq_of_length
+  h.eq_of_length
 
+@[deprecated IsPrefix.eq_of_length (since := "2024-08-12")]
 theorem eq_of_prefix_of_length_eq (h : l₁ <+: l₂) : l₁.length = l₂.length → l₁ = l₂ :=
-  h.sublist.eq_of_length
+  h.eq_of_length
 
+@[deprecated IsSuffix.eq_of_length (since := "2024-08-12")]
 theorem eq_of_suffix_of_length_eq (h : l₁ <:+ l₂) : l₁.length = l₂.length → l₁ = l₂ :=
-  h.sublist.eq_of_length
+  h.eq_of_length
 
 lemma dropSlice_sublist (n m : ℕ) (l : List α) : l.dropSlice n m <+ l :=
   calc
@@ -239,17 +249,17 @@ protected theorem IsPrefix.reduceOption {l₁ l₂ : List (Option α)} (h : l₁
 instance : IsPartialOrder (List α) (· <+: ·) where
   refl := prefix_refl
   trans _ _ _ := IsPrefix.trans
-  antisymm _ _ h₁ h₂ := eq_of_prefix_of_length_eq h₁ <| h₁.length_le.antisymm h₂.length_le
+  antisymm _ _ h₁ h₂ := h₁.eq_of_length <| h₁.length_le.antisymm h₂.length_le
 
 instance : IsPartialOrder (List α) (· <:+ ·) where
   refl := suffix_refl
   trans _ _ _ := IsSuffix.trans
-  antisymm _ _ h₁ h₂ := eq_of_suffix_of_length_eq h₁ <| h₁.length_le.antisymm h₂.length_le
+  antisymm _ _ h₁ h₂ := h₁.eq_of_length <| h₁.length_le.antisymm h₂.length_le
 
 instance : IsPartialOrder (List α) (· <:+: ·) where
   refl := infix_refl
   trans _ _ _ := IsInfix.trans
-  antisymm _ _ h₁ h₂ := eq_of_infix_of_length_eq h₁ <| h₁.length_le.antisymm h₂.length_le
+  antisymm _ _ h₁ h₂ := h₁.eq_of_length <| h₁.length_le.antisymm h₂.length_le
 
 end Fix
 
@@ -285,7 +295,7 @@ theorem mem_tails : ∀ s t : List α, s ∈ tails t ↔ s <:+ t
       show s = a :: t ∨ s <:+ t ↔ s <:+ a :: t from
         ⟨fun o =>
           match s, t, o with
-          | _, t, Or.inl rfl => suffix_rfl
+          | _, t, Or.inl rfl => suffix_refl _
           | s, _, Or.inr ⟨l, rfl⟩ => ⟨a :: l, rfl⟩,
           fun e =>
           match s, t, e with