case mk
α : Type u_1
s t✝ t : Finset α
val✝ : Multiset α
nodup✝ : Nodup val✝
⊢ { val := val✝, nodup := nodup✝ } ∈ powerset t ↔ { val := val✝, nodup := nodup✝ } ⊆ t
α : Type u_1
s✝ t✝ s t : Finset α
⊢ s ∈ powerset t ↔ s ⊆ t
cases s
no goals
case mk
α : Type u_1
s t✝ t : Finset α
val✝ : Multiset α
nodup✝ : Nodup val✝
⊢ { val := val✝, nodup := nodup✝ } ∈ powerset t ↔ { val := val✝, nodup := nodup✝ } ⊆ t
simp [powerset, mem_mk, mem_pmap, mk.injEq, mem_powerset, exists_prop, exists_eq_right,
  ← val_le_iff]