List.takeWhile and List.dropWhile

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

theorem List.length_dropWhile_le {α : Type u_1} (p : α → Bool) (l : List α) : (dropWhile p l).length ≤ l.length

@[simp]

theorem List.dropWhile_eq_nil_iff {α : Type u_1} {p : α → Bool} {l : List α} : dropWhile p l = [] ↔ ∀ (x : α), x ∈ l → p x = true

@[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

@[simp]

theorem List.takeWhile_eq_self_iff {α : Type u_1} {p : α → Bool} {l : List α} : takeWhile p l = l ↔ ∀ (x : α), x ∈ l → p x = true

@[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

theorem List.mem_takeWhile_imp {α : Type u_1} {p : α → Bool} {l : List α} {x : α} (hx : x ∈ takeWhile p l) : p x = true

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

theorem List.takeWhile_idem {α : Type u_1} {p : α → Bool} {l : List α} : takeWhile p (takeWhile p l) = takeWhile p l

theorem List.find?_eq_head?_dropWhile_not {α : Type u_1} (p : α → Bool) (l : List α) : find? p l = (dropWhile (fun (x : α) => !p x) l).head?

theorem List.find?_not_eq_head?_dropWhile {α : Type u_1} (p : α → Bool) (l : List α) : find? (fun (x : α) => !p x) l = (dropWhile p l).head?

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 ⋯)

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 ⋯)