no goals
α : Type u_1
ι : Sort ?u.3644
κ : ι → Sort ?u.3649
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
r : ℕ
A : Finset α
⊢ A ∈ 𝒜 → A ∈ powersetLen r univ ↔ A ∈ ↑𝒜 → card A = r
rw [mem_powerset_len_univ_iff, mem_coe]