α β γ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : CommApplicative F
inst✝ : CommApplicative G
g : α → G β
h : β → γ
s : Finset α
⊢ Functor.map h <$> Multiset.toFinset <$> Multiset.traverse g s.val =
    Multiset.toFinset <$> Multiset.traverse (Functor.map h ∘ g) s.val
α β γ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : CommApplicative F
inst✝ : CommApplicative G
g : α → G β
h : β → γ
s : Finset α
⊢ Functor.map h <$> traverse g s = traverse (Functor.map h ∘ g) s
unfold traverse
α β γ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : CommApplicative F
inst✝ : CommApplicative G
g : α → G β
h : β → γ
s : Finset α
⊢ (Multiset.toFinset ∘ Functor.map h) <$> Multiset.traverse g s.val =
    Multiset.toFinset <$> Multiset.traverse (Functor.map h ∘ g) s.val
α β γ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : CommApplicative F
inst✝ : CommApplicative G
g : α → G β
h : β → γ
s : Finset α
⊢ Functor.map h <$> Multiset.toFinset <$> Multiset.traverse g s.val =
    Multiset.toFinset <$> Multiset.traverse (Functor.map h ∘ g) s.val
simp only [map_comp_coe, functor_norm]
no goals
α β γ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : CommApplicative F
inst✝ : CommApplicative G
g : α → G β
h : β → γ
s : Finset α
⊢ (Multiset.toFinset ∘ Functor.map h) <$> Multiset.traverse g s.val =
    Multiset.toFinset <$> Multiset.traverse (Functor.map h ∘ g) s.val
rw [LawfulFunctor.comp_map, Multiset.map_traverse]