feat: additional lemmas for lists (#4602)

Split from #4583

`exists_of_set` appears in Batteries as `exists_of_set'`. The
`exists_of_set` version is unused in batteries and mathlib at least and
I would argue that the primed version (i.e., the one added in this PR)
is always better anyway.

`isEmpty_iff` appears in mathlib as `isEmpty_iff_eq_nil`.

src/Init/Data/List/Lemmas.lean

@@ -126,6 +126,14 @@ theorem length_pos {l : List α} : 0 < length l ↔ l ≠ [] :=
 theorem length_eq_one {l : List α} : length l = 1 ↔ ∃ a, l = [a] :=
   ⟨fun h => match l, h with | [_], _ => ⟨_, rfl⟩, fun ⟨_, h⟩ => by simp [h]⟩
 
+/-! ### `isEmpty` -/
+
+theorem isEmpty_iff {l : List α} : l.isEmpty ↔ l = [] := by
+  cases l <;> simp
+
+theorem isEmpty_iff_length_eq_zero {l : List α} : l.isEmpty ↔ l.length = 0 := by
+  rw [isEmpty_iff, length_eq_zero]
+
 /-! ### L[i] and L[i]? -/
 
 @[simp] theorem get_cons_zero : get (a::l) (0 : Fin (l.length + 1)) = a := rfl
@@ -1035,6 +1043,10 @@ theorem getElem_append_right' {l₁ l₂ : List α} {n : Nat} (h₁ : l₁.lengt
       l₂[n - l₁.length]'(by rw [length_append] at h₂; exact Nat.sub_lt_left_of_lt_add h₁ h₂) :=
   Option.some.inj <| by rw [← getElem?_eq_getElem, ← getElem?_eq_getElem, getElem?_append_right h₁]
 
+theorem getElem_append_right'' (l₁ : List α) {l₂ : List α} {n : Nat} (hn : n < l₂.length) :
+    l₂[n] = (l₁ ++ l₂)[n + l₁.length]'(by simpa [Nat.add_comm] using Nat.add_lt_add_left hn _) := by
+  rw [getElem_append_right] <;> simp [*, le_add_left]
+
 @[deprecated (since := "2024-06-12")]
 theorem get_append_right_aux {l₁ l₂ : List α} {n : Nat}
   (h₁ : l₁.length ≤ n) (h₂ : n < (l₁ ++ l₂).length) : n - l₁.length < l₂.length := by
@@ -1282,6 +1294,14 @@ theorem map_eq_bind {α β} (f : α → β) (l : List α) : map f l = l.bind fun
   simp only [← map_singleton]
   rw [← bind_singleton' l, map_bind, bind_singleton']
 
+theorem bind_eq_foldl (f : α → List β) (l : List α) :
+    l.bind f = l.foldl (fun acc a => acc ++ f a) [] := by
+  suffices ∀ l', l' ++ l.bind f = l.foldl (fun acc a => acc ++ f a) l' by simpa using this []
+  intro l'
+  induction l generalizing l'
+  · simp
+  · next ih => rw [bind_cons, ← append_assoc, ih, foldl_cons]
+
 /-! ### replicate -/
 
 @[simp] theorem replicate_one : replicate 1 a = [a] := rfl
@@ -1529,6 +1549,10 @@ theorem reverseAux_eq (as bs : List α) : reverseAux as bs = reverse as ++ bs :=
 theorem contains_eq_any_beq [BEq α] (l : List α) (a : α) : l.contains a = l.any (a == ·) := by
   induction l with simp | cons b l => cases b == a <;> simp [*]
 
+theorem contains_iff_exists_mem_beq [BEq α] (l : List α) (a : α) :
+    l.contains a ↔ ∃ a' ∈ l, a == a' := by
+  induction l <;> simp_all
+
 /-! ## Sublists -/
 
 /-! ### take and drop

src/Init/Data/List/TakeDrop.lean

@@ -272,6 +272,15 @@ theorem set_eq_take_append_cons_drop {l : List α} {n : Nat} {a : α} :
   · rw [set_eq_of_length_le]
     omega
 
+theorem exists_of_set {n : Nat} {a' : α} {l : List α} (h : n < l.length) :
+    ∃ l₁ l₂, l = l₁ ++ l[n] :: l₂ ∧ l₁.length = n ∧ l.set n a' = l₁ ++ a' :: l₂ := by
+  refine ⟨l.take n, l.drop (n + 1), ⟨by simp, ⟨length_take_of_le (Nat.le_of_lt h), ?_⟩⟩⟩
+  simp [set_eq_take_append_cons_drop, h]
+
+theorem drop_set_of_lt (a : α) {n m : Nat} (l : List α)
+    (hnm : n < m) : drop m (l.set n a) = l.drop m :=
+  ext_getElem? fun k => by simpa only [getElem?_drop] using getElem?_set_ne (by omega)
+
 theorem drop_take : ∀ (m n : Nat) (l : List α), drop n (take m l) = take (m - n) (drop n l)
   | 0, _, _ => by simp
   | _, 0, _ => by simp