-- Mathlib/Data/List/Cycle.lean
theorem prev_getElem (l : List α) (h : Nodup l) (i : Nat) (hi : i < l.length) :
    prev l l[i] (get_mem _ _) =
      (l[(i + (l.length - 1)) % l.length]'(Nat.mod_lt _ (by omega))) :=
  match l with
  | [] => by simp at hi
  | x::l => by
    induction l generalizing i x with
    | nil => simp
    | cons y l hl =>
      rcases i with (_ | _ | i)
      · simp [getLast_eq_getElem]
      · simp only [mem_cons, nodup_cons] at h
        push_neg at h
        simp only [zero_add, getElem_cons_succ, getElem_cons_zero,
          List.prev_cons_cons_of_ne _ _ _ _ h.left.left.symm, length, add_comm,
          Nat.add_sub_cancel_left, Nat.mod_self]
      · rw [prev_ne_cons_cons]
        · convert hl i.succ y h.of_cons (Nat.le_of_succ_le_succ hi) using 1
          have : ∀ k hk, (y :: l)[k] = (x :: y :: l)[k + 1]'(Nat.succ_lt_succ hk)

Proof state:
case cons.succ.succ.hy
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
y : α
l : List α
hl :
  ∀ (i : ℕ) (x : α),
    (x :: l).Nodup →
      ∀ (hi : i < (x :: l).length),
        (x :: l).prev (x :: l)[i] ⋯ = (x :: l)[(i + ((x :: l).length - 1)) % (x :: l).length]
x : α
h : (x :: y :: l).Nodup
i : ℕ
hi : i + 1 + 1 < (x :: y :: l).length
H : (x :: y :: l)[i + 1 + 1] = x
⊢ ⟨i + 1 + 1, hi⟩ = ⟨0, ⋯⟩

Tactic:
rw [nodup_iff_injective_get] at h

Result:
case cons.succ.succ.hy
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
y : α
l : List α
hl :
  ∀ (i : ℕ) (x : α),
    (x :: l).Nodup →
      ∀ (hi : i < (x :: l).length),
        (x :: l).prev (x :: l)[i] ⋯ = (x :: l)[(i + ((x :: l).length - 1)) % (x :: l).length]
x : α
h : Function.Injective (x :: y :: l).get
i : ℕ
hi : i + 1 + 1 < (x :: y :: l).length
H : (x :: y :: l)[i + 1 + 1] = x
⊢ ⟨i + 1 + 1, hi⟩ = ⟨0, ⋯⟩

Proof state:
case cons.succ.succ.hz.a
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
y : α
l : List α
hl :
  ∀ (i : ℕ) (x : α),
    (x :: l).Nodup →
      ∀ (hi : i < (x :: l).length),
        (x :: l).prev (x :: l)[i] ⋯ = (x :: l)[(i + ((x :: l).length - 1)) % (x :: l).length]
x : α
h : Function.Injective (x :: y :: l).get
i : ℕ
hi : i + 1 + 1 < (x :: y :: l).length
H : (x :: y :: l)[i + 1 + 1] = y
⊢ (x :: (x :: y :: l)[i + 1 + 1] :: l).get ⟨i + 1 + 1, hi⟩ = (x :: (x :: y :: l)[i + 1 + 1] :: l).get ⟨1, ⋯⟩

Tactic:
simp

Result:
no goals

Proof state:
case cons.succ.succ.hz
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
y : α
l : List α
hl :
  ∀ (i : ℕ) (x : α),
    (x :: l).Nodup →
      ∀ (hi : i < (x :: l).length),
        (x :: l).prev (x :: l)[i] ⋯ = (x :: l)[(i + ((x :: l).length - 1)) % (x :: l).length]
x : α
h : (x :: y :: l).Nodup
i : ℕ
hi : i + 1 + 1 < (x :: y :: l).length
H : (x :: y :: l)[i + 1 + 1] = y
⊢ i.succ.succ = 1

Tactic:
suffices Fin.mk _ hi = ⟨1, by omega⟩ by rwa [Fin.mk.inj_iff] at this

Result:
case cons.succ.succ.hz
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
y : α
l : List α
hl :
  ∀ (i : ℕ) (x : α),
    (x :: l).Nodup →
      ∀ (hi : i < (x :: l).length),
        (x :: l).prev (x :: l)[i] ⋯ = (x :: l)[(i + ((x :: l).length - 1)) % (x :: l).length]
x : α
h : (x :: y :: l).Nodup
i : ℕ
hi : i + 1 + 1 < (x :: y :: l).length
H : (x :: y :: l)[i + 1 + 1] = y
⊢ ⟨i + 1 + 1, hi⟩ = ⟨1, ⋯⟩

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
y : α
l : List α
hl :
  ∀ (i : ℕ) (x : α),
    (x :: l).Nodup →
      ∀ (hi : i < (x :: l).length),
        (x :: l).prev (x :: l)[i] ⋯ = (x :: l)[(i + ((x :: l).length - 1)) % (x :: l).length]
x : α
h : (x :: y :: l).Nodup
i : ℕ
hi : i + 1 + 1 < (x :: y :: l).length
H : (x :: y :: l)[i + 1 + 1] = x
this : ⟨i + 1 + 1, hi⟩ = ⟨0, ⋯⟩
⊢ i.succ.succ = 0

Tactic:
rwa [Fin.mk.inj_iff] at this

Result:
no goals

Proof state:
case cons.succ.zero
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
y : α
l : List α
hl :
  ∀ (i : ℕ) (x : α),
    (x :: l).Nodup →
      ∀ (hi : i < (x :: l).length),
        (x :: l).prev (x :: l)[i] ⋯ = (x :: l)[(i + ((x :: l).length - 1)) % (x :: l).length]
x : α
h : (x :: y :: l).Nodup
hi : 0 + 1 < (x :: y :: l).length
⊢ (x :: y :: l).prev (x :: y :: l)[0 + 1] ⋯ = (x :: y :: l)[(0 + 1 + ((x :: y :: l).length - 1)) % (x :: y :: l).length]

Tactic:
simp only [mem_cons, nodup_cons] at h

Result:
case cons.succ.zero
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
y : α
l : List α
hl :
  ∀ (i : ℕ) (x : α),
    (x :: l).Nodup →
      ∀ (hi : i < (x :: l).length),
        (x :: l).prev (x :: l)[i] ⋯ = (x :: l)[(i + ((x :: l).length - 1)) % (x :: l).length]
x : α
hi : 0 + 1 < (x :: y :: l).length
h : ¬(x = y ∨ x ∈ l) ∧ y ∉ l ∧ l.Nodup
⊢ (x :: y :: l).prev (x :: y :: l)[0 + 1] ⋯ = (x :: y :: l)[(0 + 1 + ((x :: y :: l).length - 1)) % (x :: y :: l).length]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
y : α
l : List α
hl :
  ∀ (i : ℕ) (x : α),
    (x :: l).Nodup →
      ∀ (hi : i < (x :: l).length),
        (x :: l).prev (x :: l)[i] ⋯ = (x :: l)[(i + ((x :: l).length - 1)) % (x :: l).length]
x : α
h : (x :: y :: l).Nodup
i : ℕ
hi : i + 1 + 1 < (x :: y :: l).length
H : (x :: y :: l)[i + 1 + 1] = x
this : i.succ.succ = 0
⊢ False

Tactic:
simpa

Result:
no goals

Proof state:
case cons.succ.succ.hy.a
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
y : α
l : List α
hl :
  ∀ (i : ℕ) (x : α),
    (x :: l).Nodup →
      ∀ (hi : i < (x :: l).length),
        (x :: l).prev (x :: l)[i] ⋯ = (x :: l)[(i + ((x :: l).length - 1)) % (x :: l).length]
x : α
h : Function.Injective (x :: y :: l).get
i : ℕ
hi : i + 1 + 1 < (x :: y :: l).length
H : (x :: y :: l)[i + 1 + 1] = x
⊢ (x :: y :: l).get ⟨i + 1 + 1, hi⟩ = (x :: y :: l).get ⟨0, ⋯⟩

Tactic:
rw [← H]

Result:
case cons.succ.succ.hy.a
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
y : α
l : List α
hl :
  ∀ (i : ℕ) (x : α),
    (x :: l).Nodup →
      ∀ (hi : i < (x :: l).length),
        (x :: l).prev (x :: l)[i] ⋯ = (x :: l)[(i + ((x :: l).length - 1)) % (x :: l).length]
x : α
h : Function.Injective (x :: y :: l).get
i : ℕ
hi : i + 1 + 1 < (x :: y :: l).length
H : (x :: y :: l)[i + 1 + 1] = x
⊢ ((x :: y :: l)[i + 1 + 1] :: y :: l).get ⟨i + 1 + 1, hi⟩ = ((x :: y :: l)[i + 1 + 1] :: y :: l).get ⟨0, ⋯⟩