Theorem: toFinset_empty (Algorithm/Data/Classes/ToFinset.lean)

State before:
α✝ : Type u_1
C : Type u_2
α : Type u_3
inst✝⁴ : ToFinset C α
c : C
inst✝³ : EmptyCollection C
inst✝² : LawfulEmptyCollection C α
inst✝¹ : ToFinset C α
inst✝ : EmptyCollection C
inst : LawfulEmptyCollection C α
⊢ toFinset ∅ = ∅
Tactic:
rwa [ToFinset.lawfulEmptyCollection_iff] at inst
State after:
no goals