α : Type u
β : Type v
δ : Type w
f : α → α
a : α
⊢ head (iterate f a) :: tail (iterate f a) = a :: iterate f (f a)
α : Type u
β : Type v
δ : Type w
f : α → α
a : α
⊢ iterate f a = a :: iterate f (f a)
rw [← Stream'.eta (iterate f a)]
α : Type u
β : Type v
δ : Type w
f : α → α
a : α
⊢ head (iterate f a) :: iterate f (f a) = a :: iterate f (f a)
α : Type u
β : Type v
δ : Type w
f : α → α
a : α
⊢ head (iterate f a) :: tail (iterate f a) = a :: iterate f (f a)
rw [tail_iterate]
no goals
α : Type u
β : Type v
δ : Type w
f : α → α
a : α
⊢ head (iterate f a) :: iterate f (f a) = a :: iterate f (f a)
rfl