chore(List): delete old, unused, deprecated theorems (#9607)

These theorems have been deprecated for at least a year, and are unused.



Co-authored-by: Michael Rothgang <rothgami@math.hu-berlin.de>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

Mathlib/Data/List/Basic.lean

@@ -862,10 +862,12 @@ theorem tail_append_of_ne_nil (l l' : List α) (h : l ≠ []) : (l ++ l').tail =
 
 theorem get_eq_iff {l : List α} {n : Fin l.length} {x : α} : l.get n = x ↔ l.get? n.1 = some x := by
   simp [get?_eq_some]
+#align list.nth_le_eq_iff List.get_eq_iff
 
 theorem get_eq_get? (l : List α) (i : Fin l.length) :
     l.get i = (l.get? i).get (by simp [get?_eq_get]) := by
   simp [get_eq_iff]
+#align list.some_nth_le_eq List.get?_eq_get
 
 section deprecated
 set_option linter.deprecated false -- TODO(Mario): make replacements for theorems in this section
@@ -1224,10 +1226,7 @@ theorem nthLe_get? {l : List α} {n} (h) : get? l n = some (nthLe l n h) := get?
 theorem get?_length (l : List α) : l.get? l.length = none := get?_len_le le_rfl
 #align list.nth_length List.get?_length
 
-@[deprecated get?_eq_some] -- 2023-01-05
-theorem get?_eq_some' {l : List α} {n a} : get? l n = some a ↔ ∃ h, nthLe l n h = a := get?_eq_some
-#align list.nth_eq_some List.get?_eq_some'
-
+#align list.nth_eq_some List.get?_eq_some
 #align list.nth_eq_none_iff List.get?_eq_none
 #align list.nth_of_mem List.get?_of_mem
 
@@ -1302,10 +1301,7 @@ theorem nthLe_zero [Inhabited α] {L : List α} (h : 0 < L.length) : List.nthLe
   simp [nthLe]
 #align list.nth_le_zero List.nthLe_zero
 
-@[deprecated get_append] -- 2023-01-05
-theorem nthLe_append {l₁ l₂ : List α} {n : ℕ} (hn₁) (hn₂) :
-    (l₁ ++ l₂).nthLe n hn₁ = l₁.nthLe n hn₂ := get_append _ hn₂
-#align list.nth_le_append List.nthLe_append
+#align list.nth_le_append List.get_append
 
 @[deprecated get_append_right'] -- 2023-01-05
 theorem nthLe_append_right {l₁ l₂ : List α} {n : ℕ} (h₁ : l₁.length ≤ n) (h₂) :
@@ -1314,30 +1310,16 @@ theorem nthLe_append_right {l₁ l₂ : List α} {n : ℕ} (h₁ : l₁.length 
 #align list.nth_le_append_right_aux List.get_append_right_aux
 #align list.nth_le_append_right List.nthLe_append_right
 
-@[deprecated get_replicate] -- 2023-01-05
-theorem nthLe_replicate (a : α) {n m : ℕ} (h : m < (replicate n a).length) :
-    (replicate n a).nthLe m h = a := get_replicate ..
-#align list.nth_le_replicate List.nthLe_replicate
-
+#align list.nth_le_replicate List.get_replicate
 #align list.nth_append List.get?_append
 #align list.nth_append_right List.get?_append_right
-
-@[deprecated getLast_eq_get] -- 2023-01-05
-theorem getLast_eq_nthLe (l : List α) (h : l ≠ []) :
-    getLast l h = l.nthLe (l.length - 1) (have := length_pos_of_ne_nil h; by omega) :=
-  getLast_eq_get ..
-#align list.last_eq_nth_le List.getLast_eq_nthLe
+#align list.last_eq_nth_le List.getLast_eq_get
 
 theorem get_length_sub_one {l : List α} (h : l.length - 1 < l.length) :
     l.get ⟨l.length - 1, h⟩ = l.getLast (by rintro rfl; exact Nat.lt_irrefl 0 h) :=
   (getLast_eq_get l _).symm
 
-@[deprecated get_length_sub_one] -- 2023-01-05
-theorem nthLe_length_sub_one {l : List α} (h : l.length - 1 < l.length) :
-    l.nthLe (l.length - 1) h = l.getLast (by rintro rfl; exact Nat.lt_irrefl 0 h) :=
-  get_length_sub_one _
-#align list.nth_le_length_sub_one List.nthLe_length_sub_one
-
+#align list.nth_le_length_sub_one List.get_length_sub_one
 #align list.nth_concat_length List.get?_concat_length
 
 @[deprecated get_cons_length] -- 2023-01-05
@@ -1466,16 +1448,6 @@ theorem eq_cons_of_length_one {l : List α} (h : l.length = 1) :
   omega
 #align list.eq_cons_of_length_one List.eq_cons_of_length_one
 
-@[deprecated get_eq_iff] -- 2023-01-05
-theorem nthLe_eq_iff {l : List α} {n : ℕ} {x : α} {h} : l.nthLe n h = x ↔ l.get? n = some x :=
-  get_eq_iff
-#align list.nth_le_eq_iff List.nthLe_eq_iff
-
-@[deprecated get?_eq_get] -- 2023-01-05
-theorem some_nthLe_eq {l : List α} {n : ℕ} {h} : some (l.nthLe n h) = l.get? n :=
-  (get?_eq_get _).symm
-#align list.some_nth_le_eq List.some_nthLe_eq
-
 end deprecated
 
 theorem modifyNthTail_modifyNthTail {f g : List α → List α} (m : ℕ) :
@@ -1545,27 +1517,16 @@ theorem length_modifyNth (f : α → α) : ∀ n l, length (modifyNth f n l) = l
 #align list.update_nth_succ List.set_succ
 #align list.update_nth_comm List.set_comm
 
-@[simp, deprecated get_set_eq] -- 2023-01-05
-theorem nthLe_set_eq (l : List α) (i : ℕ) (a : α) (h : i < (l.set i a).length) :
-    (l.set i a).nthLe i h = a := get_set_eq ..
-#align list.nth_le_update_nth_eq List.nthLe_set_eq
-
+#align list.nth_le_update_nth_eq List.get_set_eq
 @[simp]
 theorem get_set_of_ne {l : List α} {i j : ℕ} (h : i ≠ j) (a : α)
     (hj : j < (l.set i a).length) :
     (l.set i a).get ⟨j, hj⟩ = l.get ⟨j, by simpa using hj⟩ := by
   rw [← Option.some_inj, ← List.get?_eq_get, List.get?_set_ne _ _ h, List.get?_eq_get]
 
-@[simp, deprecated get_set_of_ne] -- 2023-01-05
-theorem nthLe_set_of_ne {l : List α} {i j : ℕ} (h : i ≠ j) (a : α)
-    (hj : j < (l.set i a).length) :
-    (l.set i a).nthLe j hj = l.nthLe j (by simpa using hj) :=
-  get_set_of_ne h _ hj
-#align list.nth_le_update_nth_of_ne List.nthLe_set_of_ne
-
+#align list.nth_le_update_nth_of_ne List.get_set_of_ne
 #align list.mem_or_eq_of_mem_update_nth List.mem_or_eq_of_mem_set
 
-
 /-! ### map -/
 
 #align list.map_nil List.map_nil
@@ -1781,25 +1742,8 @@ theorem take_cons (n) (a : α) (l : List α) : take (succ n) (a :: l) = a :: tak
 #align list.take_append_eq_append_take List.take_append_eq_append_take
 #align list.take_append_of_le_length List.take_append_of_le_length
 #align list.take_append List.take_append
-
-set_option linter.deprecated false in
-/-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of
-length `> i`. Version designed to rewrite from the big list to the small list. -/
-@[deprecated get_take] -- 2023-01-05
-theorem nthLe_take (L : List α) {i j : ℕ} (hi : i < L.length) (hj : i < j) :
-    nthLe L i hi = nthLe (L.take j) i (length_take .. ▸ lt_min hj hi) :=
-  get_take _ hi hj
-#align list.nth_le_take List.nthLe_take
-
-set_option linter.deprecated false in
-/-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of
-length `> i`. Version designed to rewrite from the small list to the big list. -/
-@[deprecated get_take'] -- 2023-01-05
-theorem nthLe_take' (L : List α) {i j : ℕ} (hi : i < (L.take j).length) :
-    nthLe (L.take j) i hi = nthLe L i (lt_of_lt_of_le hi (by simp only [length_take]; omega)) :=
-  get_take' _
-#align list.nth_le_take' List.nthLe_take'
-
+#align list.nth_le_take List.get_take
+#align list.nth_le_take' List.get_take'
 #align list.nth_take List.get?_take
 #align list.nth_take_of_succ List.nth_take_of_succ
 #align list.take_succ List.take_succ
@@ -1822,11 +1766,7 @@ theorem cons_get_drop_succ {l : List α} {n} :
     l.get n :: l.drop (n.1 + 1) = l.drop n.1 :=
   (drop_eq_get_cons n.2).symm
 
-@[deprecated cons_get_drop_succ] -- 2023-01-05
-theorem cons_nthLe_drop_succ {l : List α} {n : ℕ} (hn : n < l.length) :
-    l.nthLe n hn :: l.drop (n + 1) = l.drop n := cons_get_drop_succ
-#align list.cons_nth_le_drop_succ List.cons_nthLe_drop_succ
-
+#align list.cons_nth_le_drop_succ List.cons_get_drop_succ
 #align list.drop_nil List.drop_nil
 #align list.drop_one List.drop_one
 #align list.drop_add List.drop_add
@@ -1839,24 +1779,8 @@ theorem cons_nthLe_drop_succ {l : List α} {n : ℕ} (hn : n < l.length) :
 #align list.drop_append_of_le_length List.drop_append_of_le_length
 #align list.drop_append List.drop_append
 #align list.drop_sizeof_le List.drop_sizeOf_le
-
-set_option linter.deprecated false in
-/-- The `i + j`-th element of a list coincides with the `j`-th element of the list obtained by
-dropping the first `i` elements. Version designed to rewrite from the big list to the small list. -/
-@[deprecated get_drop] -- 2023-01-05
-theorem nthLe_drop (L : List α) {i j : ℕ} (h : i + j < L.length) :
-    nthLe L (i + j) h = nthLe (L.drop i) j (by rw [length_drop]; omega) := get_drop ..
-#align list.nth_le_drop List.nthLe_drop
-
-set_option linter.deprecated false in
-/-- The `i + j`-th element of a list coincides with the `j`-th element of the list obtained by
-dropping the first `i` elements. Version designed to rewrite from the small list to the big list. -/
-@[deprecated get_drop'] -- 2023-01-05
-theorem nthLe_drop' (L : List α) {i j : ℕ} (h : j < (L.drop i).length) :
-    nthLe (L.drop i) j h = nthLe L (i + j) (have := length_drop i L; by omega) :=
-  get_drop' ..
-#align list.nth_le_drop' List.nthLe_drop'
-
+#align list.nth_le_drop List.get_drop
+#align list.nth_le_drop' List.get_drop'
 #align list.nth_drop List.get?_drop
 #align list.drop_drop List.drop_drop
 #align list.drop_take List.drop_take
@@ -3640,7 +3564,6 @@ theorem get_attach (L : List α) (i) :
     (L.attach.get i).1 = (L.attach.map Subtype.val).get ⟨i, by simpa using i.2⟩ :=
       by rw [get_map]
     _ = L.get { val := i, isLt := _ } := by congr 2 <;> simp
-
 #align list.nth_le_attach List.get_attach
 
 @[simp 1100]