### List.takeWhile and List.dropWhile #

source
theorem List.dropWhile_get_zero_not {α : Type u_1} (p : α → Bool) (l : List α) (hl : 0 < (dropWhile p l).length) :
¬p ((dropWhile p l).get ⟨0, hl⟩) = true
source
theorem List.length_dropWhile_le {α : Type u_1} (p : α → Bool) (l : List α) :
(dropWhile p l).length ≤ l.length
source
@[simp]
theorem List.dropWhile_eq_nil_iff {α : Type u_1} {p : α → Bool} {l : List α} :
dropWhile p l = [] ↔ ∀ (x : α), x ∈ l → p x = true
source
@[simp]
theorem List.dropWhile_eq_self_iff {α : Type u_1} {p : α → Bool} {l : List α} :
dropWhile p l = l ↔ ∀ (hl : 0 < l.length), ¬p l[0] = true
source
@[simp]
theorem List.takeWhile_eq_self_iff {α : Type u_1} {p : α → Bool} {l : List α} :
takeWhile p l = l ↔ ∀ (x : α), x ∈ l → p x = true
source
@[simp]
theorem List.takeWhile_eq_nil_iff {α : Type u_1} {p : α → Bool} {l : List α} :
takeWhile p l = [] ↔ ∀ (hl : 0 < l.length), ¬p (l.get ⟨0, hl⟩) = true
source
theorem List.mem_takeWhile_imp {α : Type u_1} {p : α → Bool} {l : List α} {x : α} (hx : x ∈ takeWhile p l) :
p x = true
source
theorem List.takeWhile_takeWhile {α : Type u_1} (p q : α → Bool) (l : List α) :
takeWhile p (takeWhile q l) = takeWhile (fun (a : α) => decide (p a = true ∧ q a = true)) l
source
theorem List.takeWhile_idem {α : Type u_1} {p : α → Bool} {l : List α} :
takeWhile p (takeWhile p l) = takeWhile p l
source
theorem List.find?_eq_head?_dropWhile_not {α : Type u_1} (p : α → Bool) (l : List α) :
find? p l = (dropWhile (fun (x : α) => !p x) l).head?
source
theorem List.find?_not_eq_head?_dropWhile {α : Type u_1} (p : α → Bool) (l : List α) :
find? (fun (x : α) => !p x) l = (dropWhile p l).head?
source
theorem List.find?_eq_head_dropWhile_not {α : Type u_1} {p : α → Bool} {l : List α} (h : ∃ (x : α), x ∈ l ∧ p x = true) :
find? p l = some ((dropWhile (fun (x : α) => !p x) l).head ⋯)
source
theorem List.find?_not_eq_head_dropWhile {α : Type u_1} {p : α → Bool} {l : List α} (h : ∃ (x : α), x ∈ l ∧ ¬p x = true) :
find? (fun (x : α) => !p x) l = some ((dropWhile p l).head ⋯)