[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ rdrop [] n = []
[PROOFSTEP]
simp [rdrop]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ rdrop l 0 = l
[PROOFSTEP]
simp [rdrop]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ rdrop l n = reverse (drop n (reverse l))
[PROOFSTEP]
rw [rdrop]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ take (length l - n) l = reverse (drop n (reverse l))
[PROOFSTEP]
induction' l using List.reverseRecOn with xs x IH generalizing n
[GOAL]
case H0
α : Type u_1
p : α → Bool
l : List α
n✝ n : ℕ
⊢ take (length [] - n) [] = reverse (drop n (reverse []))
[PROOFSTEP]
simp
[GOAL]
case H1
α : Type u_1
p : α → Bool
l : List α
n✝ : ℕ
xs : List α
x : α
IH : ∀ (n : ℕ), take (length xs - n) xs = reverse (drop n (reverse xs))
n : ℕ
⊢ take (length (xs ++ [x]) - n) (xs ++ [x]) = reverse (drop n (reverse (xs ++ [x])))
[PROOFSTEP]
cases n
[GOAL]
case H1.zero
α : Type u_1
p : α → Bool
l : List α
n : ℕ
xs : List α
x : α
IH : ∀ (n : ℕ), take (length xs - n) xs = reverse (drop n (reverse xs))
⊢ take (length (xs ++ [x]) - Nat.zero) (xs ++ [x]) = reverse (drop Nat.zero (reverse (xs ++ [x])))
[PROOFSTEP]
simp [take_append]
[GOAL]
case H1.succ
α : Type u_1
p : α → Bool
l : List α
n : ℕ
xs : List α
x : α
IH : ∀ (n : ℕ), take (length xs - n) xs = reverse (drop n (reverse xs))
n✝ : ℕ
⊢ take (length (xs ++ [x]) - Nat.succ n✝) (xs ++ [x]) = reverse (drop (Nat.succ n✝) (reverse (xs ++ [x])))
[PROOFSTEP]
simp [take_append_eq_append_take, IH]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
x : α
⊢ rdrop (l ++ [x]) (n + 1) = rdrop l n
[PROOFSTEP]
simp [rdrop_eq_reverse_drop_reverse]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ rtake [] n = []
[PROOFSTEP]
simp [rtake]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ rtake l 0 = []
[PROOFSTEP]
simp [rtake]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ rtake l n = reverse (take n (reverse l))
[PROOFSTEP]
rw [rtake]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ drop (length l - n) l = reverse (take n (reverse l))
[PROOFSTEP]
induction' l using List.reverseRecOn with xs x IH generalizing n
[GOAL]
case H0
α : Type u_1
p : α → Bool
l : List α
n✝ n : ℕ
⊢ drop (length [] - n) [] = reverse (take n (reverse []))
[PROOFSTEP]
simp
[GOAL]
case H1
α : Type u_1
p : α → Bool
l : List α
n✝ : ℕ
xs : List α
x : α
IH : ∀ (n : ℕ), drop (length xs - n) xs = reverse (take n (reverse xs))
n : ℕ
⊢ drop (length (xs ++ [x]) - n) (xs ++ [x]) = reverse (take n (reverse (xs ++ [x])))
[PROOFSTEP]
cases n
[GOAL]
case H1.zero
α : Type u_1
p : α → Bool
l : List α
n : ℕ
xs : List α
x : α
IH : ∀ (n : ℕ), drop (length xs - n) xs = reverse (take n (reverse xs))
⊢ drop (length (xs ++ [x]) - Nat.zero) (xs ++ [x]) = reverse (take Nat.zero (reverse (xs ++ [x])))
[PROOFSTEP]
exact drop_length _
[GOAL]
case H1.succ
α : Type u_1
p : α → Bool
l : List α
n : ℕ
xs : List α
x : α
IH : ∀ (n : ℕ), drop (length xs - n) xs = reverse (take n (reverse xs))
n✝ : ℕ
⊢ drop (length (xs ++ [x]) - Nat.succ n✝) (xs ++ [x]) = reverse (take (Nat.succ n✝) (reverse (xs ++ [x])))
[PROOFSTEP]
simp [drop_append_eq_append_drop, IH]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
x : α
⊢ rtake (l ++ [x]) (n + 1) = rtake l n ++ [x]
[PROOFSTEP]
simp [rtake_eq_reverse_take_reverse]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ rdropWhile p [] = []
[PROOFSTEP]
simp [rdropWhile, dropWhile]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
x : α
⊢ rdropWhile p (l ++ [x]) = if p x = true then rdropWhile p l else l ++ [x]
[PROOFSTEP]
simp only [rdropWhile, dropWhile, reverse_append, reverse_singleton, singleton_append]
[GOAL]
α : 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]
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
p : α → Bool
l : List α
n : ℕ
x : α
h : p x = true
⊢ reverse
      (match p x with
      | true => dropWhile p (reverse l)
      | false => x :: reverse l) =
    reverse (dropWhile p (reverse l))
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
p : α → Bool
l : List α
n : ℕ
x : α
h : ¬p x = true
⊢ reverse
      (match p x with
      | true => dropWhile p (reverse l)
      | false => x :: reverse l) =
    l ++ [x]
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
x : α
h : p x = true
⊢ rdropWhile p (l ++ [x]) = rdropWhile p l
[PROOFSTEP]
rw [rdropWhile_concat, if_pos h]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
x : α
h : ¬p x = true
⊢ rdropWhile p (l ++ [x]) = l ++ [x]
[PROOFSTEP]
rw [rdropWhile_concat, if_neg h]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
x : α
⊢ rdropWhile p [x] = if p x = true then [] else [x]
[PROOFSTEP]
rw [← nil_append [x], rdropWhile_concat, rdropWhile_nil]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
hl : rdropWhile p l ≠ []
⊢ ¬p (getLast (rdropWhile p l) hl) = true
[PROOFSTEP]
simp_rw [rdropWhile]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
hl : rdropWhile p l ≠ []
⊢ ¬p (getLast (reverse (dropWhile p (reverse l))) (_ : reverse (dropWhile p (reverse l)) ≠ [])) = true
[PROOFSTEP]
rw [getLast_reverse]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
hl : rdropWhile p l ≠ []
⊢ ¬p (get (dropWhile p (reverse l)) { val := 0, isLt := (_ : 0 < length (dropWhile p (reverse l))) }) = true
[PROOFSTEP]
exact dropWhile_nthLe_zero_not _ _ _
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ rdropWhile p l <+: l
[PROOFSTEP]
rw [← reverse_suffix, rdropWhile, reverse_reverse]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ dropWhile p (reverse l) <:+ reverse l
[PROOFSTEP]
exact dropWhile_suffix _
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ rdropWhile p l = [] ↔ ∀ (x : α), x ∈ l → p x = true
[PROOFSTEP]
simp [rdropWhile]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ dropWhile p l = l ↔ ∀ (hl : 0 < length l), ¬p (nthLe l 0 hl) = true
[PROOFSTEP]
cases' l with hd tl
[GOAL]
case nil
α : Type u_1
p : α → Bool
n : ℕ
⊢ dropWhile p [] = [] ↔ ∀ (hl : 0 < length []), ¬p (nthLe [] 0 hl) = true
[PROOFSTEP]
simp only [dropWhile, true_iff]
[GOAL]
case nil
α : Type u_1
p : α → Bool
n : ℕ
⊢ ∀ (hl : 0 < length []), ¬p (nthLe [] 0 hl) = true
[PROOFSTEP]
intro h
[GOAL]
case nil
α : Type u_1
p : α → Bool
n : ℕ
h : 0 < length []
⊢ ¬p (nthLe [] 0 h) = true
[PROOFSTEP]
by_contra
[GOAL]
case nil
α : Type u_1
p : α → Bool
n : ℕ
h : 0 < length []
a✝ : p (nthLe [] 0 h) = true
⊢ False
[PROOFSTEP]
rwa [length_nil, lt_self_iff_false] at h 
[GOAL]
case cons
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
⊢ dropWhile p (hd :: tl) = hd :: tl ↔ ∀ (hl : 0 < length (hd :: tl)), ¬p (nthLe (hd :: tl) 0 hl) = true
[PROOFSTEP]
rw [dropWhile]
[GOAL]
case cons
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
⊢ (match p hd with
      | true => dropWhile p tl
      | false => hd :: tl) =
      hd :: tl ↔
    ∀ (hl : 0 < length (hd :: tl)), ¬p (nthLe (hd :: tl) 0 hl) = true
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case cons.refine'_1
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
h :
  (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
⊢ ∀ (hl : 0 < length (hd :: tl)), ¬p (nthLe (hd :: tl) 0 hl) = true
[PROOFSTEP]
intro _ H
[GOAL]
case cons.refine'_1
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
h :
  (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
hl✝ : 0 < length (hd :: tl)
H : p (nthLe (hd :: tl) 0 hl✝) = true
⊢ False
[PROOFSTEP]
rw [nthLe, get] at H 
[GOAL]
case cons.refine'_1
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
h :
  (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
hl✝ : 0 < length (hd :: tl)
H : p hd = true
⊢ False
[PROOFSTEP]
refine' (cons_ne_self hd tl) (Sublist.antisymm _ (sublist_cons _ _))
[GOAL]
case cons.refine'_1
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
h :
  (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
hl✝ : 0 < length (hd :: tl)
H : p hd = true
⊢ hd :: tl <+ tl
[PROOFSTEP]
rw [← h]
[GOAL]
case cons.refine'_1
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
h :
  (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
hl✝ : 0 < length (hd :: tl)
H : p hd = true
⊢ (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) <+
    tl
[PROOFSTEP]
simp only [H]
[GOAL]
case cons.refine'_1
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
h :
  (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
hl✝ : 0 < length (hd :: tl)
H : p hd = true
⊢ dropWhile p tl <+ tl
[PROOFSTEP]
exact List.isSuffix.sublist (dropWhile_suffix p)
[GOAL]
case cons.refine'_2
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
h : ∀ (hl : 0 < length (hd :: tl)), ¬p (nthLe (hd :: tl) 0 hl) = true
⊢ (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
[PROOFSTEP]
have := h (by simp only [length, Nat.succ_pos])
[GOAL]
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
h : ∀ (hl : 0 < length (hd :: tl)), ¬p (nthLe (hd :: tl) 0 hl) = true
⊢ 0 < length (hd :: tl)
[PROOFSTEP]
simp only [length, Nat.succ_pos]
[GOAL]
case cons.refine'_2
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
h : ∀ (hl : 0 < length (hd :: tl)), ¬p (nthLe (hd :: tl) 0 hl) = true
this : ¬p (nthLe (hd :: tl) 0 (_ : 0 < Nat.succ (length tl))) = true
⊢ (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
[PROOFSTEP]
rw [nthLe, get] at this 
[GOAL]
case cons.refine'_2
α : Type u_1
p : α → Bool
n : ℕ
hd : α
tl : List α
h : ∀ (hl : 0 < length (hd :: tl)), ¬p (nthLe (hd :: tl) 0 hl) = true
this : ¬p hd = true
⊢ (match p hd with
    | true => dropWhile p tl
    | false => hd :: tl) =
    hd :: tl
[PROOFSTEP]
simp_rw [this]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ rdropWhile p l = l ↔ ∀ (hl : l ≠ []), ¬p (getLast l hl) = true
[PROOFSTEP]
simp only [rdropWhile, reverse_eq_iff, dropWhile_eq_self_iff, getLast_eq_get]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ (∀ (hl : 0 < length (reverse l)), ¬p (nthLe (reverse l) 0 hl) = true) ↔
    ∀ (hl : l ≠ []), ¬p (get l { val := length l - 1, isLt := (_ : length l - 1 < length l) }) = true
[PROOFSTEP]
refine' ⟨fun h hl => _, fun h hl => _⟩
[GOAL]
case refine'_1
α : Type u_1
p : α → Bool
l : List α
n : ℕ
h : ∀ (hl : 0 < length (reverse l)), ¬p (nthLe (reverse l) 0 hl) = true
hl : l ≠ []
⊢ ¬p (get l { val := length l - 1, isLt := (_ : length l - 1 < length l) }) = true
[PROOFSTEP]
rw [← length_pos, ← length_reverse] at hl 
[GOAL]
case refine'_1
α : Type u_1
p : α → Bool
l : List α
n : ℕ
h : ∀ (hl : 0 < length (reverse l)), ¬p (nthLe (reverse l) 0 hl) = true
hl✝ : l ≠ []
hl : 0 < length (reverse l)
⊢ ¬p (get l { val := length l - 1, isLt := (_ : length l - 1 < length l) }) = true
[PROOFSTEP]
have := h hl
[GOAL]
case refine'_1
α : Type u_1
p : α → Bool
l : List α
n : ℕ
h : ∀ (hl : 0 < length (reverse l)), ¬p (nthLe (reverse l) 0 hl) = true
hl✝ : l ≠ []
hl : 0 < length (reverse l)
this : ¬p (nthLe (reverse l) 0 hl) = true
⊢ ¬p (get l { val := length l - 1, isLt := (_ : length l - 1 < length l) }) = true
[PROOFSTEP]
rwa [nthLe, get_reverse'] at this 
[GOAL]
case refine'_2
α : Type u_1
p : α → Bool
l : List α
n : ℕ
h : ∀ (hl : l ≠ []), ¬p (get l { val := length l - 1, isLt := (_ : length l - 1 < length l) }) = true
hl : 0 < length (reverse l)
⊢ ¬p (nthLe (reverse l) 0 hl) = true
[PROOFSTEP]
rw [length_reverse, length_pos] at hl 
[GOAL]
case refine'_2
α : Type u_1
p : α → Bool
l : List α
n : ℕ
h : ∀ (hl : l ≠ []), ¬p (get l { val := length l - 1, isLt := (_ : length l - 1 < length l) }) = true
hl✝ : 0 < length (reverse l)
hl : l ≠ []
⊢ ¬p (nthLe (reverse l) 0 hl✝) = true
[PROOFSTEP]
have := h hl
[GOAL]
case refine'_2
α : Type u_1
p : α → Bool
l : List α
n : ℕ
h : ∀ (hl : l ≠ []), ¬p (get l { val := length l - 1, isLt := (_ : length l - 1 < length l) }) = true
hl✝ : 0 < length (reverse l)
hl : l ≠ []
this : ¬p (get l { val := length l - 1, isLt := (_ : length l - 1 < length l) }) = true
⊢ ¬p (nthLe (reverse l) 0 hl✝) = true
[PROOFSTEP]
rwa [nthLe, get_reverse']
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ dropWhile p (dropWhile p l) = dropWhile p l
[PROOFSTEP]
simp only [dropWhile_eq_self_iff]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ ∀ (hl : 0 < length (dropWhile p l)), ¬p (nthLe (dropWhile p l) 0 hl) = true
[PROOFSTEP]
exact fun h => dropWhile_nthLe_zero_not p l h
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ rtakeWhile p [] = []
[PROOFSTEP]
simp [rtakeWhile, takeWhile]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
x : α
⊢ rtakeWhile p (l ++ [x]) = if p x = true then rtakeWhile p l ++ [x] else []
[PROOFSTEP]
simp only [rtakeWhile, takeWhile, reverse_append, reverse_singleton, singleton_append]
[GOAL]
α : 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 []
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
p : α → Bool
l : List α
n : ℕ
x : α
h : p x = true
⊢ reverse
      (match p x with
      | true => x :: takeWhile p (reverse l)
      | false => []) =
    reverse (takeWhile p (reverse l)) ++ [x]
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
p : α → Bool
l : List α
n : ℕ
x : α
h : ¬p x = true
⊢ reverse
      (match p x with
      | true => x :: takeWhile p (reverse l)
      | false => []) =
    []
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
x : α
h : p x = true
⊢ rtakeWhile p (l ++ [x]) = rtakeWhile p l ++ [x]
[PROOFSTEP]
rw [rtakeWhile_concat, if_pos h]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
x : α
h : ¬p x = true
⊢ rtakeWhile p (l ++ [x]) = []
[PROOFSTEP]
rw [rtakeWhile_concat, if_neg h]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ rtakeWhile p l <:+ l
[PROOFSTEP]
rw [← reverse_prefix, rtakeWhile, reverse_reverse]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ takeWhile p (reverse l) <+: reverse l
[PROOFSTEP]
exact takeWhile_prefix _
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ rtakeWhile p l = l ↔ ∀ (x : α), x ∈ l → p x = true
[PROOFSTEP]
simp [rtakeWhile, reverse_eq_iff]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ rtakeWhile p l = [] ↔ ∀ (hl : l ≠ []), ¬p (getLast l hl) = true
[PROOFSTEP]
induction' l using List.reverseRecOn with l a
[GOAL]
case H0
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ rtakeWhile p [] = [] ↔ ∀ (hl : [] ≠ []), ¬p (getLast [] hl) = true
[PROOFSTEP]
simp only [rtakeWhile, takeWhile, reverse_nil, true_iff]
[GOAL]
case H0
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ ∀ (hl : [] ≠ []), ¬p (getLast [] hl) = true
[PROOFSTEP]
intro f
[GOAL]
case H0
α : Type u_1
p : α → Bool
l : List α
n : ℕ
f : [] ≠ []
⊢ ¬p (getLast [] f) = true
[PROOFSTEP]
contradiction
[GOAL]
case H1
α : Type u_1
p : α → Bool
l✝ : List α
n : ℕ
l : List α
a : α
a✝ : rtakeWhile p l = [] ↔ ∀ (hl : l ≠ []), ¬p (getLast l hl) = true
⊢ rtakeWhile p (l ++ [a]) = [] ↔ ∀ (hl : l ++ [a] ≠ []), ¬p (getLast (l ++ [a]) hl) = true
[PROOFSTEP]
simp only [rtakeWhile, reverse_append, takeWhile, reverse_eq_nil, getLast_append, ne_eq, append_eq_nil, and_false,
  forall_true_left]
[GOAL]
case H1
α : Type u_1
p : α → Bool
l✝ : List α
n : ℕ
l : List α
a : α
a✝ : rtakeWhile p l = [] ↔ ∀ (hl : l ≠ []), ¬p (getLast l hl) = true
⊢ (match p a with
      | true => a :: takeWhile p (List.append [] (reverse l))
      | false => []) =
      [] ↔
    ¬p a = true
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case H1.refine'_1
α : Type u_1
p : α → Bool
l✝ : List α
n : ℕ
l : List α
a : α
a✝ : rtakeWhile p l = [] ↔ ∀ (hl : l ≠ []), ¬p (getLast l hl) = true
h :
  (match p a with
    | true => a :: takeWhile p (List.append [] (reverse l))
    | false => []) =
    []
⊢ ¬p a = true
[PROOFSTEP]
intro pa
[GOAL]
case H1.refine'_1
α : Type u_1
p : α → Bool
l✝ : List α
n : ℕ
l : List α
a : α
a✝ : rtakeWhile p l = [] ↔ ∀ (hl : l ≠ []), ¬p (getLast l hl) = true
h :
  (match p a with
    | true => a :: takeWhile p (List.append [] (reverse l))
    | false => []) =
    []
pa : p a = true
⊢ False
[PROOFSTEP]
simp only [pa] at h 
[GOAL]
case H1.refine'_2
α : Type u_1
p : α → Bool
l✝ : List α
n : ℕ
l : List α
a : α
a✝ : rtakeWhile p l = [] ↔ ∀ (hl : l ≠ []), ¬p (getLast l hl) = true
h : ¬p a = true
⊢ (match p a with
    | true => a :: takeWhile p (List.append [] (reverse l))
    | false => []) =
    []
[PROOFSTEP]
simp only [h]
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
x : α
hx : x ∈ rtakeWhile p l
⊢ p x = true
[PROOFSTEP]
rw [rtakeWhile, mem_reverse] at hx 
[GOAL]
α : Type u_1
p : α → Bool
l : List α
n : ℕ
x : α
hx : x ∈ takeWhile p (reverse l)
⊢ p x = true
[PROOFSTEP]
exact mem_takeWhile_imp hx
