no goals
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
x y : α
⊢ ↑(count x) (of y) = Pi.mulSingle x (↑Multiplicative.ofAdd 1) y
simp [count, countp_of, Pi.mulSingle_apply, eq_comm, Bool.beq_eq_decide_eq]