case a
α : Type u_1
s✝ t : Finset α
n : ℕ
s a✝ : Finset α
⊢ a✝ ∈ powersetLen n s ↔ a✝ ∈ filter (fun x => card x = n) (powerset s)
α : Type u_1
s✝ t : Finset α
n : ℕ
s : Finset α
⊢ powersetLen n s = filter (fun x => card x = n) (powerset s)
ext
no goals
case a
α : Type u_1
s✝ t : Finset α
n : ℕ
s a✝ : Finset α
⊢ a✝ ∈ powersetLen n s ↔ a✝ ∈ filter (fun x => card x = n) (powerset s)
simp [mem_powersetLen]