Theorem: LeanColls.Insert.toList_singleton (LeanColls/Classes/Ops/Insert.lean)

State before:
C : Type u
τ : outParam (Type v)
inst✝⁴ : Insert C τ
x : τ
inst✝³ : ToList C τ
inst✝² : LeanColls.ToMultiset C τ
inst✝¹ : LawfulToList C τ
inst✝ : ToMultiset C τ
⊢ toList (singleton x) = [x]
Tactic:
apply Multiset.coe_eq_singleton.mp
State after:
C : Type u
τ : outParam (Type v)
inst✝⁴ : Insert C τ
x : τ
inst✝³ : ToList C τ
inst✝² : LeanColls.ToMultiset C τ
inst✝¹ : LawfulToList C τ
inst✝ : ToMultiset C τ
⊢ ↑(toList (singleton x)) = {x}

State before:
C : Type u
τ : outParam (Type v)
inst✝⁴ : Insert C τ
x : τ
inst✝³ : ToList C τ
inst✝² : LeanColls.ToMultiset C τ
inst✝¹ : LawfulToList C τ
inst✝ : ToMultiset C τ
⊢ ↑(toList (singleton x)) = {x}
Tactic:
rw [LawfulToList.toMultiset_toList]
State after:
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}

State before:
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}
Tactic:
rw [ToMultiset.toMultiset_singleton]
State after:
no goals