α : Type u
β : Type v
γ : Type w
s : WSeq α
f : α → WSeq β
g : β → WSeq γ
⊢ join (join (map (map g) (map f s))) ~ʷ join (map (fun x => join (map g (f x))) s)
α : Type u
β : Type v
γ : Type w
s : WSeq α
f : α → WSeq β
g : β → WSeq γ
⊢ bind (bind s f) g ~ʷ bind s fun x => bind (f x) g
simp [bind]
α : Type u
β : Type v
γ : Type w
s : WSeq α
f : α → WSeq β
g : β → WSeq γ
⊢ join (join (map (map g ∘ f) s)) ~ʷ join (map join (map (map g ∘ f) s))
α : Type u
β : Type v
γ : Type w
s : WSeq α
f : α → WSeq β
g : β → WSeq γ
⊢ join (join (map (map g) (map f s))) ~ʷ join (map (fun x => join (map g (f x))) s)
erw [← map_comp f (map g), map_comp (map g ∘ f) join]
no goals
α : Type u
β : Type v
γ : Type w
s : WSeq α
f : α → WSeq β
g : β → WSeq γ
⊢ join (join (map (map g ∘ f) s)) ~ʷ join (map join (map (map g ∘ f) s))
apply join_join