[GOAL]
α : Type u_1
inst✝ : Fintype α
⊢ ↑(powerset univ) = ↑univ
[PROOFSTEP]
simp [-coe_eq_univ]
[GOAL]
α : Type u_1
inst✝ : Fintype α
s : Finset α
⊢ powerset s = univ ↔ s = univ
[PROOFSTEP]
rw [← Finset.powerset_univ, powerset_inj]
[GOAL]
α✝ : Type u_1
α : Type u_2
inst✝ : Fintype α
k : ℕ
⊢ filter (fun s => card s = k) univ = powersetLen k univ
[PROOFSTEP]
ext
[GOAL]
case a
α✝ : Type u_1
α : Type u_2
inst✝ : Fintype α
k : ℕ
a✝ : Finset α
⊢ a✝ ∈ filter (fun s => card s = k) univ ↔ a✝ ∈ powersetLen k univ
[PROOFSTEP]
simp [Finset.mem_powersetLen]
[GOAL]
α : Type u_1
inst✝ : Fintype α
k : ℕ
⊢ card { s // Finset.card s = k } = Nat.choose (card α) k
[PROOFSTEP]
simp [Fintype.subtype_card, Finset.card_univ]
[GOAL]
α : Type u_1
inst✝ : Fintype α
s : Set α
⊢ s ∈ map { toFun := toSet, inj' := (_ : Function.Injective toSet) } (Finset.powerset Finset.univ)
[PROOFSTEP]
classical
refine' mem_map.2 ⟨Finset.univ.filter s, Finset.mem_powerset.2 (Finset.subset_univ _), _⟩
apply (coe_filter _ _).trans
simp
rfl
[GOAL]
α : Type u_1
inst✝ : Fintype α
s : Set α
⊢ s ∈ map { toFun := toSet, inj' := (_ : Function.Injective toSet) } (Finset.powerset Finset.univ)
[PROOFSTEP]
refine' mem_map.2 ⟨Finset.univ.filter s, Finset.mem_powerset.2 (Finset.subset_univ _), _⟩
[GOAL]
α : Type u_1
inst✝ : Fintype α
s : Set α
⊢ ↑{ toFun := toSet, inj' := (_ : Function.Injective toSet) } (filter s Finset.univ) = s
[PROOFSTEP]
apply (coe_filter _ _).trans
[GOAL]
α : Type u_1
inst✝ : Fintype α
s : Set α
⊢ {x | x ∈ Finset.univ ∧ s x} = s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : Fintype α
s : Set α
⊢ {x | s x} = s
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : Finite α
⊢ Finite (Set α)
[PROOFSTEP]
cases nonempty_fintype α
[GOAL]
case intro
α : Type u_1
inst✝ : Finite α
val✝ : Fintype α
⊢ Finite (Set α)
[PROOFSTEP]
infer_instance
