-- Mathlib/Data/List/Cycle.lean
theorem next_getElem (l : List α) (h : Nodup l) (i : Nat) (hi : i < l.length) :
    next l l[i] (get_mem _ _) =
      (l[(i + 1) % l.length]'(Nat.mod_lt _ (i.zero_le.trans_lt hi))) :=
  match l, h, i, hi with
  | [], _, i, hi => by simp at hi
  | [_], _, _, _ => by simp
  | x::y::l, _h, 0, h0 => by
    have h₁ : (x :: y :: l)[0] = x

Proof state:
case inl
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
h : l✝.Nodup
i : ℕ
hi✝ : i < l✝.length
x y : α
l : List α
hn : (x :: y :: l).Nodup
hi : l.length + 1 < (x :: y :: l).length
hx' : (x :: y :: l)[l.length + 1] ≠ x
hi' : l.length ≤ l.length
⊢ (x :: y :: l).next (x :: y :: l)[l.length + 1] ⋯ = (x :: y :: l)[(l.length + 1 + 1) % (x :: y :: l).length]

Tactic:
rw [next_getLast_cons]

Result:
case inl
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
h : l✝.Nodup
i : ℕ
hi✝ : i < l✝.length
x y : α
l : List α
hn : (x :: y :: l).Nodup
hi : l.length + 1 < (x :: y :: l).length
hx' : (x :: y :: l)[l.length + 1] ≠ x
hi' : l.length ≤ l.length
⊢ x = (x :: y :: l)[(l.length + 1 + 1) % (x :: y :: l).length]

case inl.h
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
h : l✝.Nodup
i : ℕ
hi✝ : i < l✝.length
x y : α
l : List α
hn : (x :: y :: l).Nodup
hi : l.length + 1 < (x :: y :: l).length
hx' : (x :: y :: l)[l.length + 1] ≠ x
hi' : l.length ≤ l.length
⊢ (x :: y :: l)[l.length + 1] ∈ y :: l

case inl.hy
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
h : l✝.Nodup
i : ℕ
hi✝ : i < l✝.length
x y : α
l : List α
hn : (x :: y :: l).Nodup
hi : l.length + 1 < (x :: y :: l).length
hx' : (x :: y :: l)[l.length + 1] ≠ x
hi' : l.length ≤ l.length
⊢ (x :: y :: l)[l.length + 1] ≠ x

case inl.hx
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
h : l✝.Nodup
i : ℕ
hi✝ : i < l✝.length
x y : α
l : List α
hn : (x :: y :: l).Nodup
hi : l.length + 1 < (x :: y :: l).length
hx' : (x :: y :: l)[l.length + 1] ≠ x
hi' : l.length ≤ l.length
⊢ (x :: y :: l)[l.length + 1] = (x :: y :: l).getLast ⋯

case inl.hl
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
h : l✝.Nodup
i : ℕ
hi✝ : i < l✝.length
x y : α
l : List α
hn : (x :: y :: l).Nodup
hi : l.length + 1 < (x :: y :: l).length
hx' : (x :: y :: l)[l.length + 1] ≠ x
hi' : l.length ≤ l.length
⊢ (y :: l).Nodup

Proof state:
case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
h : l✝.Nodup
i✝ : ℕ
hi✝ : i✝ < l✝.length
x y : α
l : List α
hn : (x :: y :: l).Nodup
i : ℕ
hi : i + 1 < (x :: y :: l).length
hx' : (x :: y :: l)[i + 1] ≠ x
hi'✝ : i ≤ l.length
hi' : i < l.length
⊢ (x :: y :: l)[i + 1] ≠ (x :: y :: l).getLast ⋯

Tactic:
rw [getLast_eq_getElem]

Result:
case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
h : l✝.Nodup
i✝ : ℕ
hi✝ : i✝ < l✝.length
x y : α
l : List α
hn : (x :: y :: l).Nodup
i : ℕ
hi : i + 1 < (x :: y :: l).length
hx' : (x :: y :: l)[i + 1] ≠ x
hi'✝ : i ≤ l.length
hi' : i < l.length
⊢ (x :: y :: l)[i + 1] ≠ (x :: y :: l)[(x :: y :: l).length - 1]

Proof state:
case inr.e_i
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
h : l✝.Nodup
i✝ : ℕ
hi✝ : i✝ < l✝.length
x y : α
l : List α
hn : (x :: y :: l).Nodup
i : ℕ
hi : i + 1 < (x :: y :: l).length
hx' : (x :: y :: l)[i + 1] ≠ x
hi'✝ : i ≤ l.length
hi' : i < l.length
⊢ (i + 1) % (y :: l).length + 1 = (i + 1 + 1) % (x :: y :: l).length

Tactic:
dsimp

Result:
case inr.e_i
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
h : l✝.Nodup
i✝ : ℕ
hi✝ : i✝ < l✝.length
x y : α
l : List α
hn : (x :: y :: l).Nodup
i : ℕ
hi : i + 1 < (x :: y :: l).length
hx' : (x :: y :: l)[i + 1] ≠ x
hi'✝ : i ≤ l.length
hi' : i < l.length
⊢ (i + 1) % (l.length + 1) + 1 = (i + 1 + 1) % (l.length + 1 + 1)

Proof state:
case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
h✝ : l✝.Nodup
i✝ : ℕ
hi✝ : i✝ < l✝.length
x y : α
l : List α
hn : (x :: y :: l).Nodup
i : ℕ
hi : i + 1 < (x :: y :: l).length
hx' : (x :: y :: l)[i + 1] ≠ x
hi'✝ : i ≤ l.length
hi' : i < l.length
h : (x :: y :: l)[i + 1] = (x :: y :: l)[(x :: y :: l).length - 1]
this : ⟨i + 1, hi⟩ = ⟨(x :: y :: l).length - 1, ⋯⟩
⊢ False

Tactic:
simp at this

Result:
case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
h✝ : l✝.Nodup
i✝ : ℕ
hi✝ : i✝ < l✝.length
x y : α
l : List α
hn : (x :: y :: l).Nodup
i : ℕ
hi : i + 1 < (x :: y :: l).length
hx' : (x :: y :: l)[i + 1] ≠ x
hi'✝ : i ≤ l.length
hi' : i < l.length
h : (x :: y :: l)[i + 1] = (x :: y :: l)[(x :: y :: l).length - 1]
this : i = l.length
⊢ False

Proof state:
case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
h✝ : l✝.Nodup
i✝ : ℕ
hi✝ : i✝ < l✝.length
x y : α
l : List α
hn : (x :: y :: l).Nodup
i : ℕ
hi : i + 1 < (x :: y :: l).length
hx' : (x :: y :: l)[i + 1] ≠ x
hi'✝ : i ≤ l.length
hi' : i < l.length
h : (x :: y :: l)[i + 1] = (x :: y :: l)[(x :: y :: l).length - 1]
this : i = l.length
⊢ False

Tactic:
simp [this] at hi'

Result:
no goals

Proof state:
case inr.h
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
h : l✝.Nodup
i✝ : ℕ
hi✝ : i✝ < l✝.length
x y : α
l : List α
hn : (x :: y :: l).Nodup
i : ℕ
hi : i + 1 < (x :: y :: l).length
hx' : (x :: y :: l)[i + 1] ≠ x
hi'✝ : i ≤ l.length
hi' : i < l.length
⊢ (i + 1) % (y :: l).length + 1 < (x :: y :: l).length

Tactic:
simp [Nat.mod_eq_of_lt (Nat.succ_lt_succ_iff.2 hi'), hi']

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
h : l✝.Nodup
i : ℕ
hi : i < l✝.length
x y : α
l : List α
_h : (x :: y :: l).Nodup
h0 : 0 < (x :: y :: l).length
h₁ : (x :: y :: l)[0] = x
⊢ (x :: y :: l).next (x :: y :: l)[0] ⋯ = (x :: y :: l)[(0 + 1) % (x :: y :: l).length]

Tactic:
rw [next_cons_cons_eq' _ _ _ _ _ h₁]

Result:
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
h : l✝.Nodup
i : ℕ
hi : i < l✝.length
x y : α
l : List α
_h : (x :: y :: l).Nodup
h0 : 0 < (x :: y :: l).length
h₁ : (x :: y :: l)[0] = x
⊢ y = (x :: y :: l)[(0 + 1) % (x :: y :: l).length]

Proof state:
case inl
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
h : l✝.Nodup
i : ℕ
hi✝ : i < l✝.length
x y : α
l : List α
hn : (x :: y :: l).Nodup
hi : l.length + 1 < (x :: y :: l).length
hx' : (x :: y :: l)[l.length + 1] ≠ x
hi' : l.length ≤ l.length
⊢ x = (x :: y :: l)[(l.length + 1 + 1) % (x :: y :: l).length]

Tactic:
simp [hi', get]

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
h : l✝.Nodup
i✝ : ℕ
hi✝ : i✝ < l✝.length
x y : α
l : List α
hn : (x :: y :: l).Nodup
i : ℕ
hi : i + 1 < (x :: y :: l).length
hx' : (x :: y :: l)[i + 1] ≠ x
hi'✝ : i ≤ l.length
hi' : i < l.length
⊢ (x :: y :: l)[(i + 1) % (y :: l).length + 1] = (x :: y :: l)[(i + 1 + 1) % (x :: y :: l).length]

Tactic:
congr

Result:
case inr.e_i
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
h : l✝.Nodup
i✝ : ℕ
hi✝ : i✝ < l✝.length
x y : α
l : List α
hn : (x :: y :: l).Nodup
i : ℕ
hi : i + 1 < (x :: y :: l).length
hx' : (x :: y :: l)[i + 1] ≠ x
hi'✝ : i ≤ l.length
hi' : i < l.length
⊢ (i + 1) % (y :: l).length + 1 = (i + 1 + 1) % (x :: y :: l).length

Proof state:
case inl.hy
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
h : l✝.Nodup
i : ℕ
hi✝ : i < l✝.length
x y : α
l : List α
hn : (x :: y :: l).Nodup
hi : l.length + 1 < (x :: y :: l).length
hx' : (x :: y :: l)[l.length + 1] ≠ x
hi' : l.length ≤ l.length
⊢ (x :: y :: l)[l.length + 1] ≠ x

Tactic:
exact hx'

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
h : l✝.Nodup
i✝ : ℕ
hi✝ : i✝ < l✝.length
x y : α
l : List α
hn : (x :: y :: l).Nodup
i : ℕ
hi : i + 1 < (x :: y :: l).length
hx' : (x :: y :: l)[i + 1] ≠ x
⊢ (x :: y :: l).next (x :: y :: l)[i + 1] ⋯ = (x :: y :: l)[(i + 1 + 1) % (x :: y :: l).length]

Tactic:
have hi' : i ≤ l.length := Nat.le_of_lt_succ (Nat.succ_lt_succ_iff.1 hi)

Result:
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
h : l✝.Nodup
i✝ : ℕ
hi✝ : i✝ < l✝.length
x y : α
l : List α
hn : (x :: y :: l).Nodup
i : ℕ
hi : i + 1 < (x :: y :: l).length
hx' : (x :: y :: l)[i + 1] ≠ x
hi' : i ≤ l.length
⊢ (x :: y :: l).next (x :: y :: l)[i + 1] ⋯ = (x :: y :: l)[(i + 1 + 1) % (x :: y :: l).length]