-- 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.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 < k.succ

Tactic:
exact Nat.lt_succ_of_lt hi

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
i : ℕ
h : [].Nodup
hi : i < [].length
⊢ [].prev [][i] ⋯ = [][(i + ([].length - 1)) % [].length]

Tactic:
simp at hi

Result:
no goals

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] = y
this : i.succ.succ = 1
⊢ False

Tactic:
simpa

Result:
no goals

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.succ.succ = 0

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

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 : (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, ⋯⟩

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

Tactic:
intro 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 : (x :: y :: l).Nodup
i : ℕ
hi : i + 1 + 1 < (x :: y :: l).length
H : (x :: y :: l)[i + 1 + 1] = x
⊢ False

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : l.Nodup
i : ℕ
hi : i < l.length
⊢ l.length > 0

Tactic:
omega

Result:
no goals

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 : ℕ
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

Tactic:
simp only [Nat.add_succ_sub_one, add_zero, 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 : ℕ
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 + (l.length + 1)) % (l.length + 1 + 1) = (i.succ + l.length) % (l.length + 1) + 1

Proof state:
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]

Tactic:
simp [getLast_eq_getElem]

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 : α
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]

Tactic:
push_neg 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:
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] =
    (y :: l)[(i.succ + ((y :: l).length - 1)) % (y :: l).length]

Tactic:
rw [this]

Result:
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]