no goals
α : Type u_2
β : Type u_1
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
op' : β → β → β
inst✝¹ : IsCommutative β op'
inst✝ : IsAssociative β op'
m : α → β
hm : ∀ (x y : α), m (op x y) = op' (m x) (m y)
b : α
s : Multiset α
⊢ fold op' (m b) (map m 0) = m (fold op b 0)
simp
no goals
α : Type u_2
β : Type u_1
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
op' : β → β → β
inst✝¹ : IsCommutative β op'
inst✝ : IsAssociative β op'
m : α → β
hm : ∀ (x y : α), m (op x y) = op' (m x) (m y)
b : α
s : Multiset α
⊢ ∀ ⦃a : α⦄ {s : Multiset α},
    fold op' (m b) (map m s) = m (fold op b s) → fold op' (m b) (map m (a ::ₘ s)) = m (fold op b (a ::ₘ s))
simp (config := { contextual := true }) [hm]