case a
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : IsSeq s
⊢ ↑(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 : IsSeq s
⊢ 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 : IsSeq s
⊢ Stream'.map (Option.map (g ∘ f)) s = Stream'.map (Option.map g ∘ Option.map f) s
case a
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : IsSeq s
⊢ ↑(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 : IsSeq s
⊢ Option.map (g ∘ f) = Option.map g ∘ Option.map f
case a
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : IsSeq s
⊢ Stream'.map (Option.map (g ∘ f)) s = Stream'.map (Option.map g ∘ Option.map f) 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 : IsSeq s
⊢ Option.map (g ∘ f) = Option.map g ∘ Option.map f
ext ⟨⟩ <;> rfl