α : Type u_1
β : Type ?u.3980
inst✝ : DecidableEq α
m : Multiset α
a : α
x✝ : List α
⊢ List.count a (List.dedup x✝) = if a ∈ x✝ then 1 else 0
α : Type u_1
β : Type ?u.3980
inst✝ : DecidableEq α
m : Multiset α
a : α
x✝ : List α
⊢ count a (dedup (Quot.mk Setoid.r x✝)) = if a ∈ Quot.mk Setoid.r x✝ then 1 else 0
simp only [quot_mk_to_coe'', coe_dedup, mem_coe, List.mem_dedup, coe_nodup, coe_count]
no goals
α : Type u_1
β : Type ?u.3980
inst✝ : DecidableEq α
m : Multiset α
a : α
x✝ : List α
⊢ List.count a (List.dedup x✝) = if a ∈ x✝ then 1 else 0
apply List.count_dedup _ _