case a
α✝ : Type ?u.1171
α : Type u_1
inst✝ : Fintype α
k : ℕ
a✝ : Finset α
⊢ a✝ ∈ filter (fun s => card s = k) univ ↔ a✝ ∈ powersetLen k univ
α✝ : Type ?u.1171
α : Type u_1
inst✝ : Fintype α
k : ℕ
⊢ filter (fun s => card s = k) univ = powersetLen k univ
ext
no goals
case a
α✝ : Type ?u.1171
α : Type u_1
inst✝ : Fintype α
k : ℕ
a✝ : Finset α
⊢ a✝ ∈ filter (fun s => card s = k) univ ↔ a✝ ∈ powersetLen k univ
simp [Finset.mem_powersetLen]