Theorem: count_toMultiset_ne_zero (Algorithm/Data/Classes/ToMultiset.lean)

State before:
α✝ : Type u_1
C : Type u_2
α : Type u_3
inst✝¹ : ToMultiset C α
c✝ : C
inst✝ : DecidableEq α
a : α
c : C
⊢ Multiset.count a (toMultiset c) ≠ 0 ↔ a ∈ c
Tactic:
simp [count_toMultiset_eq_zero, mem_toMultiset]
State after:
no goals