Theorem: ToFinset.lawfulEmptyCollection_iff (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
⊢ LawfulEmptyCollection C α ↔ toFinset ∅ = ∅
Tactic:
rw [ToMultiset.lawfulEmptyCollection_iff]
State after:
α✝ : 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
⊢ ToMultiset.toMultiset ∅ = 0 ↔ toFinset ∅ = ∅

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
⊢ ToMultiset.toMultiset ∅ = 0 ↔ toFinset ∅ = ∅
Tactic:
change (toFinset (∅ : C)).val = ∅ ↔ _
State after:
α✝ : 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
⊢ (toFinset ∅).val = ∅ ↔ toFinset ∅ = ∅

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
⊢ (toFinset ∅).val = ∅ ↔ toFinset ∅ = ∅
Tactic:
simp
State after:
no goals