α : Type u
l : List α
hl : Nodup l
hn : l ≠ []
i j : ℕ
h : rotate l i = rotate l j
hi : i % length l < length l
⊢ i % length l = j % length l
α : Type u
l : List α
hl : Nodup l
hn : l ≠ []
i j : ℕ
h : rotate l i = rotate l j
⊢ i % length l = j % length l
have hi : i % l.length < l.length := mod_lt _ (length_pos_of_ne_nil hn)
α : Type u
l : List α
hl : Nodup l
hn : l ≠ []
i j : ℕ
h : rotate l i = rotate l j
hi : i % length l < length l
hj : j % length l < length l
⊢ i % length l = j % length l
α : Type u
l : List α
hl : Nodup l
hn : l ≠ []
i j : ℕ
h : rotate l i = rotate l j
hi : i % length l < length l
⊢ i % length l = j % length l
have hj : j % l.length < l.length := mod_lt _ (length_pos_of_ne_nil hn)
α : Type u
l : List α
hl : Nodup l
hn : l ≠ []
i j : ℕ
h : rotate l i = rotate l j
hi : i % length l < length l
hj : j % length l < length l
⊢ nthLe l (i % length l) hi = nthLe l (j % length l) hj
α : Type u
l : List α
hl : Nodup l
hn : l ≠ []
i j : ℕ
h : rotate l i = rotate l j
hi : i % length l < length l
hj : j % length l < length l
⊢ i % length l = j % length l
refine' (nodup_iff_nthLe_inj.mp hl) _ _ hi hj _
α : Type u
l : List α
hl : Nodup l
hn : l ≠ []
i j : ℕ
h : rotate l i = rotate l j
hi : i % length l < length l
hj : j % length l < length l
⊢ nthLe (rotate l i) ((length l - i % length l + i % length l) % length l)
      (_ : (length l - i % length l + i % length l) % length l < length (rotate l i)) =
    nthLe (rotate l j) ((length l - j % length l + j % length l) % length l)
      (_ : (length l - j % length l + j % length l) % length l < length (rotate l j))
α : Type u
l : List α
hl : Nodup l
hn : l ≠ []
i j : ℕ
h : rotate l i = rotate l j
hi : i % length l < length l
hj : j % length l < length l
⊢ nthLe l (i % length l) hi = nthLe l (j % length l) hj
rw [← nthLe_rotate' l i, ← nthLe_rotate' l j]
no goals
α : Type u
l : List α
hl : Nodup l
hn : l ≠ []
i j : ℕ
h : rotate l i = rotate l j
hi : i % length l < length l
hj : j % length l < length l
⊢ nthLe (rotate l i) ((length l - i % length l + i % length l) % length l)
      (_ : (length l - i % length l + i % length l) % length l < length (rotate l i)) =
    nthLe (rotate l j) ((length l - j % length l + j % length l) % length l)
      (_ : (length l - j % length l + j % length l) % length l < length (rotate l j))
simp [tsub_add_cancel_of_le, hi.le, hj.le, h]