case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
⊢ prev (reverse l) (nthLe l k hk) (_ : nthLe l k hk ∈ reverse l) = next l (nthLe l k hk) hx
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
x : α
hx : x ∈ l
⊢ prev (reverse l) x (_ : x ∈ reverse l) = next l x hx
obtain ⟨k, hk, rfl⟩ := nthLe_of_mem hx
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
lpos : 0 < length l
⊢ prev (reverse l) (nthLe l k hk) (_ : nthLe l k hk ∈ reverse l) = next l (nthLe l k hk) hx
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
⊢ prev (reverse l) (nthLe l k hk) (_ : nthLe l k hk ∈ reverse l) = next l (nthLe l k hk) hx
have lpos : 0 < l.length := k.zero_le.trans_lt hk
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
lpos : 0 < length l
key : length l - 1 - k < length l
⊢ prev (reverse l) (nthLe l k hk) (_ : nthLe l k hk ∈ reverse l) = next l (nthLe l k hk) hx
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
lpos : 0 < length l
⊢ prev (reverse l) (nthLe l k hk) (_ : nthLe l k hk ∈ reverse l) = next l (nthLe l k hk) hx
have key : l.length - 1 - k < l.length :=
  (Nat.sub_le _ _).trans_lt (tsub_lt_self lpos Nat.succ_pos')
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
lpos : 0 < length l
key : length l - 1 - k < length l
⊢ prev (reverse l) (nthLe l k hk) (_ : nthLe l k hk ∈ reverse l) =
    nthLe (pmap (next l) l (_ : ∀ (x : α), x ∈ l → x ∈ l)) k
      (_ : k < length (pmap (next l) l (_ : ∀ (x : α), x ∈ l → x ∈ l)))
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
lpos : 0 < length l
key : length l - 1 - k < length l
⊢ prev (reverse l) (nthLe l k hk) (_ : nthLe l k hk ∈ reverse l) = next l (nthLe l k hk) hx
rw [← nthLe_pmap l.next (fun _ h => h) (by simpa using hk)]
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
lpos : 0 < length l
key : length l - 1 - k < length l
⊢ prev (reverse l) (nthLe (reverse l) (length l - 1 - k) (_ : length l - 1 - k < length (reverse l)))
      (_ : nthLe (reverse l) (length l - 1 - k) (_ : length l - 1 - k < length (reverse l)) ∈ reverse l) =
    nthLe (rotate l 1) k (_ : k < length (rotate l 1))
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
lpos : 0 < length l
key : length l - 1 - k < length l
⊢ prev (reverse l) (nthLe l k hk) (_ : nthLe l k hk ∈ reverse l) =
    nthLe (pmap (next l) l (_ : ∀ (x : α), x ∈ l → x ∈ l)) k
      (_ : k < length (pmap (next l) l (_ : ∀ (x : α), x ∈ l → x ∈ l)))
simp_rw [← nthLe_reverse l k (key.trans_le (by simp)), pmap_next_eq_rotate_one _ h]
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
lpos : 0 < length l
key : length l - 1 - k < length l
⊢ nthLe (pmap (prev (reverse l)) (reverse l) (_ : ∀ (x : α), x ∈ reverse l → x ∈ reverse l)) (length l - 1 - k)
      ?intro.intro =
    nthLe (rotate l 1) k (_ : k < length (rotate l 1))

case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
lpos : 0 < length l
key : length l - 1 - k < length l
⊢ length l - 1 - k < length (pmap (prev (reverse l)) (reverse l) (_ : ∀ (x : α), x ∈ reverse l → x ∈ reverse l))
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
lpos : 0 < length l
key : length l - 1 - k < length l
⊢ prev (reverse l) (nthLe (reverse l) (length l - 1 - k) (_ : length l - 1 - k < length (reverse l)))
      (_ : nthLe (reverse l) (length l - 1 - k) (_ : length l - 1 - k < length (reverse l)) ∈ reverse l) =
    nthLe (rotate l 1) k (_ : k < length (rotate l 1))
rw [← nthLe_pmap l.reverse.prev fun _ h => h]
no goals
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
lpos : 0 < length l
key : length l - 1 - k < length l
⊢ k < length (pmap (next l) l (_ : ∀ (x : α), x ∈ l → x ∈ l))
simpa using hk
no goals
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
lpos : 0 < length l
key : length l - 1 - k < length l
⊢ length l ≤ length (reverse l)
simp
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
lpos : 0 < length l
key : length l - 1 - k < length l
⊢ nthLe (reverse (rotate l (Nat.succ 0))) (length l - 1 - k)
      (_ : length l - 1 - k < length (reverse (rotate l (Nat.succ 0)))) =
    nthLe (rotate l 1) k (_ : k < length (rotate l 1))
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
lpos : 0 < length l
key : length l - 1 - k < length l
⊢ nthLe (pmap (prev (reverse l)) (reverse l) (_ : ∀ (x : α), x ∈ reverse l → x ∈ reverse l)) (length l - 1 - k)
      ?intro.intro =
    nthLe (rotate l 1) k (_ : k < length (rotate l 1))
simp_rw [pmap_prev_eq_rotate_length_sub_one _ (nodup_reverse.mpr h), rotate_reverse,
  length_reverse, Nat.mod_eq_of_lt (tsub_lt_self lpos Nat.succ_pos'),
  tsub_tsub_cancel_of_le (Nat.succ_le_of_lt lpos)]
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
lpos : 0 < length l
key : length l - 1 - k < length l
⊢ nthLe (reverse (reverse (rotate l (Nat.succ 0)))) (length (reverse (rotate l (Nat.succ 0))) - 1 - (length l - 1 - k))
      ?intro.intro.h1 =
    nthLe (rotate l 1) k (_ : k < length (rotate l 1))

case intro.intro.h1
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
lpos : 0 < length l
key : length l - 1 - k < length l
⊢ length (reverse (rotate l (Nat.succ 0))) - 1 - (length l - 1 - k) < length (reverse (reverse (rotate l (Nat.succ 0))))

case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
lpos : 0 < length l
key : length l - 1 - k < length l
⊢ length l - 1 - k < length (pmap (prev (reverse l)) (reverse l) (_ : ∀ (x : α), x ∈ reverse l → x ∈ reverse l))
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
lpos : 0 < length l
key : length l - 1 - k < length l
⊢ nthLe (reverse (rotate l (Nat.succ 0))) (length l - 1 - k)
      (_ : length l - 1 - k < length (reverse (rotate l (Nat.succ 0)))) =
    nthLe (rotate l 1) k (_ : k < length (rotate l 1))
rw [← nthLe_reverse]
no goals
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
lpos : 0 < length l
key : length l - 1 - k < length l
⊢ length l - 1 - k < length (pmap (prev (reverse l)) (reverse l) (_ : ∀ (x : α), x ∈ reverse l → x ∈ reverse l))
. simpa
no goals
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
lpos : 0 < length l
key : length l - 1 - k < length l
⊢ nthLe (reverse (reverse (rotate l (Nat.succ 0)))) (length (reverse (rotate l (Nat.succ 0))) - 1 - (length l - 1 - k))
      ?intro.intro.h1 =
    nthLe (rotate l 1) k (_ : k < length (rotate l 1))
simp [tsub_tsub_cancel_of_le (Nat.le_pred_of_lt hk)]
no goals
case intro.intro.h1
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
lpos : 0 < length l
key : length l - 1 - k < length l
⊢ length (reverse (rotate l (Nat.succ 0))) - 1 - (length l - 1 - k) < length (reverse (reverse (rotate l (Nat.succ 0))))
simpa using (Nat.sub_le _ _).trans_lt (tsub_lt_self lpos Nat.succ_pos')
no goals
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
lpos : 0 < length l
key : length l - 1 - k < length l
⊢ length l - 1 - k < length (pmap (prev (reverse l)) (reverse l) (_ : ∀ (x : α), x ∈ reverse l → x ∈ reverse l))
simpa