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