feat: add List.enum_eq_nil and List.mapIdx_eq_nil (#8493)

Adds `List.enum_eq_nil` and `List.mapIdx_eq_nil`.
These are analogous to [`List.map_eq_nil`](https://github.com/leanprover/std4/blob/c14f6a65b2c08caa38e1ab5db83451460d6cde3e//Std/Data/List/Lemmas.lean#L166-L167).

Mathlib/Data/List/Basic.lean

@@ -3865,6 +3865,13 @@ theorem nthLe_enum (l : List α) (i : ℕ) (hi' : i < l.enum.length)
     l.enum.nthLe i hi' = (i, l.nthLe i hi) := get_enum ..
 #align list.nth_le_enum List.nthLe_enum
 
+@[simp]
+theorem enumFrom_eq_nil {n : ℕ} {l : List α} : List.enumFrom n l = [] ↔ l = [] := by
+  cases l <;> simp
+
+@[simp]
+theorem enum_eq_nil {l : List α} : List.enum l = [] ↔ l = [] := enumFrom_eq_nil
+
 section Choose
 
 variable (p : α → Prop) [DecidablePred p] (l : List α)

Mathlib/Data/List/Indexes.lean

@@ -192,6 +192,10 @@ theorem length_mapIdx {α β} (l : List α) (f : ℕ → α → β) : (l.mapIdx
   · simp [IH]
 #align list.length_map_with_index List.length_mapIdx
 
+@[simp]
+theorem mapIdx_eq_nil {α β} {f : ℕ → α → β} {l : List α} : List.mapIdx f l = [] ↔ l = [] := by
+  rw [List.mapIdx_eq_enum_map, List.map_eq_nil, List.enum_eq_nil]
+
 @[simp, deprecated]
 theorem nthLe_mapIdx {α β} (l : List α) (f : ℕ → α → β) (i : ℕ) (h : i < l.length)
     (h' : i < (l.mapIdx f).length := h.trans_le (l.length_mapIdx f).ge) :