-- 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.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 ⋯

Tactic:
simp [getLast_eq_getElem]

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

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

Tactic:
have h₁ : (x :: y :: l)[0] = x := by simp

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

Tactic:
exact get_mem _ _

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 : Function.Injective (x :: y :: l).get
i : ℕ
hi : i + 1 < (x :: y :: l).length
H : (x :: y :: l)[i + 1] = x
⊢ i + 1 = 0

Tactic:
refine Fin.val_eq_of_eq (@hn ⟨i + 1, hi⟩ ⟨0, by simp⟩ ?_)

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

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

Tactic:
rw [getElem_cons_succ]

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

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

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

Result:
no goals

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

Tactic:
exact hn.of_cons

Result:
no goals

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

Tactic:
exact get_mem _ _

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
⊢ i + 1 = 0

Tactic:
rw [nodup_iff_injective_get] at hn

Result:
α : 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
⊢ i + 1 = 0

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)[i + 1] ≠ x

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

Tactic:
rw [next_ne_head_ne_getLast _ _ _ _ _ hx']

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

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

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

Tactic:
simp

Result:
no goals