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

State before:
α✝ : Type u_1
C : Type u_2
α : Type u_3
inst✝ : ToMultiset C α
c : C
h : isEmpty c = true
⊢ toMultiset c = 0
Tactic:
simpa [size_eq_card_toMultiset] using h
State after:
no goals