α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : IsLawfulTraversable t
f : α → β → β
xs : t α
x : β
⊢ foldr f x xs = ↑(Foldr.ofFreeMonoid f) (↑FreeMonoid.ofList (toList xs)) x
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : IsLawfulTraversable t
f : α → β → β
xs : t α
x : β
⊢ foldr f x xs = List.foldr f x (toList xs)
change _ = Foldr.ofFreeMonoid _ (FreeMonoid.ofList <| toList xs) _
no goals
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : IsLawfulTraversable t
f : α → β → β
xs : t α
x : β
⊢ foldr f x xs = ↑(Foldr.ofFreeMonoid f) (↑FreeMonoid.ofList (toList xs)) x
rw [toList_spec, foldr, Foldr.get, FreeMonoid.ofList_toList, foldMap_hom_free,
  foldr.ofFreeMonoid_comp_of]