α : Type u
l l' : List α
⊢ (∃ n, n ≤ length l ∧ rotate l n = l') ↔ ∃ a, a < length l + 1 ∧ rotate l a = l'
α : Type u
l l' : List α
⊢ l ~r l' ↔ l' ∈ map (rotate l) (range (length l + 1))
simp_rw [mem_map, mem_range, isRotated_iff_mod]
no goals
α : Type u
l l' : List α
⊢ (∃ n, n ≤ length l ∧ rotate l n = l') ↔ ∃ a, a < length l + 1 ∧ rotate l a = l'
exact
  ⟨fun ⟨n, hn, h⟩ => ⟨n, Nat.lt_succ_of_le hn, h⟩,
    fun ⟨n, hn, h⟩ => ⟨n, Nat.le_of_lt_succ hn, h⟩⟩