no goals
α✝ : Type u
β : Type v
ι : Sort w
γ : Type x
α : Type u
a : Set α
h : Set.Finite a
s : Set α
⊢ s ∈ Finset.map Finset.coeEmb.toEmbedding (Finset.powerset (Finite.toFinset h)) ↔ s ∈ {b | b ⊆ a}
simpa [← @exists_finite_iff_finset α fun t => t ⊆ a ∧ t = s, Finite.subset_toFinset, ←
  and_assoc, Finset.coeEmb] using h.subset