case mp
α✝ β α : Type u
s : Set α
⊢ (#↑s) = 0 → s = ∅

case mpr
α✝ β α : Type u
s : Set α
⊢ s = ∅ → (#↑s) = 0
α✝ β α : Type u
s : Set α
⊢ (#↑s) = 0 ↔ s = ∅
constructor
case mp
α✝ β α : Type u
s : Set α
h : (#↑s) = 0
⊢ s = ∅
case mp
α✝ β α : Type u
s : Set α
⊢ (#↑s) = 0 → s = ∅
intro h
case mp
α✝ β α : Type u
s : Set α
h : IsEmpty ↑s
⊢ s = ∅
case mp
α✝ β α : Type u
s : Set α
h : (#↑s) = 0
⊢ s = ∅
rw [mk_eq_zero_iff] at h
no goals
case mp
α✝ β α : Type u
s : Set α
h : IsEmpty ↑s
⊢ s = ∅
exact eq_empty_iff_forall_not_mem.2 fun x hx => h.elim' ⟨x, hx⟩
case mpr
α✝ β α : Type u
⊢ (#↑∅) = 0
case mpr
α✝ β α : Type u
s : Set α
⊢ s = ∅ → (#↑s) = 0
rintro rfl
no goals
case mpr
α✝ β α : Type u
⊢ (#↑∅) = 0
exact mk_emptyCollection _