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

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

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

Tactic:
simp

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

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 + 1 + 1, hi⟩ = ⟨1, ⋯⟩

Tactic:
rw [nodup_iff_injective_get] at 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 : 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, ⋯⟩

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
⊢ (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:
convert hl i.succ y h.of_cons (Nat.le_of_succ_le_succ hi) using 1

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
⊢ (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]

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 + 1 + 1, hi⟩ = ⟨1, ⋯⟩
⊢ i.succ.succ = 1

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

Result:
no goals

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
⊢ (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:
have : ∀ k hk, (y :: l)[k] = (x :: y :: l)[k + 1]'(Nat.succ_lt_succ hk) := by
  simp

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

Tactic:
rw [Nat.succ_add, ← Nat.add_succ, Nat.add_mod_right, Nat.succ_add, ← Nat.add_succ _ k,
  Nat.add_mod_right, Nat.mod_eq_of_lt, Nat.mod_eq_of_lt]

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

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