case mk
α : Type u_1
s t✝ : Finset α
n : ℕ
t : Finset α
val✝ : Multiset α
nodup✝ : Nodup val✝
⊢ { val := val✝, nodup := nodup✝ } ∈ powersetLen n t ↔
    { val := val✝, nodup := nodup✝ } ⊆ t ∧ card { val := val✝, nodup := nodup✝ } = n
α : Type u_1
s✝ t✝ : Finset α
n : ℕ
s t : Finset α
⊢ s ∈ powersetLen n t ↔ s ⊆ t ∧ card s = n
cases s
no goals
case mk
α : Type u_1
s t✝ : Finset α
n : ℕ
t : Finset α
val✝ : Multiset α
nodup✝ : Nodup val✝
⊢ { val := val✝, nodup := nodup✝ } ∈ powersetLen n t ↔
    { val := val✝, nodup := nodup✝ } ⊆ t ∧ card { val := val✝, nodup := nodup✝ } = n
simp [powersetLen, val_le_iff.symm]