α : Type u
β : Type v
δ : Type w
a : α
l : List α
h : l ≠ []
ainl : a ∈ l
⊢ a ∈ l ++ₛ cycle l h
α : Type u
β : Type v
δ : Type w
a : α
l : List α
h : l ≠ []
ainl : a ∈ l
⊢ a ∈ cycle l h
rw [cycle_eq]
no goals
α : Type u
β : Type v
δ : Type w
a : α
l : List α
h : l ≠ []
ainl : a ∈ l
⊢ a ∈ l ++ₛ cycle l h
exact mem_append_stream_left _ ainl