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

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