no goals
α : Type u_1
β : Type u_2
γ : Type ?u.48922
δ : Type ?u.48925
a✝ : α
s t : Multiset α
f✝ g : α → Multiset β
inst✝ : DecidableEq α
m : Multiset β
f : β → Multiset α
a : α
⊢ count a (sum (map f 0)) = sum (map (fun b => count a (f b)) 0)
simp
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.48922
δ : Type ?u.48925
a✝ : α
s t : Multiset α
f✝ g : α → Multiset β
inst✝ : DecidableEq α
m : Multiset β
f : β → Multiset α
a : α
⊢ ∀ ⦃a_1 : β⦄ {s : Multiset β},
    count a (sum (map f s)) = sum (map (fun b => count a (f b)) s) →
      count a (sum (map f (a_1 ::ₘ s))) = sum (map (fun b => count a (f b)) (a_1 ::ₘ s))
simp