ι : Type ?u.249628
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → α → α
hcomm : Commutative f
hassoc : Associative f
a b : α
l : List α
⊢ f b (foldl f a l) = f b (foldr f a l)
ι : Type ?u.249628
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → α → α
hcomm : Commutative f
hassoc : Associative f
a b : α
l : List α
⊢ foldl f a (b :: l) = foldr f a (b :: l)
simp only [foldr_cons, foldl_eq_of_comm_of_assoc hcomm hassoc]
no goals
ι : Type ?u.249628
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → α → α
hcomm : Commutative f
hassoc : Associative f
a b : α
l : List α
⊢ f b (foldl f a l) = f b (foldr f a l)
rw [foldl_eq_foldr a l]