case h
α : Type u_1
s✝ t s x✝ : Finset α
⊢ x✝ ∈ ↑(powerset s) ↔ x✝ ∈ toSet ⁻¹' 𝒫↑s
α : Type u_1
s✝ t s : Finset α
⊢ ↑(powerset s) = toSet ⁻¹' 𝒫↑s
ext
no goals
case h
α : Type u_1
s✝ t s x✝ : Finset α
⊢ x✝ ∈ ↑(powerset s) ↔ x✝ ∈ toSet ⁻¹' 𝒫↑s
simp