α : Type u_1
ι : Sort ?u.4153
κ : ι → Sort ?u.4158
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
⊢ card 𝒜 ≤ card (powersetLen r univ)
α : Type u_1
ι : Sort ?u.4153
κ : ι → Sort ?u.4158
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
⊢ card 𝒜 ≤ Nat.choose (Fintype.card α) r
rw [Fintype.card, ← card_powersetLen]
no goals
α : Type u_1
ι : Sort ?u.4153
κ : ι → Sort ?u.4158
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
⊢ card 𝒜 ≤ card (powersetLen r univ)
exact card_le_of_subset (subset_powersetLen_univ_iff.mpr h𝒜)