α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : IsLawfulTraversable t
f : α → β → α
xs : t β
x : α
⊢ foldl f x xs = unop (↑(Foldl.ofFreeMonoid f) (↑FreeMonoid.ofList (toList xs))) x
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : IsLawfulTraversable t
f : α → β → α
xs : t β
x : α
⊢ foldl f x xs = List.foldl f x (toList xs)
rw [← FreeMonoid.toList_ofList (toList xs), ← foldl.unop_ofFreeMonoid]
no goals
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : IsLawfulTraversable t
f : α → β → α
xs : t β
x : α
⊢ foldl f x xs = unop (↑(Foldl.ofFreeMonoid f) (↑FreeMonoid.ofList (toList xs))) x
simp only [foldl, toList_spec, foldMap_hom_free, foldl.ofFreeMonoid_comp_of, Foldl.get,
  FreeMonoid.ofList_toList]