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