-- 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
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).next (x :: y :: l)[i + 1] ⋯ = (x :: y :: l)[(i + 1 + 1) % (x :: y :: l).length]

Tactic:
subst hi'

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 :: y :: l).next (x :: y :: l)[l.length + 1] ⋯ = (x :: y :: l)[(l.length + 1 + 1) % (x :: y :: l).length]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
h : l✝.Nodup
i✝ : ℕ
hi✝ : i✝ < l✝.length
x y : α
l : List α
hn : Function.Injective (x :: y :: l).get
i : ℕ
hi : i + 1 < (x :: y :: l).length
H : (x :: y :: l)[i + 1] = x
⊢ (x :: y :: l).get ⟨i + 1, hi⟩ = (x :: y :: l).get ⟨0, ⋯⟩

Tactic:
simpa using H

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
⊢ (x :: y :: l)[0] = x

Tactic:
simp

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

Tactic:
have hx' : (x :: y :: l)[i+1] ≠ x := by
  intro H
  suffices (i + 1 : ℕ) = 0 by simpa
  rw [nodup_iff_injective_get] at hn
  refine Fin.val_eq_of_eq (@hn ⟨i + 1, hi⟩ ⟨0, by simp⟩ ?_)
  simpa using H

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

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
hi' : i ≤ l.length
⊢ (x :: y :: l).next (x :: y :: l)[i + 1] ⋯ = (x :: y :: l)[(i + 1 + 1) % (x :: y :: l).length]

Tactic:
rcases hi'.eq_or_lt with (hi' | hi')

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
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).next (x :: y :: l)[i + 1] ⋯ = (x :: y :: l)[(i + 1 + 1) % (x :: y :: l).length]

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).next (x :: y :: l)[i + 1] ⋯ = (x :: y :: l)[(i + 1 + 1) % (x :: y :: l).length]

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

Tactic:
rw [next_getElem (y::l), ← getElem_cons_succ (a := x)]

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

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

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
⊢ (y :: l).Nodup

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
⊢ (y :: l).Nodup

Tactic:
exact hn.of_cons

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

Tactic:
suffices (i + 1 : ℕ) = 0 by simpa

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

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

Tactic:
simp at hi

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

Tactic:
intro h

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

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

Tactic:
rw [getElem_cons_succ]

Result:
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
⊢ (y :: l)[l.length] ∈ y :: l