case a
α : Type u
β : Type v
γ : Type w
f : α → β
a : α
s : Stream' (Option α)
al : IsSeq s
⊢ ↑(map f (cons a { val := s, property := al })) = ↑(cons (f a) (map f { val := s, property := al }))
α : Type u
β : Type v
γ : Type w
f : α → β
a : α
s : Stream' (Option α)
al : IsSeq s
⊢ map f (cons a { val := s, property := al }) = cons (f a) (map f { val := s, property := al })
apply Subtype.eq
case a
α : Type u
β : Type v
γ : Type w
f : α → β
a : α
s : Stream' (Option α)
al : IsSeq s
⊢ Stream'.map (Option.map f) (some a :: s) = some (f a) :: Stream'.map (Option.map f) s
case a
α : Type u
β : Type v
γ : Type w
f : α → β
a : α
s : Stream' (Option α)
al : IsSeq s
⊢ ↑(map f (cons a { val := s, property := al })) = ↑(cons (f a) (map f { val := s, property := al }))
dsimp [cons, map]
case a
α : Type u
β : Type v
γ : Type w
f : α → β
a : α
s : Stream' (Option α)
al : IsSeq s
⊢ Option.map f (some a) :: Stream'.map (Option.map f) s = some (f a) :: Stream'.map (Option.map f) s
case a
α : Type u
β : Type v
γ : Type w
f : α → β
a : α
s : Stream' (Option α)
al : IsSeq s
⊢ Stream'.map (Option.map f) (some a :: s) = some (f a) :: Stream'.map (Option.map f) s
rw [Stream'.map_cons]
no goals
case a
α : Type u
β : Type v
γ : Type w
f : α → β
a : α
s : Stream' (Option α)
al : IsSeq s
⊢ Option.map f (some a) :: Stream'.map (Option.map f) s = some (f a) :: Stream'.map (Option.map f) s
rfl