α : Type u_1
p : α → Bool
x : α
xs : List α
⊢ ((match p x with
      | true => x :: takeWhile p xs
      | false => []) ++
      match p x with
      | true => dropWhile p xs
      | false => x :: xs) =
    x :: xs
α : Type u_1
p : α → Bool
x : α
xs : List α
⊢ takeWhile p (x :: xs) ++ dropWhile p (x :: xs) = x :: xs
simp [takeWhile, dropWhile]
no goals
α : Type u_1
p : α → Bool
x : α
xs : List α
⊢ ((match p x with
      | true => x :: takeWhile p xs
      | false => []) ++
      match p x with
      | true => dropWhile p xs
      | false => x :: xs) =
    x :: xs
cases p x <;> simp [takeWhile_append_dropWhile p xs]