-- Mathlib/Data/List/DropRight.lean
theorem rtakeWhile_eq_nil_iff : rtakeWhile p l = [] ↔ ∀ hl : l ≠ [], ¬p (l.getLast hl)

Proof state:
case append_singleton.refine_2
α : Type u_1
p : α → Bool
l✝ l : List α
a : α
a✝ : rtakeWhile p l = [] ↔ ∀ (hl : l ≠ []), ¬p (l.getLast hl) = true
h : ¬l ++ [a] = [] → ¬p a = true
⊢ (match p a with
      | true => a :: takeWhile p l.reverse
      | false => []).reverse =
    []

Tactic:
simp [h]

Result:
no goals

Proof state:
case nil
α : Type u_1
p : α → Bool
l : List α
f : [] ≠ []
⊢ ¬p ([].getLast f) = true

Tactic:
contradiction

Result:
no goals

Proof state:
case append_singleton
α : Type u_1
p : α → Bool
l✝ l : List α
a : α
a✝ : rtakeWhile p l = [] ↔ ∀ (hl : l ≠ []), ¬p (l.getLast hl) = true
⊢ rtakeWhile p (l ++ [a]) = [] ↔ ∀ (hl : l ++ [a] ≠ []), ¬p ((l ++ [a]).getLast hl) = true

Tactic:
simp only [rtakeWhile, reverse_append, reverse_cons, reverse_nil, nil_append, singleton_append,
  takeWhile, ne_eq, cons_ne_self, not_false_eq_true, getLast_append_of_ne_nil,
  getLast_singleton]

Result:
case append_singleton
α : Type u_1
p : α → Bool
l✝ l : List α
a : α
a✝ : rtakeWhile p l = [] ↔ ∀ (hl : l ≠ []), ¬p (l.getLast hl) = true
⊢ (match p a with
        | true => a :: takeWhile p l.reverse
        | false => []).reverse =
      [] ↔
    ¬l ++ [a] = [] → ¬p a = true

Proof state:
case append_singleton
α : Type u_1
p : α → Bool
l✝ l : List α
a : α
a✝ : rtakeWhile p l = [] ↔ ∀ (hl : l ≠ []), ¬p (l.getLast hl) = true
⊢ (match p a with
        | true => a :: takeWhile p l.reverse
        | false => []).reverse =
      [] ↔
    ¬l ++ [a] = [] → ¬p a = true

Tactic:
refine ⟨fun h => ?_ , fun h => ?_⟩

Result:
case append_singleton.refine_1
α : Type u_1
p : α → Bool
l✝ l : List α
a : α
a✝ : rtakeWhile p l = [] ↔ ∀ (hl : l ≠ []), ¬p (l.getLast hl) = true
h :
  (match p a with
      | true => a :: takeWhile p l.reverse
      | false => []).reverse =
    []
⊢ ¬l ++ [a] = [] → ¬p a = true

case append_singleton.refine_2
α : Type u_1
p : α → Bool
l✝ l : List α
a : α
a✝ : rtakeWhile p l = [] ↔ ∀ (hl : l ≠ []), ¬p (l.getLast hl) = true
h : ¬l ++ [a] = [] → ¬p a = true
⊢ (match p a with
      | true => a :: takeWhile p l.reverse
      | false => []).reverse =
    []

Proof state:
case append_singleton.refine_1
α : Type u_1
p : α → Bool
l✝ l : List α
a : α
a✝ : rtakeWhile p l = [] ↔ ∀ (hl : l ≠ []), ¬p (l.getLast hl) = true
h :
  (match p a with
      | true => a :: takeWhile p l.reverse
      | false => []).reverse =
    []
⊢ ¬l ++ [a] = [] → ¬p a = true

Tactic:
split at h <;> simp_all

Result:
no goals

Proof state:
case nil
α : Type u_1
p : α → Bool
l : List α
⊢ ∀ (hl : [] ≠ []), ¬p ([].getLast hl) = true

Tactic:
intro f

Result:
case nil
α : Type u_1
p : α → Bool
l : List α
f : [] ≠ []
⊢ ¬p ([].getLast f) = true

Proof state:
case nil
α : Type u_1
p : α → Bool
l : List α
⊢ rtakeWhile p [] = [] ↔ ∀ (hl : [] ≠ []), ¬p ([].getLast hl) = true

Tactic:
simp only [rtakeWhile, takeWhile, reverse_nil, true_iff]

Result:
case nil
α : Type u_1
p : α → Bool
l : List α
⊢ ∀ (hl : [] ≠ []), ¬p ([].getLast hl) = true

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ rtakeWhile p l = [] ↔ ∀ (hl : l ≠ []), ¬p (l.getLast hl) = true

Tactic:
induction' l using List.reverseRecOn with l a

Result:
case nil
α : Type u_1
p : α → Bool
l : List α
⊢ rtakeWhile p [] = [] ↔ ∀ (hl : [] ≠ []), ¬p ([].getLast hl) = true

case append_singleton
α : Type u_1
p : α → Bool
l✝ l : List α
a : α
a✝ : rtakeWhile p l = [] ↔ ∀ (hl : l ≠ []), ¬p (l.getLast hl) = true
⊢ rtakeWhile p (l ++ [a]) = [] ↔ ∀ (hl : l ++ [a] ≠ []), ¬p ((l ++ [a]).getLast hl) = true