no goals
α β γ : Type u
t : Type u → Type u
inst✝² : Traversable t
inst✝¹ : IsLawfulTraversable t
inst✝ : Monoid γ
f : α → β
g : β → γ
xs : t α
⊢ foldMap g (f <$> xs) = foldMap (g ∘ f) xs
simp only [foldMap, traverse_map, Function.comp]