α : Type u_1
p : α → Bool
l : List α
n : ℕ
x : α
⊢ reverse
      (match p x with
      | true => x :: takeWhile p (reverse l)
      | false => []) =
    if p x = true then reverse (takeWhile p (reverse l)) ++ [x] else []
α : Type u_1
p : α → Bool
l : List α
n : ℕ
x : α
⊢ rtakeWhile p (l ++ [x]) = if p x = true then rtakeWhile p l ++ [x] else []
simp only [rtakeWhile, takeWhile, reverse_append, reverse_singleton, singleton_append]
no goals
α : Type u_1
p : α → Bool
l : List α
n : ℕ
x : α
⊢ reverse
      (match p x with
      | true => x :: takeWhile p (reverse l)
      | false => []) =
    if p x = true then reverse (takeWhile p (reverse l)) ++ [x] else []
split_ifs with h <;> simp [h]