rw [ToMultiset.toMultiset_singleton]
C : Type u
τ : outParam (Type v)
inst✝⁴ : Insert C τ
x : τ
inst✝³ : ToList C τ
inst✝² : LeanColls.ToMultiset C τ
inst✝¹ : LawfulToList C τ
inst✝ : ToMultiset C τ
⊢ ToMultiset.toMultiset (singleton x) = {x}
no goals