-- Mathlib/Data/List/Cycle.lean
theorem prev_next (l : List α) (h : Nodup l) (x : α) (hx : x ∈ l) :
    prev l (next l x hx) (next_mem _ _ _) = x

Proof state:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : n < l.length
hx : l[n] ∈ l
⊢ l.prev (l.next l[n] hx) ⋯ = l[n]

Tactic:
simp only [next_getElem, prev_getElem, h, Nat.mod_add_mod]

Result:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : n < l.length
hx : l[n] ∈ l
⊢ l[(n + 1 + (l.length - 1)) % l.length] = l[n]

Proof state:
case intro.intro.cons
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
hd : α
tl : List α
h : (hd :: tl).Nodup
hn : n < (hd :: tl).length
hx : (hd :: tl)[n] ∈ hd :: tl
⊢ (hd :: tl)[(n + 1 + ((hd :: tl).length - 1)) % (hd :: tl).length] = (hd :: tl)[n]

Tactic:
have : (n + 1 + length tl) % (length tl + 1) = n := by
  rw [length_cons] at hn
  rw [add_assoc, add_comm 1, Nat.add_mod_right, Nat.mod_eq_of_lt hn]

Result:
case intro.intro.cons
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
hd : α
tl : List α
h : (hd :: tl).Nodup
hn : n < (hd :: tl).length
hx : (hd :: tl)[n] ∈ hd :: tl
this : (n + 1 + tl.length) % (tl.length + 1) = n
⊢ (hd :: tl)[(n + 1 + ((hd :: tl).length - 1)) % (hd :: tl).length] = (hd :: tl)[n]

Proof state:
case intro.intro.nil
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
h : [].Nodup
hn : n < [].length
hx : [][n] ∈ []
⊢ [][(n + 1 + ([].length - 1)) % [].length] = [][n]

Tactic:
simp at hn

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
x : α
hx : x ∈ l
⊢ l.prev (l.next x hx) ⋯ = x

Tactic:
obtain ⟨n, hn, rfl⟩ := getElem_of_mem hx

Result:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : n < l.length
hx : l[n] ∈ l
⊢ l.prev (l.next l[n] hx) ⋯ = l[n]

Proof state:
case intro.intro.cons
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
hd : α
tl : List α
h : (hd :: tl).Nodup
hn : n < (hd :: tl).length
hx : (hd :: tl)[n] ∈ hd :: tl
this : (n + 1 + tl.length) % (tl.length + 1) = n
⊢ (hd :: tl)[(n + 1 + ((hd :: tl).length - 1)) % (hd :: tl).length] = (hd :: tl)[n]

Tactic:
simp only [length_cons, Nat.succ_sub_succ_eq_sub, Nat.sub_zero, Nat.succ_eq_add_one, this]

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : n < l.length
hx : l[n] ∈ l
⊢ l[(n + 1 + (l.length - 1)) % l.length] = l[n]

Tactic:
rcases l with - | ⟨hd, tl⟩

Result:
case intro.intro.nil
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
h : [].Nodup
hn : n < [].length
hx : [][n] ∈ []
⊢ [][(n + 1 + ([].length - 1)) % [].length] = [][n]

case intro.intro.cons
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
hd : α
tl : List α
h : (hd :: tl).Nodup
hn : n < (hd :: tl).length
hx : (hd :: tl)[n] ∈ hd :: tl
⊢ (hd :: tl)[(n + 1 + ((hd :: tl).length - 1)) % (hd :: tl).length] = (hd :: tl)[n]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
hd : α
tl : List α
h : (hd :: tl).Nodup
hn : n < (hd :: tl).length
hx : (hd :: tl)[n] ∈ hd :: tl
⊢ (n + 1 + tl.length) % (tl.length + 1) = n

Tactic:
rw [length_cons] at hn

Result:
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
hd : α
tl : List α
h : (hd :: tl).Nodup
hn✝ : n < (hd :: tl).length
hn : n < tl.length + 1
hx : (hd :: tl)[n] ∈ hd :: tl
⊢ (n + 1 + tl.length) % (tl.length + 1) = n

Proof state:
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
hd : α
tl : List α
h : (hd :: tl).Nodup
hn✝ : n < (hd :: tl).length
hn : n < tl.length + 1
hx : (hd :: tl)[n] ∈ hd :: tl
⊢ (n + 1 + tl.length) % (tl.length + 1) = n

Tactic:
rw [add_assoc, add_comm 1, Nat.add_mod_right, Nat.mod_eq_of_lt hn]

Result:
no goals