no goals
ι : Type ?u.264536
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
op : α → α → α
ha : IsAssociative α op
hc : IsCommutative α op
a : α
l : List α
a₁ a₂ : α
⊢ ((a :: l) <*> op a₁ a₂) = l <*> op a₁ (op a₂ a)
simp only [foldl_cons, ha.assoc]
no goals
ι : Type ?u.264536
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
op : α → α → α
ha : IsAssociative α op
hc : IsCommutative α op
a : α
l : List α
a₁ a₂ : α
⊢ (l <*> op a₁ (op a₂ a)) = op a₁ ((a :: l) <*> a₂)
rw [foldl_assoc, foldl_cons]