case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l l' : List α
h : l ~r l'
hn : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
⊢ next l (nthLe l k hk) hx = next l' (nthLe l k hk) (_ : nthLe l k hk ∈ l')
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l l' : List α
h : l ~r l'
hn : Nodup l
x : α
hx : x ∈ l
⊢ next l x hx = next l' x (_ : x ∈ l')
obtain ⟨k, hk, rfl⟩ := nthLe_of_mem hx
case intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
hn : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
n : ℕ
h : l ~r rotate l n
⊢ next l (nthLe l k hk) hx = next (rotate l n) (nthLe l k hk) (_ : nthLe l k hk ∈ rotate l n)
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l l' : List α
h : l ~r l'
hn : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
⊢ next l (nthLe l k hk) hx = next l' (nthLe l k hk) (_ : nthLe l k hk ∈ l')
obtain ⟨n, rfl⟩ := id h
case intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
hn : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
n : ℕ
h : l ~r rotate l n
⊢ nthLe l ((k + 1) % length l) (_ : (k + 1) % length l < length l) =
    next (rotate l n) (nthLe l k hk) (_ : nthLe l k hk ∈ rotate l n)
case intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
hn : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
n : ℕ
h : l ~r rotate l n
⊢ next l (nthLe l k hk) hx = next (rotate l n) (nthLe l k hk) (_ : nthLe l k hk ∈ rotate l n)
rw [next_nthLe _ hn]
case intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
hn : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
n : ℕ
h : l ~r rotate l n
⊢ nthLe l ((k + 1) % length l) (_ : (k + 1) % length l < length l) =
    next (rotate l n)
      (nthLe (rotate l n) ((length l - n % length l + k) % length l)
        (_ : (length l - n % length l + k) % length l < length (rotate l n)))
      (_ :
        nthLe (rotate l n) ((length l - n % length l + k) % length l)
            (_ : (length l - n % length l + k) % length l < length (rotate l n)) ∈
          rotate l n)
case intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
hn : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
n : ℕ
h : l ~r rotate l n
⊢ nthLe l ((k + 1) % length l) (_ : (k + 1) % length l < length l) =
    next (rotate l n) (nthLe l k hk) (_ : nthLe l k hk ∈ rotate l n)
simp_rw [← nthLe_rotate' _ n k]
case intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
hn : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
n : ℕ
h : l ~r rotate l n
⊢ nthLe (rotate l n) ((length l - n % length l + (k + 1) % length l) % length l)
      (_ : (length l - n % length l + (k + 1) % length l) % length l < length (rotate l n)) =
    nthLe (rotate l n) (((length l - n % length l + k) % length l + 1) % length (rotate l n))
      (_ : ((length l - n % length l + k) % length l + 1) % length (rotate l n) < length (rotate l n))
case intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
hn : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
n : ℕ
h : l ~r rotate l n
⊢ nthLe l ((k + 1) % length l) (_ : (k + 1) % length l < length l) =
    next (rotate l n)
      (nthLe (rotate l n) ((length l - n % length l + k) % length l)
        (_ : (length l - n % length l + k) % length l < length (rotate l n)))
      (_ :
        nthLe (rotate l n) ((length l - n % length l + k) % length l)
            (_ : (length l - n % length l + k) % length l < length (rotate l n)) ∈
          rotate l n)
rw [next_nthLe _ (h.nodup_iff.mp hn), ← nthLe_rotate' _ n]
no goals
case intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
hn : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
n : ℕ
h : l ~r rotate l n
⊢ nthLe (rotate l n) ((length l - n % length l + (k + 1) % length l) % length l)
      (_ : (length l - n % length l + (k + 1) % length l) % length l < length (rotate l n)) =
    nthLe (rotate l n) (((length l - n % length l + k) % length l + 1) % length (rotate l n))
      (_ : ((length l - n % length l + k) % length l + 1) % length (rotate l n) < length (rotate l n))
simp [add_assoc]