α : Type u
l l' : List α
h : l ~r l'
⊢ ∃ n, n ≤ length l ∧ rotate l n = l'
α : Type u
l l' : List α
⊢ l ~r l' ↔ ∃ n, n ≤ length l ∧ rotate l n = l'
refine' ⟨fun h => _, fun ⟨n, _, h⟩ => ⟨n, h⟩⟩
case intro
α : Type u
l : List α
n : ℕ
⊢ ∃ n_1, n_1 ≤ length l ∧ rotate l n_1 = rotate l n
α : Type u
l l' : List α
h : l ~r l'
⊢ ∃ n, n ≤ length l ∧ rotate l n = l'
obtain ⟨n, rfl⟩ := h
case intro.nil
α : Type u
n : ℕ
⊢ ∃ n_1, n_1 ≤ length [] ∧ rotate [] n_1 = rotate [] n

case intro.cons
α : Type u
n : ℕ
hd : α
tl : List α
⊢ ∃ n_1, n_1 ≤ length (hd :: tl) ∧ rotate (hd :: tl) n_1 = rotate (hd :: tl) n
case intro
α : Type u
l : List α
n : ℕ
⊢ ∃ n_1, n_1 ≤ length l ∧ rotate l n_1 = rotate l n
cases' l with hd tl
no goals
case intro.nil
α : Type u
n : ℕ
⊢ ∃ n_1, n_1 ≤ length [] ∧ rotate [] n_1 = rotate [] n
simp
case intro.cons
α : Type u
n : ℕ
hd : α
tl : List α
⊢ n % length (hd :: tl) ≤ length (hd :: tl)
case intro.cons
α : Type u
n : ℕ
hd : α
tl : List α
⊢ ∃ n_1, n_1 ≤ length (hd :: tl) ∧ rotate (hd :: tl) n_1 = rotate (hd :: tl) n
refine' ⟨n % (hd :: tl).length, _, rotate_mod _ _⟩
case intro.cons
α : Type u
n : ℕ
hd : α
tl : List α
⊢ length (hd :: tl) > 0
case intro.cons
α : Type u
n : ℕ
hd : α
tl : List α
⊢ n % length (hd :: tl) ≤ length (hd :: tl)
refine' (Nat.mod_lt _ _).le
no goals
case intro.cons
α : Type u
n : ℕ
hd : α
tl : List α
⊢ length (hd :: tl) > 0
simp