no goals
α✝ : Type ?u.414392
β✝ : Type ?u.414395
γ : Type ?u.414398
inst✝¹ : DecidableEq α✝
α : Type u_1
β : Type u_2
f : α → β
s : Multiset α
inst✝ : DecidableEq β
b : β
⊢ count b (map f s) = ↑card (filter (fun a => b = f a) s)
simp [Bool.beq_eq_decide_eq, eq_comm, count, countp_map]