Theorem: ToList.lawfulEmptyCollection_iff (Algorithm/Data/Classes/ToList.lean)

State before:
C : Type u_1
α : Type u_2
inst✝¹ : ToList C α
inst✝ : EmptyCollection C
⊢ LawfulEmptyCollection C α ↔ toList ∅ = []
Tactic:
rw [ToMultiset.lawfulEmptyCollection_iff]
State after:
C : Type u_1
α : Type u_2
inst✝¹ : ToList C α
inst✝ : EmptyCollection C
⊢ ToMultiset.toMultiset ∅ = 0 ↔ toList ∅ = []

State before:
C : Type u_1
α : Type u_2
inst✝¹ : ToList C α
inst✝ : EmptyCollection C
⊢ ToMultiset.toMultiset ∅ = 0 ↔ toList ∅ = []
Tactic:
simp [toMultiset]
State after:
no goals