case a
α : Type u_1
s✝ t s a✝ : Finset α
⊢ a✝ ∈ powersetLen 0 s ↔ a✝ ∈ {∅}
α : Type u_1
s✝ t s : Finset α
⊢ powersetLen 0 s = {∅}
ext
case a
α : Type u_1
s✝ t s a✝ : Finset α
⊢ a✝ ⊆ s ∧ a✝ = ∅ ↔ a✝ = ∅
case a
α : Type u_1
s✝ t s a✝ : Finset α
⊢ a✝ ∈ powersetLen 0 s ↔ a✝ ∈ {∅}
rw [mem_powersetLen, mem_singleton, card_eq_zero]
no goals
case a
α : Type u_1
s✝ t s a✝ : Finset α
⊢ a✝ ⊆ s ∧ a✝ = ∅ ↔ a✝ = ∅
refine'
  ⟨fun h => h.2, fun h => by
    rw [h]
    exact ⟨empty_subset s, rfl⟩⟩
α : Type u_1
s✝ t s a✝ : Finset α
h : a✝ = ∅
⊢ ∅ ⊆ s ∧ ∅ = ∅
α : Type u_1
s✝ t s a✝ : Finset α
h : a✝ = ∅
⊢ a✝ ⊆ s ∧ a✝ = ∅
rw [h]
no goals
α : Type u_1
s✝ t s a✝ : Finset α
h : a✝ = ∅
⊢ ∅ ⊆ s ∧ ∅ = ∅
exact ⟨empty_subset s, rfl⟩