[GOAL]
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
A B : Set (Finset α)
r : ℕ
f : ι → Set (Finset α)
⊢ Sized r (⋃ (i : ι), f i) ↔ ∀ (i : ι), Sized r (f i)
[PROOFSTEP]
simp_rw [Set.Sized, Set.mem_iUnion, forall_exists_index]
[GOAL]
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
A B : Set (Finset α)
r : ℕ
f : ι → Set (Finset α)
⊢ (∀ ⦃x : Finset α⦄ (x_1 : ι), x ∈ f x_1 → card x = r) ↔ ∀ (i : ι) ⦃x : Finset α⦄, x ∈ f i → card x = r
[PROOFSTEP]
exact forall_swap
[GOAL]
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
A B : Set (Finset α)
r : ℕ
f : (i : ι) → κ i → Set (Finset α)
⊢ Sized r (⋃ (i : ι) (j : κ i), f i j) ↔ ∀ (i : ι) (j : κ i), Sized r (f i j)
[PROOFSTEP]
simp only [Set.sized_iUnion]
[GOAL]
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
r : ℕ
A : Finset α
⊢ A ∈ 𝒜 → A ∈ powersetLen r univ ↔ A ∈ ↑𝒜 → card A = r
[PROOFSTEP]
rw [mem_powerset_len_univ_iff, mem_coe]
[GOAL]
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
⊢ card 𝒜 ≤ Nat.choose (Fintype.card α) r
[PROOFSTEP]
rw [Fintype.card, ← card_powersetLen]
[GOAL]
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
⊢ card 𝒜 ≤ card (powersetLen r univ)
[PROOFSTEP]
exact card_le_of_subset (subset_powersetLen_univ_iff.mpr h𝒜)
[GOAL]
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
𝒜 : Finset (Finset α)
A A₁ A₂ : Finset α
r r₁ r₂ : ℕ
inst✝ : Fintype α
⊢ ∑ r in Iic (Fintype.card α), card (𝒜 # r) = card 𝒜
[PROOFSTEP]
letI := Classical.decEq α
[GOAL]
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
𝒜 : Finset (Finset α)
A A₁ A₂ : Finset α
r r₁ r₂ : ℕ
inst✝ : Fintype α
this : DecidableEq α := Classical.decEq α
⊢ ∑ r in Iic (Fintype.card α), card (𝒜 # r) = card 𝒜
[PROOFSTEP]
rw [← card_biUnion, biUnion_slice]
[GOAL]
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
𝒜 : Finset (Finset α)
A A₁ A₂ : Finset α
r r₁ r₂ : ℕ
inst✝ : Fintype α
this : DecidableEq α := Classical.decEq α
⊢ ∀ (x : ℕ), x ∈ Iic (Fintype.card α) → ∀ (y : ℕ), y ∈ Iic (Fintype.card α) → x ≠ y → Disjoint (𝒜 # x) (𝒜 # y)
[PROOFSTEP]
exact Finset.pairwiseDisjoint_slice.subset (Set.subset_univ _)
