feat(List/Enum): add lemmas about ∀ x ∈ l.enum, p x etc (#16789)

Mathlib/Data/List/Enum.lean

@@ -3,18 +3,17 @@ Copyright (c) 2017 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Yakov Pechersky, Eric Wieser
 -/
-import Batteries.Tactic.Alias
-import Mathlib.Tactic.TypeStar
-import Mathlib.Data.Nat.Notation
+import Mathlib.Data.List.Basic
 
 /-!
 # Properties of `List.enum`
 
 ## Deprecation note
-Everything in this file has been replaced by theorems in Lean4,
+
+Many lemmas in this file have been replaced by theorems in Lean4,
 in terms of `xs[i]?` and `xs[i]` rather than `get` and `get?`.
 
-The results here are unused in Mathlib, and deprecated.
+The deprecated results here are unused in Mathlib.
 Any downstream users who can not easily adapt may remove the deprecations as needed.
 -/
 
@@ -64,4 +63,20 @@ set_option linter.deprecated false in
 theorem mem_enum_iff_get? {x : ℕ × α} {l : List α} : x ∈ enum l ↔ l.get? x.1 = x.2 :=
   mk_mem_enum_iff_get?
 
+theorem forall_mem_enumFrom {l : List α} {n : ℕ} {p : ℕ × α → Prop} :
+    (∀ x ∈ l.enumFrom n, p x) ↔ ∀ (i : ℕ) (_ : i < length l), p (n + i, l[i]) := by
+  simp only [forall_mem_iff_getElem, getElem_enumFrom, enumFrom_length]
+
+theorem forall_mem_enum {l : List α} {p : ℕ × α → Prop} :
+    (∀ x ∈ l.enum, p x) ↔ ∀ (i : ℕ) (_ : i < length l), p (i, l[i]) :=
+  forall_mem_enumFrom.trans <| by simp
+
+theorem exists_mem_enumFrom {l : List α} {n : ℕ} {p : ℕ × α → Prop} :
+    (∃ x ∈ l.enumFrom n, p x) ↔ ∃ (i : ℕ) (_ : i < length l), p (n + i, l[i]) := by
+  simp only [exists_mem_iff_getElem, getElem_enumFrom, enumFrom_length]
+
+theorem exists_mem_enum {l : List α} {p : ℕ × α → Prop} :
+    (∃ x ∈ l.enum, p x) ↔ ∃ (i : ℕ) (_ : i < length l), p (i, l[i]) :=
+  exists_mem_enumFrom.trans <| by simp
+
 end List