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

State before:
α✝ : Type u_1
C : Type u_2
α : Type u_3
inst✝ : ToMultiset C α
c✝ c : C
v : α
hv : v ∈ c
⊢ ¬isEmpty c = true
Tactic:
simpa [size_eq_card_toMultiset, Multiset.eq_zero_iff_forall_not_mem] using ⟨v, hv⟩
State after:
no goals