-- 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.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
⊢ False

Tactic:
suffices i.succ.succ = 1 by simpa

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

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

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

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

Tactic:
simp

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
⊢ 1 < (x :: y :: l).length

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

Tactic:
exact Nat.succ_lt_succ (Nat.lt_succ_of_lt hi)

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

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
⊢ False

Tactic:
suffices i.succ.succ = 0 by simpa

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

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 + (l.length + 1)) % (l.length + 1 + 1) = (i.succ + l.length) % (l.length + 1) + 1

Tactic:
simp only [length, Nat.succ_lt_succ_iff] at hi

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]
hi : i < l.length
⊢ (i + 1 + 1 + (l.length + 1)) % (l.length + 1 + 1) = (i.succ + l.length) % (l.length + 1) + 1

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

Tactic:
intro H

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
⊢ False