case hl
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : Nodup l
⊢ length (pmap (prev l) l (_ : ∀ (x : α), x ∈ l → x ∈ l)) = length (rotate l (length l - 1))

case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : Nodup l
⊢ ∀ (n : ℕ) (h₁ : n < length (pmap (prev l) l (_ : ∀ (x : α), x ∈ l → x ∈ l)))
    (h₂ : n < length (rotate l (length l - 1))),
    nthLe (pmap (prev l) l (_ : ∀ (x : α), x ∈ l → x ∈ l)) n h₁ = nthLe (rotate l (length l - 1)) n h₂
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : Nodup l
⊢ pmap (prev l) l (_ : ∀ (x : α), x ∈ l → x ∈ l) = rotate l (length l - 1)
apply List.ext_nthLe
no goals
case hl
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : Nodup l
⊢ length (pmap (prev l) l (_ : ∀ (x : α), x ∈ l → x ∈ l)) = length (rotate l (length l - 1))
simp
case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : Nodup l
n : ℕ
hn : n < length (pmap (prev l) l (_ : ∀ (x : α), x ∈ l → x ∈ l))
hn' : n < length (rotate l (length l - 1))
⊢ nthLe (pmap (prev l) l (_ : ∀ (x : α), x ∈ l → x ∈ l)) n hn = nthLe (rotate l (length l - 1)) n hn'
case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : Nodup l
⊢ ∀ (n : ℕ) (h₁ : n < length (pmap (prev l) l (_ : ∀ (x : α), x ∈ l → x ∈ l)))
    (h₂ : n < length (rotate l (length l - 1))),
    nthLe (pmap (prev l) l (_ : ∀ (x : α), x ∈ l → x ∈ l)) n h₁ = nthLe (rotate l (length l - 1)) n h₂
intro n hn hn'
no goals
case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : Nodup l
n : ℕ
hn : n < length (pmap (prev l) l (_ : ∀ (x : α), x ∈ l → x ∈ l))
hn' : n < length (rotate l (length l - 1))
⊢ nthLe (pmap (prev l) l (_ : ∀ (x : α), x ∈ l → x ∈ l)) n hn = nthLe (rotate l (length l - 1)) n hn'
rw [nthLe_rotate, nthLe_pmap, prev_nthLe _ h]