-- Mathlib/Data/List/Cycle.lean
theorem prev_reverse_eq_next (l : List α) (h : Nodup l) (x : α) (hx : x ∈ l) :
    prev l.reverse x (mem_reverse.mpr hx) = next l x hx

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
x : α
hx : x ∈ l
⊢ l.reverse.prev x ⋯ = l.next x hx

Tactic:
obtain ⟨k, hk, rfl⟩ := getElem_of_mem hx

Result:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
⊢ l.reverse.prev l[k] ⋯ = l.next l[k] hx

Proof state:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
lpos : 0 < l.length
⊢ l.reverse.prev l[k] ⋯ = l.next l[k] hx

Tactic:
have key : l.length - 1 - k < l.length := by omega

Result:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
lpos : 0 < l.length
key : l.length - 1 - k < l.length
⊢ l.reverse.prev l[k] ⋯ = l.next l[k] hx

Proof state:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
⊢ l.reverse.prev l[k] ⋯ = l.next l[k] hx

Tactic:
have lpos : 0 < l.length := k.zero_le.trans_lt hk

Result:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
lpos : 0 < l.length
⊢ l.reverse.prev l[k] ⋯ = l.next l[k] hx

Proof state:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
lpos : 0 < l.length
key : l.length - 1 - k < l.length
⊢ (pmap l.reverse.prev l.reverse ⋯)[l.length - 1 - k] = (l.rotate 1)[k]

Tactic:
simp_rw [pmap_prev_eq_rotate_length_sub_one _ (nodup_reverse.mpr h), rotate_reverse,
  length_reverse, Nat.mod_eq_of_lt (Nat.sub_lt lpos Nat.succ_pos'),
  Nat.sub_sub_self (Nat.succ_le_of_lt lpos)]

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

Proof state:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
lpos : 0 < l.length
key : l.length - 1 - k < l.length
⊢ l.length - 1 - k < (pmap l.reverse.prev l.reverse ⋯).length

Tactic:
simpa

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
lpos : 0 < l.length
key : l.length - 1 - k < l.length
⊢ l.reverse.prev l.reverse[l.length - 1 - k] ⋯ = (l.rotate 1)[k]

Tactic:
rw [← getElem_pmap l.reverse.prev fun _ h => h]

Result:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
lpos : 0 < l.length
key : l.length - 1 - k < l.length
⊢ (pmap l.reverse.prev l.reverse ⋯)[l.length - 1 - k] = (l.rotate 1)[k]

case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
lpos : 0 < l.length
key : l.length - 1 - k < l.length
⊢ l.length - 1 - k < (pmap l.reverse.prev l.reverse ⋯).length

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
lpos : 0 < l.length
⊢ l.length - 1 - k < l.length

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
lpos : 0 < l.length
key : l.length - 1 - k < l.length
⊢ k < (pmap l.next l ⋯).length

Tactic:
simpa using hk

Result:
no goals

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

Tactic:
simp [Nat.sub_sub_self (Nat.le_sub_one_of_lt hk)]

Result:
no goals

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

Tactic:
rw [getElem_eq_getElem_reverse]

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

Proof state:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
lpos : 0 < l.length
key : l.length - 1 - k < l.length
⊢ l.reverse.prev l[k] ⋯ = l.next l[k] hx

Tactic:
rw [← getElem_pmap l.next (fun _ h => h) (by simpa using hk)]

Result:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
lpos : 0 < l.length
key : l.length - 1 - k < l.length
⊢ l.reverse.prev l[k] ⋯ = (pmap l.next l ⋯)[k]

Proof state:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
lpos : 0 < l.length
key : l.length - 1 - k < l.length
⊢ l.reverse.prev l[k] ⋯ = (pmap l.next l ⋯)[k]

Tactic:
simp_rw [getElem_eq_getElem_reverse (l := l), pmap_next_eq_rotate_one _ h]

Result:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
lpos : 0 < l.length
key : l.length - 1 - k < l.length
⊢ l.reverse.prev l.reverse[l.length - 1 - k] ⋯ = (l.rotate 1)[k]