case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
a✝ : Fintype ↑s
⊢ ∃ s', ∀ (a : α), a ∈ s' ↔ a ∈ s
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
h : Set.Finite s
⊢ ∃ s', ∀ (a : α), a ∈ s' ↔ a ∈ s
cases h
no goals
case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
a✝ : Fintype ↑s
⊢ ∃ s', ∀ (a : α), a ∈ s' ↔ a ∈ s
exact ⟨s.toFinset, fun _ => mem_toFinset⟩