α : 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
α : Type u_1
p : α → Bool
l : List α
n : ℕ
hl : rdropWhile p l ≠ []
⊢ ¬p (getLast (rdropWhile p l) hl) = true
simp_rw [rdropWhile]
α : 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
α : 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
rw [getLast_reverse]
no goals
α : 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
exact dropWhile_nthLe_zero_not _ _ _