α : Type u_1
s✝ t✝ s t : Finset α
a : α
ht : t ∈ powerset s
h : ¬a ∈ s
⊢ a ∈ t → a ∈ s
α : Type u_1
s✝ t✝ s t : Finset α
a : α
ht : t ∈ powerset s
h : ¬a ∈ s
⊢ ¬a ∈ t
apply mt _ h
no goals
α : Type u_1
s✝ t✝ s t : Finset α
a : α
ht : t ∈ powerset s
h : ¬a ∈ s
⊢ a ∈ t → a ∈ s
apply mem_powerset.1 ht