case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
n : ℕ
hn : n < length l
hx : nthLe l n hn ∈ l
⊢ prev l (next l (nthLe l n hn) hx) (_ : next l (nthLe l n hn) hx ∈ l) = nthLe l n hn
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
x : α
hx : x ∈ l
⊢ prev l (next l x hx) (_ : next l x hx ∈ l) = x
obtain ⟨n, hn, rfl⟩ := nthLe_of_mem hx
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
n : ℕ
hn : n < length l
hx : nthLe l n hn ∈ l
⊢ nthLe l ((n + 1 + (length l - 1)) % length l) (_ : (n + 1 + (length l - 1)) % length l < length l) = nthLe l n hn
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
n : ℕ
hn : n < length l
hx : nthLe l n hn ∈ l
⊢ prev l (next l (nthLe l n hn) hx) (_ : next l (nthLe l n hn) hx ∈ l) = nthLe l n hn
simp only [next_nthLe, prev_nthLe, h, Nat.mod_add_mod]
case intro.intro.nil
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
n : ℕ
h : Nodup []
hn : n < length []
hx : nthLe [] n hn ∈ []
⊢ nthLe [] ((n + 1 + (length [] - 1)) % length []) (_ : (n + 1 + (length [] - 1)) % length [] < length []) =
    nthLe [] n hn

case intro.intro.cons
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
n : ℕ
hd : α
tl : List α
h : Nodup (hd :: tl)
hn : n < length (hd :: tl)
hx : nthLe (hd :: tl) n hn ∈ hd :: tl
⊢ nthLe (hd :: tl) ((n + 1 + (length (hd :: tl) - 1)) % length (hd :: tl))
      (_ : (n + 1 + (length (hd :: tl) - 1)) % length (hd :: tl) < length (hd :: tl)) =
    nthLe (hd :: tl) n hn
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
n : ℕ
hn : n < length l
hx : nthLe l n hn ∈ l
⊢ nthLe l ((n + 1 + (length l - 1)) % length l) (_ : (n + 1 + (length l - 1)) % length l < length l) = nthLe l n hn
cases' l with hd tl
no goals
case intro.intro.nil
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
n : ℕ
h : Nodup []
hn : n < length []
hx : nthLe [] n hn ∈ []
⊢ nthLe [] ((n + 1 + (length [] - 1)) % length []) (_ : (n + 1 + (length [] - 1)) % length [] < length []) =
    nthLe [] n hn
simp at hx
case intro.intro.cons
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
n : ℕ
hd : α
tl : List α
h : Nodup (hd :: tl)
hn : n < length (hd :: tl)
hx : nthLe (hd :: tl) n hn ∈ hd :: tl
this : (n + 1 + length tl) % (length tl + 1) = n
⊢ nthLe (hd :: tl) ((n + 1 + (length (hd :: tl) - 1)) % length (hd :: tl))
      (_ : (n + 1 + (length (hd :: tl) - 1)) % length (hd :: tl) < length (hd :: tl)) =
    nthLe (hd :: tl) n hn
case intro.intro.cons
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
n : ℕ
hd : α
tl : List α
h : Nodup (hd :: tl)
hn : n < length (hd :: tl)
hx : nthLe (hd :: tl) n hn ∈ hd :: tl
⊢ nthLe (hd :: tl) ((n + 1 + (length (hd :: tl) - 1)) % length (hd :: tl))
      (_ : (n + 1 + (length (hd :: tl) - 1)) % length (hd :: tl) < length (hd :: tl)) =
    nthLe (hd :: tl) n hn
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]
no goals
case intro.intro.cons
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
n : ℕ
hd : α
tl : List α
h : Nodup (hd :: tl)
hn : n < length (hd :: tl)
hx : nthLe (hd :: tl) n hn ∈ hd :: tl
this : (n + 1 + length tl) % (length tl + 1) = n
⊢ nthLe (hd :: tl) ((n + 1 + (length (hd :: tl) - 1)) % length (hd :: tl))
      (_ : (n + 1 + (length (hd :: tl) - 1)) % length (hd :: tl) < length (hd :: tl)) =
    nthLe (hd :: tl) n hn
simp only [length_cons, Nat.succ_sub_succ_eq_sub, tsub_zero, Nat.succ_eq_add_one, this]
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
n : ℕ
hd : α
tl : List α
h : Nodup (hd :: tl)
hn✝ : n < length (hd :: tl)
hn : n < Nat.succ (length tl)
hx : nthLe (hd :: tl) n hn✝ ∈ hd :: tl
⊢ (n + 1 + length tl) % (length tl + 1) = n
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
n : ℕ
hd : α
tl : List α
h : Nodup (hd :: tl)
hn : n < length (hd :: tl)
hx : nthLe (hd :: tl) n hn ∈ hd :: tl
⊢ (n + 1 + length tl) % (length tl + 1) = n
rw [length_cons] at hn
no goals
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
n : ℕ
hd : α
tl : List α
h : Nodup (hd :: tl)
hn✝ : n < length (hd :: tl)
hn : n < Nat.succ (length tl)
hx : nthLe (hd :: tl) n hn✝ ∈ hd :: tl
⊢ (n + 1 + length tl) % (length tl + 1) = n
rw [add_assoc, add_comm 1, Nat.add_mod_right, Nat.mod_eq_of_lt hn]