case mp
α : Type u
l✝ l'✝ l l' : List α
⊢ l ∈ cyclicPermutations l' → l ~r l'

case mpr
α : Type u
l✝ l'✝ l l' : List α
⊢ l ~r l' → l ∈ cyclicPermutations l'
α : Type u
l✝ l'✝ l l' : List α
⊢ l ∈ cyclicPermutations l' ↔ l ~r l'
constructor
case mp
α : Type u
l✝ l'✝ l l' : List α
h : l ∈ cyclicPermutations l'
⊢ l ~r l'
case mp
α : Type u
l✝ l'✝ l l' : List α
⊢ l ∈ cyclicPermutations l' → l ~r l'
intro h
case mp.intro.intro
α : Type u
l l'✝ l' : List α
k : ℕ
hk : k < length (cyclicPermutations l')
h : nthLe (cyclicPermutations l') k hk ∈ cyclicPermutations l'
⊢ nthLe (cyclicPermutations l') k hk ~r l'
case mp
α : Type u
l✝ l'✝ l l' : List α
h : l ∈ cyclicPermutations l'
⊢ l ~r l'
obtain ⟨k, hk, rfl⟩ := nthLe_of_mem h
no goals
case mp.intro.intro
α : Type u
l l'✝ l' : List α
k : ℕ
hk : k < length (cyclicPermutations l')
h : nthLe (cyclicPermutations l') k hk ∈ cyclicPermutations l'
⊢ nthLe (cyclicPermutations l') k hk ~r l'
simp
case mpr
α : Type u
l✝ l'✝ l l' : List α
h : l ~r l'
⊢ l ∈ cyclicPermutations l'
case mpr
α : Type u
l✝ l'✝ l l' : List α
⊢ l ~r l' → l ∈ cyclicPermutations l'
intro h
case mpr.intro
α : Type u
l l'✝ l' : List α
k : ℕ
h : rotate l' k ~r l'
⊢ rotate l' k ∈ cyclicPermutations l'
case mpr
α : Type u
l✝ l'✝ l l' : List α
h : l ~r l'
⊢ l ∈ cyclicPermutations l'
obtain ⟨k, rfl⟩ := h.symm
case mpr.intro
α : Type u
l l'✝ l' : List α
k : ℕ
h : rotate l' k ~r l'
⊢ ∃ n h, nthLe (cyclicPermutations l') n h = rotate l' k
case mpr.intro
α : Type u
l l'✝ l' : List α
k : ℕ
h : rotate l' k ~r l'
⊢ rotate l' k ∈ cyclicPermutations l'
rw [mem_iff_nthLe]
case mpr.intro
α : Type u
l l'✝ l' : List α
k : ℕ
h : rotate l' k ~r l'
⊢ ∃ n, n < length (cyclicPermutations l') ∧ rotate l' n = rotate l' k
case mpr.intro
α : Type u
l l'✝ l' : List α
k : ℕ
h : rotate l' k ~r l'
⊢ ∃ n h, nthLe (cyclicPermutations l') n h = rotate l' k
simp only [exists_prop, nthLe_cyclicPermutations]
case mpr.intro.nil
α : Type u
l l' : List α
k : ℕ
h : rotate [] k ~r []
⊢ ∃ n, n < length (cyclicPermutations []) ∧ rotate [] n = rotate [] k

case mpr.intro.cons
α : Type u
l✝ l' : List α
k : ℕ
x : α
l : List α
h : rotate (x :: l) k ~r (x :: l)
⊢ ∃ n, n < length (cyclicPermutations (x :: l)) ∧ rotate (x :: l) n = rotate (x :: l) k
case mpr.intro
α : Type u
l l'✝ l' : List α
k : ℕ
h : rotate l' k ~r l'
⊢ ∃ n, n < length (cyclicPermutations l') ∧ rotate l' n = rotate l' k
cases' l' with x l
no goals
case mpr.intro.nil
α : Type u
l l' : List α
k : ℕ
h : rotate [] k ~r []
⊢ ∃ n, n < length (cyclicPermutations []) ∧ rotate [] n = rotate [] k
simp
case mpr.intro.cons
α : Type u
l✝ l' : List α
k : ℕ
x : α
l : List α
h : rotate (x :: l) k ~r (x :: l)
⊢ k % length (x :: l) < length (cyclicPermutations (x :: l))
case mpr.intro.cons
α : Type u
l✝ l' : List α
k : ℕ
x : α
l : List α
h : rotate (x :: l) k ~r (x :: l)
⊢ ∃ n, n < length (cyclicPermutations (x :: l)) ∧ rotate (x :: l) n = rotate (x :: l) k
refine' ⟨k % length (x :: l), _, rotate_mod _ _⟩
no goals
case mpr.intro.cons
α : Type u
l✝ l' : List α
k : ℕ
x : α
l : List α
h : rotate (x :: l) k ~r (x :: l)
⊢ k % length (x :: l) < length (cyclicPermutations (x :: l))
simpa using Nat.mod_lt _ (zero_lt_succ _)