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