case a
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
⊢ ↑(map (g ∘ f) { val := s, property := al }) = ↑(map g (map f { val := s, property := al }))
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
⊢ map (g ∘ f) { val := s, property := al } = map g (map f { val := s, property := al })
apply Subtype.eq
case a
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
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 (g (f val))) o) s =
    Stream'.map
      ((fun o => Option.rec none (fun val => some (g val)) o) ∘ fun o => Option.rec none (fun val => some (f val)) o) s
case a
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
⊢ ↑(map (g ∘ f) { val := s, property := al }) = ↑(map g (map f { val := s, property := al }))
dsimp [map]
case a
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
⊢ (fun o => Option.rec none (fun val => some (g (f val))) o) =
    (fun o => Option.rec none (fun val => some (g val)) o) ∘ fun o => Option.rec none (fun val => some (f val)) o
case a
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
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 (g (f val))) o) s =
    Stream'.map
      ((fun o => Option.rec none (fun val => some (g val)) o) ∘ fun o => Option.rec none (fun val => some (f val)) o) s
apply congr_arg fun f : _ → Option γ => Stream'.map f s
no goals
case a
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
⊢ (fun o => Option.rec none (fun val => some (g (f val))) o) =
    (fun o => Option.rec none (fun val => some (g val)) o) ∘ fun o => Option.rec none (fun val => some (f val)) o
ext ⟨⟩ <;> rfl