α : 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
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ rdropWhile p l = l ↔ ∀ (hl : l ≠ []), ¬p (getLast l hl) = true
simp only [rdropWhile, reverse_eq_iff, dropWhile_eq_self_iff, getLast_eq_get]
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

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
α : 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
refine' ⟨fun h hl => _, fun h hl => _⟩
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
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
rw [← length_pos, ← length_reverse] at hl
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
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
have := h hl
no goals
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
rwa [nthLe, get_reverse'] at this
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
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
rw [length_reverse, length_pos] at hl
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
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
have := h hl
no goals
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
rwa [nthLe, get_reverse']