case pos
α : Type u
l✝ l'✝ l l' : List α
hl : l = []
⊢ cyclicPermutations l ~r cyclicPermutations l' ↔ l ~r l'

case neg
α : Type u
l✝ l'✝ l l' : List α
hl : ¬l = []
⊢ cyclicPermutations l ~r cyclicPermutations l' ↔ l ~r l'
α : Type u
l✝ l'✝ l l' : List α
⊢ cyclicPermutations l ~r cyclicPermutations l' ↔ l ~r l'
by_cases hl : l = []
case neg
α : Type u
l✝ l'✝ l l' : List α
hl : ¬l = []
hl' : length (cyclicPermutations l) = length l
⊢ cyclicPermutations l ~r cyclicPermutations l' ↔ l ~r l'
case neg
α : Type u
l✝ l'✝ l l' : List α
hl : ¬l = []
⊢ cyclicPermutations l ~r cyclicPermutations l' ↔ l ~r l'
have hl' : l.cyclicPermutations.length = l.length := length_cyclicPermutations_of_ne_nil _ hl
case neg
α : Type u
l✝ l'✝ l l' : List α
hl : ¬l = []
hl' : length (cyclicPermutations l) = length l
h : cyclicPermutations l ~r cyclicPermutations l'
⊢ l ~r l'
case neg
α : Type u
l✝ l'✝ l l' : List α
hl : ¬l = []
hl' : length (cyclicPermutations l) = length l
⊢ cyclicPermutations l ~r cyclicPermutations l' ↔ l ~r l'
refine' ⟨fun h => _, IsRotated.cyclicPermutations⟩
case neg.intro
α : Type u
l✝ l'✝ l l' : List α
hl : ¬l = []
hl' : length (cyclicPermutations l) = length l
k : ℕ
hk : rotate (cyclicPermutations l) k = cyclicPermutations l'
⊢ l ~r l'
case neg
α : Type u
l✝ l'✝ l l' : List α
hl : ¬l = []
hl' : length (cyclicPermutations l) = length l
h : cyclicPermutations l ~r cyclicPermutations l'
⊢ l ~r l'
obtain ⟨k, hk⟩ := h
case neg.intro
α : Type u
l✝ l'✝ l l' : List α
hl : ¬l = []
hl' : length (cyclicPermutations l) = length l
k : ℕ
hk : rotate (cyclicPermutations l) k = cyclicPermutations l'
⊢ rotate l (k % length l) = l'
case neg.intro
α : Type u
l✝ l'✝ l l' : List α
hl : ¬l = []
hl' : length (cyclicPermutations l) = length l
k : ℕ
hk : rotate (cyclicPermutations l) k = cyclicPermutations l'
⊢ l ~r l'
refine' ⟨k % l.length, _⟩
case neg.intro
α : Type u
l✝ l'✝ l l' : List α
hl : ¬l = []
hl' : length (cyclicPermutations l) = length l
k : ℕ
hk : rotate (cyclicPermutations l) k = cyclicPermutations l'
hk' : k % length l < length l
⊢ rotate l (k % length l) = l'
case neg.intro
α : Type u
l✝ l'✝ l l' : List α
hl : ¬l = []
hl' : length (cyclicPermutations l) = length l
k : ℕ
hk : rotate (cyclicPermutations l) k = cyclicPermutations l'
⊢ rotate l (k % length l) = l'
have hk' : k % l.length < l.length := mod_lt _ (length_pos_of_ne_nil hl)
case neg.intro
α : Type u
l✝ l'✝ l l' : List α
hl : ¬l = []
hl' : length (cyclicPermutations l) = length l
k : ℕ
hk : rotate (cyclicPermutations l) k = cyclicPermutations l'
hk' : k % length l < length l
⊢ nthLe (rotate (cyclicPermutations l) k)
      ((length (cyclicPermutations l) - k % length (cyclicPermutations l) + k % length l) %
        length (cyclicPermutations l))
      (_ :
        (length (cyclicPermutations l) - k % length (cyclicPermutations l) + k % length l) %
            length (cyclicPermutations l) <
          length (rotate (cyclicPermutations l) k)) =
    l'
case neg.intro
α : Type u
l✝ l'✝ l l' : List α
hl : ¬l = []
hl' : length (cyclicPermutations l) = length l
k : ℕ
hk : rotate (cyclicPermutations l) k = cyclicPermutations l'
hk' : k % length l < length l
⊢ rotate l (k % length l) = l'
rw [← nthLe_cyclicPermutations _ _ (hk'.trans_le hl'.ge), ← nthLe_rotate' _ k]
no goals
case neg.intro
α : Type u
l✝ l'✝ l l' : List α
hl : ¬l = []
hl' : length (cyclicPermutations l) = length l
k : ℕ
hk : rotate (cyclicPermutations l) k = cyclicPermutations l'
hk' : k % length l < length l
⊢ nthLe (rotate (cyclicPermutations l) k)
      ((length (cyclicPermutations l) - k % length (cyclicPermutations l) + k % length l) %
        length (cyclicPermutations l))
      (_ :
        (length (cyclicPermutations l) - k % length (cyclicPermutations l) + k % length l) %
            length (cyclicPermutations l) <
          length (rotate (cyclicPermutations l) k)) =
    l'
simp [hk, hl', tsub_add_cancel_of_le hk'.le]
no goals
case pos
α : Type u
l✝ l'✝ l l' : List α
hl : l = []
⊢ cyclicPermutations l ~r cyclicPermutations l' ↔ l ~r l'
simp [hl, eq_comm]