-- 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 h.e'_3
α : 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
this : ∀ (k : ℕ) (hk : k < (y :: l).length), (y :: l)[k] = (x :: y :: l)[k + 1]
⊢ (x :: y :: l)[(i + 1 + 1 + ((x :: y :: l).length - 1)) % (x :: y :: l).length] =
    (x :: y :: l)[(i.succ + ((y :: l).length - 1)) % (y :: l).length + 1]

Tactic:
congr

Result:
case h.e'_3.e_i
α : 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
this : ∀ (k : ℕ) (hk : k < (y :: l).length), (y :: l)[k] = (x :: y :: l)[k + 1]
⊢ (i + 1 + 1 + ((x :: y :: l).length - 1)) % (x :: y :: l).length =
    (i.succ + ((y :: l).length - 1)) % (y :: l).length + 1

Proof state:
case cons
α : 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]
i : ℕ
x : α
h : (x :: y :: l).Nodup
hi : i < (x :: y :: l).length
⊢ (x :: y :: l).prev (x :: y :: l)[i] ⋯ = (x :: y :: l)[(i + ((x :: y :: l).length - 1)) % (x :: y :: l).length]

Tactic:
rcases i with (_ | _ | i)

Result:
case cons.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 < (x :: y :: l).length
⊢ (x :: y :: l).prev (x :: y :: l)[0] ⋯ = (x :: y :: l)[(0 + ((x :: y :: l).length - 1)) % (x :: y :: l).length]

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]

case cons.succ.succ
α : 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
⊢ (x :: y :: l).prev (x :: y :: l)[i + 1 + 1] ⋯ =
    (x :: y :: l)[(i + 1 + 1 + ((x :: y :: l).length - 1)) % (x :: y :: l).length]

Proof state:
case h.e'_3.e_i
α : 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 : ℕ
this : ∀ (k : ℕ) (hk : k < (y :: l).length), (y :: l)[k] = (x :: y :: l)[k + 1]
hi : i < l.length
⊢ (i + 1 + 1 + (l.length + 1)) % (l.length + 1 + 1) = (i.succ + l.length) % (l.length + 1) + 1

Tactic:
set k := l.length

Result:
case h.e'_3.e_i
α : 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 : ℕ
this : ∀ (k : ℕ) (hk : k < (y :: l).length), (y :: l)[k] = (x :: y :: l)[k + 1]
k : ℕ := l.length
hi : i < k
⊢ (i + 1 + 1 + (k + 1)) % (k + 1 + 1) = (i.succ + k) % (k + 1) + 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
⊢ 0 < (x :: y :: l).length

Tactic:
omega

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 : Function.Injective (x :: y :: l).get
i : ℕ
hi : i + 1 + 1 < (x :: y :: l).length
H : (x :: y :: l)[i + 1 + 1] = y
⊢ ⟨i + 1 + 1, hi⟩ = ⟨1, ⋯⟩

Tactic:
apply h

Result:
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 :: y :: l).get ⟨i + 1 + 1, hi⟩ = (x :: y :: l).get ⟨1, ⋯⟩

Proof state:
case cons.succ.succ
α : 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
⊢ (x :: y :: l).prev (x :: y :: l)[i + 1 + 1] ⋯ =
    (x :: y :: l)[(i + 1 + 1 + ((x :: y :: l).length - 1)) % (x :: y :: l).length]

Tactic:
rw [prev_ne_cons_cons]

Result:
case cons.succ.succ
α : 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
⊢ (y :: l).prev (x :: y :: l)[i + 1 + 1] ⋯ =
    (x :: y :: l)[(i + 1 + 1 + ((x :: y :: l).length - 1)) % (x :: y :: l).length]

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
⊢ (x :: y :: l)[i + 1 + 1] ≠ x

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
⊢ (x :: y :: l)[i + 1 + 1] ≠ y