no goals
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : IsLawfulTraversable t
xs : t α
⊢ ↑FreeMonoid.toList (foldMap FreeMonoid.of xs) =
    ↑FreeMonoid.toList (List.reverse (List.reverse (foldMap FreeMonoid.of xs)))
simp only [List.reverse_reverse]
no goals
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : IsLawfulTraversable t
xs : t α
⊢ ↑FreeMonoid.toList (List.reverse (List.reverse (foldMap FreeMonoid.of xs))) =
    ↑FreeMonoid.toList (List.reverse (List.foldr cons [] (List.reverse (foldMap FreeMonoid.of xs))))
simp only [List.foldr_eta]
no goals
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : IsLawfulTraversable t
xs : t α
⊢ ↑FreeMonoid.toList (List.reverse (List.foldr cons [] (List.reverse (foldMap FreeMonoid.of xs)))) =
    List.reverse (unop (↑(Foldl.ofFreeMonoid (flip cons)) (foldMap FreeMonoid.of xs)) [])
simp [flip, List.foldr_reverse, Foldl.ofFreeMonoid, unop_op]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : IsLawfulTraversable t
xs : t α
⊢ List.reverse (unop (foldMap (↑(Foldl.ofFreeMonoid (flip cons)) ∘ FreeMonoid.of) xs) []) = toList xs
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : IsLawfulTraversable t
xs : t α
⊢ List.reverse (unop (↑(Foldl.ofFreeMonoid (flip cons)) (foldMap FreeMonoid.of xs)) []) = toList xs
rw [foldMap_hom_free (Foldl.ofFreeMonoid (flip <| @cons α))]
no goals
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : IsLawfulTraversable t
xs : t α
⊢ List.reverse (unop (foldMap (↑(Foldl.ofFreeMonoid (flip cons)) ∘ FreeMonoid.of) xs) []) = toList xs
simp only [toList, foldl, List.reverse_inj, Foldl.get, foldl.ofFreeMonoid_comp_of,
  Function.comp_apply]