α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : WSeq α
⊢ Seq.map (Option.map (g ∘ f)) s = Seq.map (Option.map g) (Seq.map (Option.map f) s)
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : WSeq α
⊢ map (g ∘ f) s = map g (map f s)
dsimp [map]
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : WSeq α
⊢ Seq.map (Option.map (g ∘ f)) s = Seq.map (Option.map g ∘ Option.map f) s
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : WSeq α
⊢ Seq.map (Option.map (g ∘ f)) s = Seq.map (Option.map g) (Seq.map (Option.map f) s)
rw [← Seq.map_comp]
case h
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : WSeq α
⊢ Seq.map (Option.map (g ∘ f)) = fun s => Seq.map (Option.map g ∘ Option.map f) s
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : WSeq α
⊢ Seq.map (Option.map (g ∘ f)) s = Seq.map (Option.map g ∘ Option.map f) s
apply congr_fun
case h.h
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : WSeq α
⊢ Option.map (g ∘ f) = Option.map g ∘ Option.map f
case h
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : WSeq α
⊢ Seq.map (Option.map (g ∘ f)) = fun s => Seq.map (Option.map g ∘ Option.map f) s
apply congr_arg
no goals
case h.h
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : WSeq α
⊢ Option.map (g ∘ f) = Option.map g ∘ Option.map f
ext ⟨⟩ <;> rfl