case a
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
⊢ ↑(map f (think { val := s, property := al })) = ↑(think (map f { val := s, property := al }))
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
⊢ map f (think { val := s, property := al }) = think (map f { val := s, property := al })
apply Subtype.eq
case a
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
⊢ Stream'.map (fun o => Option.rec none (fun val => some (f val)) o) (Stream'.cons none s) =
    Stream'.cons none (Stream'.map (fun o => Option.rec none (fun val => some (f val)) o) s)
case a
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
⊢ ↑(map f (think { val := s, property := al })) = ↑(think (map f { val := s, property := al }))
dsimp [think, map]
no goals
case a
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
⊢ Stream'.map (fun o => Option.rec none (fun val => some (f val)) o) (Stream'.cons none s) =
    Stream'.cons none (Stream'.map (fun o => Option.rec none (fun val => some (f val)) o) s)
rw [Stream'.map_cons]