case nil
α : Type u
l l' : List α
hn : Nodup []
⊢ Nodup (List.cyclicPermutations [])

case cons
α : Type u
l✝ l' : List α
x : α
l : List α
hn : Nodup (x :: l)
⊢ Nodup (List.cyclicPermutations (x :: l))
α : Type u
l✝ l' l : List α
hn : Nodup l
⊢ Nodup (List.cyclicPermutations l)
cases' l with x l
case cons
α : Type u
l✝ l' : List α
x : α
l : List α
hn : Nodup (x :: l)
⊢ ∀ (i j : ℕ) (h₁ : i < length (List.cyclicPermutations (x :: l))) (h₂ : j < length (List.cyclicPermutations (x :: l))),
    nthLe (List.cyclicPermutations (x :: l)) i h₁ = nthLe (List.cyclicPermutations (x :: l)) j h₂ → i = j
case cons
α : Type u
l✝ l' : List α
x : α
l : List α
hn : Nodup (x :: l)
⊢ Nodup (List.cyclicPermutations (x :: l))
rw [nodup_iff_nthLe_inj]
case cons
α : Type u
l✝ l' : List α
x : α
l : List α
hn : Nodup (x :: l)
i j : ℕ
hi : i < length (List.cyclicPermutations (x :: l))
hj : j < length (List.cyclicPermutations (x :: l))
h : nthLe (List.cyclicPermutations (x :: l)) i hi = nthLe (List.cyclicPermutations (x :: l)) j hj
⊢ i = j
case cons
α : Type u
l✝ l' : List α
x : α
l : List α
hn : Nodup (x :: l)
⊢ ∀ (i j : ℕ) (h₁ : i < length (List.cyclicPermutations (x :: l))) (h₂ : j < length (List.cyclicPermutations (x :: l))),
    nthLe (List.cyclicPermutations (x :: l)) i h₁ = nthLe (List.cyclicPermutations (x :: l)) j h₂ → i = j
intro i j hi hj h
case cons
α : Type u
l✝ l' : List α
x : α
l : List α
hn : Nodup (x :: l)
i j : ℕ
hi✝ : i < length (List.cyclicPermutations (x :: l))
hj✝ : j < length (List.cyclicPermutations (x :: l))
h : nthLe (List.cyclicPermutations (x :: l)) i hi✝ = nthLe (List.cyclicPermutations (x :: l)) j hj✝
hi : i < length l + 1
hj : j < length l + 1
⊢ i = j
case cons
α : Type u
l✝ l' : List α
x : α
l : List α
hn : Nodup (x :: l)
i j : ℕ
hi : i < length (List.cyclicPermutations (x :: l))
hj : j < length (List.cyclicPermutations (x :: l))
h : nthLe (List.cyclicPermutations (x :: l)) i hi = nthLe (List.cyclicPermutations (x :: l)) j hj
⊢ i = j
simp only [length_cyclicPermutations_cons] at hi hj
case cons
α : Type u
l✝ l' : List α
x : α
l : List α
hn : Nodup (x :: l)
i j : ℕ
hi✝ : i < length (List.cyclicPermutations (x :: l))
hj✝ : j < length (List.cyclicPermutations (x :: l))
h : nthLe (List.cyclicPermutations (x :: l)) i hi✝ = nthLe (List.cyclicPermutations (x :: l)) j hj✝
hi : i < length l + 1
hj : j < length l + 1
⊢ i % (length l + 1) = j % (length l + 1)
case cons
α : Type u
l✝ l' : List α
x : α
l : List α
hn : Nodup (x :: l)
i j : ℕ
hi✝ : i < length (List.cyclicPermutations (x :: l))
hj✝ : j < length (List.cyclicPermutations (x :: l))
h : nthLe (List.cyclicPermutations (x :: l)) i hi✝ = nthLe (List.cyclicPermutations (x :: l)) j hj✝
hi : i < length l + 1
hj : j < length l + 1
⊢ i = j
rw [← mod_eq_of_lt hi, ← mod_eq_of_lt hj]
case cons.hn
α : Type u
l✝ l' : List α
x : α
l : List α
hn : Nodup (x :: l)
i j : ℕ
hi✝ : i < length (List.cyclicPermutations (x :: l))
hj✝ : j < length (List.cyclicPermutations (x :: l))
h : nthLe (List.cyclicPermutations (x :: l)) i hi✝ = nthLe (List.cyclicPermutations (x :: l)) j hj✝
hi : i < length l + 1
hj : j < length l + 1
⊢ x :: l ≠ []

case cons.h
α : Type u
l✝ l' : List α
x : α
l : List α
hn : Nodup (x :: l)
i j : ℕ
hi✝ : i < length (List.cyclicPermutations (x :: l))
hj✝ : j < length (List.cyclicPermutations (x :: l))
h : nthLe (List.cyclicPermutations (x :: l)) i hi✝ = nthLe (List.cyclicPermutations (x :: l)) j hj✝
hi : i < length l + 1
hj : j < length l + 1
⊢ rotate (x :: l) i = rotate (x :: l) j
case cons
α : Type u
l✝ l' : List α
x : α
l : List α
hn : Nodup (x :: l)
i j : ℕ
hi✝ : i < length (List.cyclicPermutations (x :: l))
hj✝ : j < length (List.cyclicPermutations (x :: l))
h : nthLe (List.cyclicPermutations (x :: l)) i hi✝ = nthLe (List.cyclicPermutations (x :: l)) j hj✝
hi : i < length l + 1
hj : j < length l + 1
⊢ i % (length l + 1) = j % (length l + 1)
apply hn.rotate_congr
no goals
case nil
α : Type u
l l' : List α
hn : Nodup []
⊢ Nodup (List.cyclicPermutations [])
simp
no goals
case cons.hn
α : Type u
l✝ l' : List α
x : α
l : List α
hn : Nodup (x :: l)
i j : ℕ
hi✝ : i < length (List.cyclicPermutations (x :: l))
hj✝ : j < length (List.cyclicPermutations (x :: l))
h : nthLe (List.cyclicPermutations (x :: l)) i hi✝ = nthLe (List.cyclicPermutations (x :: l)) j hj✝
hi : i < length l + 1
hj : j < length l + 1
⊢ x :: l ≠ []
simp
no goals
case cons.h
α : Type u
l✝ l' : List α
x : α
l : List α
hn : Nodup (x :: l)
i j : ℕ
hi✝ : i < length (List.cyclicPermutations (x :: l))
hj✝ : j < length (List.cyclicPermutations (x :: l))
h : nthLe (List.cyclicPermutations (x :: l)) i hi✝ = nthLe (List.cyclicPermutations (x :: l)) j hj✝
hi : i < length l + 1
hj : j < length l + 1
⊢ rotate (x :: l) i = rotate (x :: l) j
simpa using h